6.2. Proof of the Tile Correlation Lemma #
This file contains the proofs of lemmas 6.2.1, 6.2.2, 6.2.3 and 6.1.5 from the blueprint.
Main definitions #
Tile.correlation: the functionφdefined in Lemma 6.2.1.
Main results #
Tile.mem_ball_of_correlation_ne_zeroandTile.correlation_kernel_bound: Lemma 6.2.1.Tile.range_support: Lemma 6.2.2.Tile.uncertainty: Lemma 6.2.3.Tile.correlation_leandTile.correlation_zero_of_ne_subset: Lemma 6.1.5.
noncomputable def
Tile.correlation
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
(s₁ s₂ : ℤ)
(x₁ x₂ y : X)
:
Def 6.2.1 (from Lemma 6.2.1), denoted by φ(y) in the blueprint.
Equations
- Tile.correlation s₁ s₂ x₁ x₂ y = (starRingEnd ℂ) (Ks s₁ x₁ y) * Ks s₂ x₂ y
Instances For
theorem
Tile.measurable_correlation
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
:
theorem
Tile.mem_ball_of_correlation_ne_zero
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{s₁ s₂ : ℤ}
{x₁ x₂ y : X}
(hy : correlation s₁ s₂ x₁ x₂ y ≠ 0)
:
First part of Lemma 6.2.1 (eq. 6.2.2).
theorem
Tile.correlation_kernel_bound
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{s₁ s₂ : ℤ}
{x₁ x₂ : X}
(hs : s₁ ≤ s₂)
:
iHolENorm (correlation s₁ s₂ x₁ x₂) x₁ (2 * ↑(defaultD a) ^ s₁) (defaultτ a) ≤ ↑(C6_2_1 a) / (MeasureTheory.volume (Metric.ball x₁ (↑(defaultD a) ^ s₁)) * MeasureTheory.volume (Metric.ball x₂ (↑(defaultD a) ^ s₂)))
Second part of Lemma 6.2.1 (eq. 6.2.3).
theorem
Tile.range_support
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{g : X → ℂ}
{y : X}
(hpy : adjointCarleson p g y ≠ 0)
:
Lemma 6.2.2.
theorem
Tile.uncertainty'
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(ha : 1 ≤ a)
{p₁ p₂ : 𝔓 X}
(hle : 𝔰 p₁ ≤ 𝔰 p₂)
(hinter : (Metric.ball (𝔠 p₁) (5 * ↑(defaultD a) ^ 𝔰 p₁) ∩ Metric.ball (𝔠 p₂) (5 * ↑(defaultD a) ^ 𝔰 p₂)).Nonempty)
{x₁ x₂ : X}
(hx₁ : x₁ ∈ E p₁)
(hx₂ : x₂ ∈ E p₂)
:
Lemma 6.2.3 (dist version).
theorem
Tile.uncertainty
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(ha : 1 ≤ a)
{p₁ p₂ : 𝔓 X}
(hle : 𝔰 p₁ ≤ 𝔰 p₂)
(hinter : (Metric.ball (𝔠 p₁) (5 * ↑(defaultD a) ^ 𝔰 p₁) ∩ Metric.ball (𝔠 p₂) (5 * ↑(defaultD a) ^ 𝔰 p₂)).Nonempty)
{x₁ x₂ : X}
(hx₁ : x₁ ∈ E p₁)
(hx₂ : x₂ ∈ E p₂)
:
Lemma 6.2.3 (edist version).
theorem
Tile.I12_le'
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p p' : 𝔓 X}
(hle : 𝔰 p' ≤ 𝔰 p)
{g : X → ℂ}
(x1 : ↑(E p'))
(x2 : ↑(E p))
:
Inequality (6.2.28).
theorem
Tile.I12_le
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(ha : 4 ≤ a)
{p p' : 𝔓 X}
(hle : 𝔰 p' ≤ 𝔰 p)
{g : X → ℂ}
(hinter : (Metric.ball (𝔠 p') (5 * ↑(defaultD a) ^ 𝔰 p') ∩ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)).Nonempty)
(x1 : ↑(E p'))
(x2 : ↑(E p))
:
Inequality (6.2.29).
theorem
Tile.volume_coeGrid_le
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
(x2 : ↑(E p))
:
MeasureTheory.volume ↑(𝓘 p) ≤ 2 ^ (3 * a) * MeasureTheory.volume (Metric.ball (↑x2) (↑(defaultD a) ^ 𝔰 p))
Inequality (6.2.32).
theorem
Tile.bound_6_2_29
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(ha : 4 ≤ a)
{p p' : 𝔓 X}
(x2 : ↑(E p))
:
2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 8 * a + 1) * (1 + edist_{𝔠 p', ↑(defaultD a) ^ 𝔰 p' / 4} (𝒬 p') (𝒬 p)) ^ (-(2 * ↑a ^ 2 + ↑a ^ 3)⁻¹) / MeasureTheory.volume (Metric.ball (↑x2) (↑(defaultD a) ^ 𝔰 p)) ≤ ↑(C6_1_5 a) * (1 + edist_{𝔠 p', ↑(defaultD a) ^ 𝔰 p' / 4} (𝒬 p') (𝒬 p)) ^ (-(2 * ↑a ^ 2 + ↑a ^ 3)⁻¹) / MeasureTheory.volume ↑(𝓘 p)
theorem
Tile.enorm_eq_zero_of_notMem_closedBall
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{g : X → ℂ}
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
{x : X}
(hx : x ∉ Metric.closedBall (cancelPt X) (↑(defaultD a) ^ defaultS X / 4))
:
theorem
Tile.eq_zero_of_notMem_closedBall
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{g : X → ℂ}
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
{x : X}
(hx : x ∉ Metric.closedBall (cancelPt X) (↑(defaultD a) ^ defaultS X / 4))
:
theorem
Tile.boundedCompactSupport_star_Ks_mul_g
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p' : 𝔓 X}
{g : X → ℂ}
(hg : Measurable g)
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
:
MeasureTheory.BoundedCompactSupport (fun (x : X × X) => (starRingEnd ℂ) (Ks (𝔰 p') x.1 x.2) * g x.1)
MeasureTheory.volume
theorem
Tile.boundedCompactSupport_Ks_mul_star_g
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p : 𝔓 X}
{g : X → ℂ}
(hg : Measurable g)
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
:
MeasureTheory.BoundedCompactSupport (fun (x : X × X) => Ks (𝔰 p) x.1 x.2 * (⇑(starRingEnd ℂ) ∘ g) x.1)
MeasureTheory.volume
theorem
Tile.boundedCompactSupport_aux_6_2_26
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p p' : 𝔓 X}
{g : X → ℂ}
(hg : Measurable g)
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
:
MeasureTheory.BoundedCompactSupport
(fun (x : X × X × X) =>
match x with
| (x, z1, z2) =>
(starRingEnd ℂ) (Ks (𝔰 p') z1 x) * Complex.exp (Complex.I * (↑((Q z1) z1) - ↑((Q z1) x))) * g z1 * (Ks (𝔰 p) z2 x * Complex.exp (Complex.I * (-↑((Q z2) z2) + ↑((Q z2) x))) * (starRingEnd ℂ) (g z2)))
MeasureTheory.volume
theorem
Tile.bound_6_2_26_aux
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p p' : 𝔓 X}
{g : X → ℂ}
:
have f := fun (x : X × X × X) =>
match x with
| (x, z1, z2) =>
(starRingEnd ℂ) (Ks (𝔰 p') z1 x) * Complex.exp (Complex.I * (↑((Q z1) z1) - ↑((Q z1) x))) * g z1 * (Ks (𝔰 p) z2 x * Complex.exp (Complex.I * (-↑((Q z2) z2) + ↑((Q z2) x))) * (starRingEnd ℂ) (g z2));
∫⁻ (x : X × X) in E p' ×ˢ E p, ‖∫ (y : X), f (y, x)‖ₑ = ∫⁻ (z : X × X) in E p' ×ˢ E p, I12 p p' g z.1 z.2
theorem
Tile.bound_6_2_26
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p p' : 𝔓 X}
{g : X → ℂ}
(hg : Measurable g)
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
:
theorem
Tile.correlation_le_of_nonempty_inter
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(ha : 4 ≤ a)
{p p' : 𝔓 X}
(hle : 𝔰 p' ≤ 𝔰 p)
{g : X → ℂ}
(hg : Measurable g)
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
(hinter : (Metric.ball (𝔠 p') (5 * ↑(defaultD a) ^ 𝔰 p') ∩ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)).Nonempty)
:
theorem
Tile.correlation_le_of_empty_inter
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p p' : 𝔓 X}
{g : X → ℂ}
(hinter : ¬(Metric.ball (𝔠 p') (5 * ↑(defaultD a) ^ 𝔰 p') ∩ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)).Nonempty)
:
If (6.2.23) does not hold, the LHS is zero and the result follows trivially.
theorem
Tile.correlation_le
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p p' : 𝔓 X}
(hle : 𝔰 p' ≤ 𝔰 p)
{g : X → ℂ}
(hg : Measurable g)
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
:
Part 1 of Lemma 6.1.5 (eq. 6.1.43).
theorem
Tile.correlation_zero_of_ne_subset
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{p p' : 𝔓 X}
(hle : 𝔰 p' ≤ 𝔰 p)
{g : X → ℂ}
(hp : ¬↑(𝓘 p') ⊆ Metric.ball (𝔠 p) (14 * ↑(defaultD a) ^ 𝔰 p))
:
Part 2 of Lemma 6.1.5 (claim 6.1.44).