Documentation

Carleson.ForestOperator.RemainingTiles

Section 7.6 and Lemma 7.4.6 #

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₁ : 𝔓 X) :
Set (Grid X)

The definition 𝓙' at the start of Section 7.6. We use a different notation to distinguish it from the 𝓙' used in Section 7.5

Equations
Instances For
    source
    theorem TileStructure.Forest.union_𝓙₆ {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} (hu₁ : u₁ ∈ t) :
    ⋃ J ∈ t.𝓙₆ u₁, ↑J = ↑(π“˜ u₁)

    Part of Lemma 7.6.1.

    source
    theorem TileStructure.Forest.pairwiseDisjoint_𝓙₆ {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} :
    (t.𝓙₆ u₁).PairwiseDisjoint fun (I : Grid X) => ↑I

    Part of Lemma 7.6.1.

    source
    theorem TileStructure.Forest.C7_6_3_def (a n : β„•) :
    C7_6_3 a n = ↑(defaultZ a) * ↑n / (202 * ↑a ^ 3) - 2
    source
    @[irreducible]
    def TileStructure.Forest.C7_6_3 (a n : β„•) :
    ℝ

    The constant used in thin_scale_impact. This is denoted s₁ in the proof of Lemma 7.6.3. Has value Z * n / (202 * a ^ 3) - 2 in the blueprint.

    Equations
    Instances For
      source
      theorem TileStructure.Forest.nonneg_C7_6_3_add_two {a n : β„•} :
      0 ≀ C7_6_3 a n + 2
      source
      theorem TileStructure.Forest.thin_scale_impact_prelims {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} {J : Grid X} (hu₁ : u₁ ∈ t) (hJ : J ∈ t.𝓙₆ u₁) (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) (h : ↑(s J) - C7_6_3 a n < ↑(𝔰 p)) :
      dist (𝔠 p) (c J) < 16 * ↑(defaultD a) ^ (↑(𝔰 p) + C7_6_3 a n + 2) ∧ βˆƒ (J' : Grid X), J < J' ∧ s J' = s J + 1 ∧ βˆƒ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u₁, ↑(π“˜ p) βŠ† Metric.ball (c J') (100 * ↑(defaultD a) ^ (s J' + 1))

      Some preliminary relations for Lemma 7.6.3.

      source
      theorem TileStructure.Forest.thin_scale_impact_key {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} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₆ u₁) (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) (h : ↑(s J) - C7_6_3 a n < ↑(𝔰 p)) :
      2 ^ (defaultZ a * (n + 1) - 1) < 2 ^ (↑a * (100 * ↑a ^ 2 * (C7_6_3 a n + 2 + 1) + 9)) * 2 ^ (↑(defaultZ a) * ↑n / 2)

      The key relation of Lemma 7.6.3, which will eventually be shown to lead to a contradiction.

      source
      theorem TileStructure.Forest.thin_scale_impact {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} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₆ u₁) (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) :
      ↑(𝔰 p) ≀ ↑(s J) - C7_6_3 a n

      Lemma 7.6.3.

      source
      theorem TileStructure.Forest.C7_6_4_def (a : β„•) (s : β„€) :
      C7_6_4 a s = 2 ^ (14 * ↑a + 1) * (8 * ↑(defaultD a) ^ (-s)) ^ defaultΞΊ a
      source
      @[irreducible]
      def TileStructure.Forest.C7_6_4 (a : β„•) (s : β„€) :
      NNReal

      The constant used in square_function_count.

      Equations
      Instances For
        source
        theorem TileStructure.Forest.square_function_count {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} (hJ : J ∈ t.𝓙₆ u₁) (s' : β„€) :
        ⨍⁻ (x : X) in ↑J, (βˆ‘ I ∈ Finset.filter (fun (I : Grid X) => s I = s J - s' ∧ Disjoint ↑I ↑(π“˜ u₁) ∧ Β¬Disjoint (↑J) (Metric.ball (c I) (8 * ↑(defaultD a) ^ s I))) Finset.univ, (Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)).indicator 1 x) ^ 2 βˆ‚MeasureTheory.volume ≀ ↑(C7_6_4 a s')

        Lemma 7.6.4.

        source
        theorem TileStructure.Forest.C7_6_2_def (a n : β„•) :
        C7_6_2 a n = 2 ^ (118 * ↑a ^ 3 - 100 / (202 * ↑a) * ↑(defaultZ a) * ↑n * defaultΞΊ a)
        source
        @[irreducible]
        def TileStructure.Forest.C7_6_2 (a n : β„•) :
        NNReal

        The constant used in bound_for_tree_projection. Has value 2 ^ (118 * a ^ 3 - 100 / (202 * a) * Z * n * ΞΊ) in the blueprint.

        Equations
        Instances For
          source
          theorem TileStructure.Forest.bound_for_tree_projection {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} {f : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (h3f : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
          MeasureTheory.eLpNorm (approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–) 2 MeasureTheory.volume ≀ ↑(C7_6_2 a n) * MeasureTheory.eLpNorm ((↑(π“˜ u₁)).indicator fun (x : X) => (MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 (fun (x : X) => β€–f xβ€–) x).toReal) 2 MeasureTheory.volume

          Lemma 7.6.2. Todo: add needed hypothesis to LaTeX

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

          The constant used in correlation_near_tree_parts. Has value 2 ^ (541 * a ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3)) in the blueprint.

          Equations
          Instances For
            source
            theorem TileStructure.Forest.C7_4_6_def (a n : β„•) :
            C7_4_6 a n = 2 ^ (222 * ↑a ^ 3 - ↑(defaultZ a) * ↑n * 2 ^ (-10 * ↑a))
            source
            theorem TileStructure.Forest.correlation_near_tree_parts {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} {f₁ fβ‚‚ g₁ gβ‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) :
            β†‘β€–βˆ« (x : X), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(C7_4_6 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x).toReal) 2 MeasureTheory.volume

            Lemma 7.4.6