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)
:
Equations
- Tile.correlation s₁ s₂ x₁ x₂ y = (starRingEnd ℂ) (Ks s₁ x₁ y) * Ks s₂ x₂ y
Instances For
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 : Tile.correlation s₁ s₂ x₁ x₂ y ≠ 0)
:
y ∈ Metric.ball x₁ (↑(defaultD a) ^ s₁)
theorem
Tile.aux_6_2_3
{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 y' : X)
:
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]
(ha : 1 < a)
{s₁ s₂ : ℤ}
(hs₁ : s₁ ∈ Set.Icc (-↑(defaultS X)) s₂)
{x₁ x₂ : X}
:
hnorm (Tile.correlation s₁ s₂ x₁ x₂) x₁ (↑(defaultD a) ^ s₁) ≤ ↑(Tile.C_6_2_1 a) / (MeasureTheory.volume (Metric.ball x₁ (↑(defaultD a) ^ s₁)) * MeasureTheory.volume (Metric.ball x₂ (↑(defaultD a) ^ s₂)))
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 : TileStructure.Forest.adjointCarleson p g y ≠ 0)
:
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₂)
:
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)
:
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 → ℂ}
(hg : Measurable g)
(hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
(hpp' : ¬↑(𝓘 p) ⊆ Metric.ball (𝔠 p) (15 * ↑(defaultD a) ^ 𝔰 p))
:
‖∫ (y : X),
TileStructure.Forest.adjointCarleson p' g y * (starRingEnd ℂ) (TileStructure.Forest.adjointCarleson p g y)‖₊ = 0