Documentation

Carleson.ForestOperator.AlmostOrthogonality

Section 7.4 except Lemmas 4-6 #

source
noncomputable def TileStructure.Forest.adjointBoundaryOperator {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)] {n : β„•} (t : Forest X n) (u : 𝔓 X) (f : X β†’ β„‚) (x : X) :
ENNReal

The operator S_{2,𝔲} f(x), given above Lemma 7.4.3.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def TileStructure.Forest.𝔖₀ {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)] {n : β„•} (t : Forest X n) (u₁ uβ‚‚ : 𝔓 X) :
    Set (𝔓 X)

    The set 𝔖 defined in the proof of Lemma 7.4.4. We append a subscript 0 to distinguish it from the section variable.

    Equations
    Instances For
      source
      theorem TileStructure.Forest.adjoint_tile_support1 {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} {f : X β†’ β„‚} :
      adjointCarleson p f = (Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)).indicator (adjointCarleson p ((↑(π“˜ p)).indicator f))

      Part 1 of Lemma 7.4.1. Todo: update blueprint with precise properties needed on the function.

      source
      theorem TileStructure.Forest.adjoint_tile_support2 {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)] {n : β„•} {t : Forest X n} {u p : 𝔓 X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) :
      adjointCarleson p f = (↑(π“˜ u)).indicator (adjointCarleson p ((↑(π“˜ u)).indicator f))

      Part 2 of Lemma 7.4.1. Todo: update blueprint with precise properties needed on the function.

      source
      theorem TileStructure.Forest.adjoint_tile_support2_sum {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)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hu : u ∈ t) :
      adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f = (↑(π“˜ u)).indicator (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) ((↑(π“˜ u)).indicator f))
      source
      theorem TileStructure.Forest.adjoint_tile_support2_sum_partial {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)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hu : u ∈ t) :
      adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f = adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) ((↑(π“˜ u)).indicator f)

      A partially applied variant of adjoint_tile_support2_sum, used to prove Lemma 7.7.3.

      source
      theorem TileStructure.Forest.enorm_adjointCarleson_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} {f : X β†’ β„‚} {x : X} :
      β€–adjointCarleson p f xβ€–β‚‘ ≀ ↑(C2_1_3 a) * 2 ^ (4 * a) * (MeasureTheory.volume (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)))⁻¹ * ∫⁻ (y : X) in E p, β€–f yβ€–β‚‘
      source
      theorem TileStructure.Forest.enorm_adjointCarleson_le_mul_indicator {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} {f : X β†’ β„‚} {x : X} :
      β€–adjointCarleson p f xβ€–β‚‘ ≀ (↑(C2_1_3 a) * 2 ^ (4 * a) * (MeasureTheory.volume (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)))⁻¹ * ∫⁻ (y : X) in E p, β€–f yβ€–β‚‘) * (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)).indicator 1 x
      source
      theorem TileStructure.Forest.adjoint_density_tree_bound1 {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)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {f g : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (h2g : Function.support g βŠ† G) (hu : u ∈ t) :
      β€–βˆ« (x : X), (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) g x) * f xβ€–β‚‘ ≀ ↑(C7_3_1_1 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
      source
      theorem TileStructure.Forest.adjoint_tree_estimate {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)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {g : X β†’ β„‚} (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (h2g : Function.support g βŠ† G) (hu : u ∈ t) :
      MeasureTheory.eLpNorm (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) g) 2 MeasureTheory.volume ≀ ↑(C7_3_1_1 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

      Part 1 of Lemma 7.4.2.

      source
      theorem TileStructure.Forest.adjoint_density_tree_bound2 {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)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {f g : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (h2f : Function.support f βŠ† F) (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (h2g : Function.support g βŠ† G) (hu : u ∈ t) :
      β€–βˆ« (x : X), (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) g x) * f xβ€–β‚‘ ≀ ↑(C7_3_1_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * densβ‚‚ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
      source
      theorem TileStructure.Forest.indicator_adjoint_tree_estimate {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)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {g : X β†’ β„‚} (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (h2g : Function.support g βŠ† G) (hu : u ∈ t) :
      MeasureTheory.eLpNorm (F.indicator (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) g)) 2 MeasureTheory.volume ≀ ↑(C7_3_1_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * densβ‚‚ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

      Part 2 of Lemma 7.4.2.

      source
      @[irreducible]
      def TileStructure.Forest.C7_4_3 (a : β„•) :
      NNReal

      The constant used in adjoint_tree_control. Has value 2 ^ (182 * a ^ 3) in the blueprint.

      Equations
      Instances For
        source
        theorem TileStructure.Forest.C7_4_3_def (a : β„•) :
        C7_4_3 a = 2 ^ ((𝕔 + 7 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3)
        source
        theorem TileStructure.Forest.le_C7_4_3 {a : β„•} (ha : 4 ≀ a) :
        C7_3_1_1 a + CMB (↑(defaultA a)) 2 + 1 ≀ C7_4_3 a
        source
        theorem TileStructure.Forest.adjoint_tree_control {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)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hu : u ∈ t) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (h2f : Function.support f βŠ† G) :
        MeasureTheory.eLpNorm (fun (x : X) => t.adjointBoundaryOperator u f x) 2 MeasureTheory.volume ≀ ↑(C7_4_3 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

        Lemma 7.4.3.

        source
        theorem TileStructure.Forest.overlap_implies_distance {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)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u₁ βˆͺ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) (hpu₁ : Β¬Disjoint ↑(π“˜ p) ↑(π“˜ u₁)) :
        p ∈ t.𝔖₀ u₁ uβ‚‚

        Part 1 of Lemma 7.4.7.

        source
        theorem TileStructure.Forest.𝔗_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)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) :
        (fun (x : 𝔓 X) => t.𝔗 x) u₁ βŠ† t.𝔖₀ u₁ uβ‚‚

        Part 2 of Lemma 7.4.7.