Documentation

Carleson.ForestOperator.QuantativeEstimate

Section 7.3 and Lemma 7.3.1 #

source
theorem TileStructure.Forest.C7_3_2_def (a : β„•) :
C7_3_2 a = 2 ^ ((𝕔 + 1) * a ^ 3)
source
@[irreducible]
def TileStructure.Forest.C7_3_2 (a : β„•) :
NNReal

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

Equations
Instances For
    source
    theorem TileStructure.Forest.local_dens1_tree_bound_exists {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} {L : Grid X} (hu : u ∈ t) (hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) (hpβ‚‚ : βˆƒ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u, Β¬Disjoint (↑L) (E p) ∧ 𝔰 p ≀ s L) :
    MeasureTheory.volume (↑L ∩ G ∩ ⋃ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u, E p) ≀ ↑(C7_3_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) * MeasureTheory.volume ↑L

    Part 1 of Lemma 7.3.2.

    source
    theorem TileStructure.Forest.volume_bound_of_Grid_lt {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)] {L L' : Grid X} (lL : L ≀ L') (sL : s L' = s L + 1) :
    MeasureTheory.volume ↑L' ≀ 2 ^ (𝕔 * a ^ 3 + 5 * a) * MeasureTheory.volume ↑L
    source
    theorem TileStructure.Forest.local_dens1_tree_bound {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} {L : Grid X} (hu : u ∈ t) (hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) :
    MeasureTheory.volume (↑L ∩ G ∩ ⋃ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u, E p) ≀ ↑(C7_3_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) * MeasureTheory.volume ↑L

    Lemma 7.3.2.

    source
    theorem TileStructure.Forest.C7_3_3_def (a : β„•) :
    C7_3_3 a = 2 ^ ((2 * ↑𝕔 + 1) * ↑a ^ 3)
    source
    @[irreducible]
    def TileStructure.Forest.C7_3_3 (a : β„•) :
    NNReal

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

    Equations
    Instances For
      source
      theorem TileStructure.Forest.local_dens2_tree_bound {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} {J : Grid X} (hu : u ∈ t) (hJ : J ∈ 𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) :
      MeasureTheory.volume (F ∩ ↑J) ≀ ↑(C7_3_3 a) * densβ‚‚ ((fun (x : 𝔓 X) => t.𝔗 x) u) * MeasureTheory.volume ↑J

      Lemma 7.3.3.

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

      The constant used in density_tree_bound1 and adjoint_tree_estimate. Has value 2 ^ (181 * a ^ 3) in the blueprint.

      Equations
      Instances For
        source
        theorem TileStructure.Forest.C7_3_1_1_def (a : β„•) :
        C7_3_1_1 a = 2 ^ ((𝕔 + 6 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3)
        source
        theorem TileStructure.Forest.eLpNorm_approxOnCube_two_le_self {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)] {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) {C : Set (Grid X)} (pdC : C.PairwiseDisjoint fun (I : Grid X) => ↑I) :
        MeasureTheory.eLpNorm (approxOnCube C fun (x : X) => β€–f xβ€–) 2 MeasureTheory.volume ≀ MeasureTheory.eLpNorm f 2 MeasureTheory.volume
        source
        theorem TileStructure.Forest.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 β„‚) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) 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

        First part of Lemma 7.3.1.

        source
        theorem TileStructure.Forest.C7_3_1_2_def (a : β„•) :
        C7_3_1_2 a = 2 ^ ((2 * 𝕔 + 7 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3)
        source
        @[irreducible]
        def TileStructure.Forest.C7_3_1_2 (a : β„•) :
        NNReal

        The constant used in density_tree_bound2 and indicator_adjoint_tree_estimate. Has value 2 ^ (282 * a ^ 3) in the blueprint.

        Equations
        Instances For
          source
          theorem TileStructure.Forest.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 β„‚) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) 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

          Second part of Lemma 7.3.1.

          source
          theorem MeasureTheory.BoundedCompactSupport.const_smul {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {f : X β†’ β„‚} (hf : BoundedCompactSupport f volume) (c : ℝ) :
          BoundedCompactSupport (c β€’ f) volume
          source
          theorem smul_le_indicator {X : Type u_1} {f : X β†’ β„‚} {A : Set X} (hf : Function.support f βŠ† A) {C : ℝ} (hC : βˆ€ (x : X), β€–f xβ€– ≀ C) (hCpos : 0 < C) (x : X) :
          β€–(C⁻¹ β€’ f) xβ€– ≀ A.indicator 1 x
          source
          theorem MonoidHomClass.map_mulIndicator {F : Type u_3} {X : Type u_4} {A : Type u_5} {B : Type u_6} [Monoid A] [Monoid B] [FunLike F A B] [MonoidHomClass F A B] {s : Set X} (f : F) (x : X) (g : X β†’ A) :
          f (s.mulIndicator g x) = s.mulIndicator (⇑f ∘ g) x
          source
          theorem AddMonoidHomClass.map_indicator {F : Type u_3} {X : Type u_4} {A : Type u_5} {B : Type u_6} [AddMonoid A] [AddMonoid B] [FunLike F A B] [AddMonoidHomClass F A B] {s : Set X} (f : F) (x : X) (g : X β†’ A) :
          f (s.indicator g x) = s.indicator (⇑f ∘ g) x