Documentation

Carleson.ForestOperator.LargeSeparation

Section 7.5 #

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 : TileStructure.Forest X n) (u₁ uβ‚‚ : 𝔓 X) :
Set (Grid X)

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

Equations
Instances For
    source
    def TileStructure.Forest.Ο‡tilde {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)] (J : Grid X) (x : X) :
    NNReal

    The definition of Ο‡-tilde, defined in the proof of Lemma 7.5.2

    Equations
    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 : TileStructure.Forest X n) (u₁ uβ‚‚ : 𝔓 X) (J : Grid X) (x : X) :
      NNReal

      The definition of Ο‡, defined in the proof of Lemma 7.5.2

      Equations
      Instances For
        source
        def TileStructure.Forest.holderFunction {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 : TileStructure.Forest X n) (u₁ uβ‚‚ : 𝔓 X) (f₁ fβ‚‚ : X β†’ β„‚) (J : Grid X) (x : X) :
        β„‚

        The definition of h_J, defined in the proof of Section 7.5.2

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Subsection 7.5.1 and Lemma 7.5.2 #

          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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) :
          ⋃ J ∈ t.𝓙₅ u₁ uβ‚‚, ↑J = ↑(π“˜ u₁)

          Part of Lemma 7.5.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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) :
          (t.𝓙₅ u₁ uβ‚‚).PairwiseDisjoint fun (I : Grid X) => ↑I

          Part of Lemma 7.5.1.

          source
          theorem TileStructure.Forest.moderate_scale_change {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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {J J' : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hJ' : J' ∈ t.𝓙₅ u₁ uβ‚‚) (h : Β¬Disjoint ↑J ↑J') :
          s J + 1 ≀ s J'

          Lemma 7.5.3 (stated somewhat differently).

          source
          theorem TileStructure.Forest.C7_5_2_def (a : β„•) :
          TileStructure.Forest.C7_5_2 a = 2 ^ (226 * ↑a ^ 3)
          source
          @[irreducible]
          def TileStructure.Forest.C7_5_2 (a : β„•) :
          NNReal

          The constant used in dist_Ο‡_Ο‡_le. Has value 2 ^ (226 * a ^ 3) in the blueprint.

          Equations
          Instances For
            source
            theorem TileStructure.Forest.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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (x : X) :
            βˆ‘ J ∈ Finset.filter (fun (I : Grid X) => I ∈ t.𝓙₅ u₁ uβ‚‚) Finset.univ, t.Ο‡ u₁ uβ‚‚ J x = (↑(π“˜ u₁)).indicator 1 x

            Part of Lemma 7.5.2.

            source
            theorem TileStructure.Forest.Ο‡_mem_Icc {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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x : X} {I J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hx : x ∈ π“˜ u₁) :
            t.Ο‡ u₁ uβ‚‚ J x ∈ Set.Icc 0 ((Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)).indicator 1 x)

            Part of Lemma 7.5.2.

            source
            theorem TileStructure.Forest.dist_Ο‡_Ο‡_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)] {n : β„•} {t : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x x' : X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hx : x ∈ π“˜ u₁) (hx' : x' ∈ π“˜ u₁) :
            dist (t.Ο‡ u₁ uβ‚‚ J x) (t.Ο‡ u₁ uβ‚‚ J x) ≀ ↑(TileStructure.Forest.C7_5_2 a) * dist x x' / ↑(defaultD a) ^ s J

            Part of Lemma 7.5.2.

            Subsection 7.5.2 and Lemma 7.5.4 #

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

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

            Equations
            Instances For
              source
              theorem TileStructure.Forest.C7_5_5_def (a : β„•) :
              TileStructure.Forest.C7_5_5 a = 2 ^ (151 * ↑a ^ 3)
              source
              theorem TileStructure.Forest.holder_correlation_tile {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 : TileStructure.Forest X n} {u p : 𝔓 X} {x x' : X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f) :
              ↑(nndist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * TileStructure.Forest.adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * TileStructure.Forest.adjointCarleson p f x')) ≀ ↑(TileStructure.Forest.C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (↑(nndist x x') / ↑(defaultD a) ^ ↑(𝔰 p)) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, ↑‖f xβ€–β‚Š

              Lemma 7.5.5.

              source
              theorem TileStructure.Forest.limited_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 : TileStructure.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₁ uβ‚‚) (h : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))) :
              𝔰 p ∈ Set.Icc (s J) (s J + 3)

              Lemma 7.5.6.

              source
              theorem TileStructure.Forest.C7_5_7_def (a : β„•) :
              TileStructure.Forest.C7_5_7 a = 2 ^ (104 * ↑a ^ 3)
              source
              @[irreducible]
              def TileStructure.Forest.C7_5_7 (a : β„•) :
              NNReal

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

              Equations
              Instances For
                source
                theorem TileStructure.Forest.local_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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
                ↑(⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚Š) ≀ ↑(TileStructure.Forest.C7_5_7 a) * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                Lemma 7.5.7.

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

                Lemma 7.5.8.

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

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

                Equations
                Instances For
                  source
                  theorem TileStructure.Forest.C7_5_9_1_def (a : β„•) :
                  TileStructure.Forest.C7_5_9_1 a = 2 ^ (154 * ↑a ^ 3)
                  source
                  @[irreducible]
                  def TileStructure.Forest.C7_5_9_2 (a : β„•) :
                  NNReal

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

                  Equations
                  Instances For
                    source
                    theorem TileStructure.Forest.C7_5_9_2_def (a : β„•) :
                    TileStructure.Forest.C7_5_9_2 a = 2 ^ (153 * ↑a ^ 3)
                    source
                    theorem TileStructure.Forest.global_tree_control1_1 {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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (β„­ : Set (𝔓 X)) (hβ„­ : β„­ = (fun (x : 𝔓 X) => t.𝔗 x) u₁ ∨ β„­ = (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
                    ↑(⨆ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum β„­ f xβ€–β‚Š) ≀ ↑(β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum β„­ f xβ€–β‚Š) + ↑(TileStructure.Forest.C7_5_9_1 a) * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                    Part 1 of Lemma 7.5.9

                    source
                    theorem TileStructure.Forest.global_tree_control1_2 {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 : TileStructure.Forest X n} {u u₁ uβ‚‚ p : 𝔓 X} {x x' : X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (β„­ : Set (𝔓 X)) (hβ„­ : β„­ = (fun (x : 𝔓 X) => t.𝔗 x) u₁ ∨ β„­ = (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) :
                    ↑(nndist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * TileStructure.Forest.adjointCarlesonSum β„­ f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * TileStructure.Forest.adjointCarlesonSum β„­ f x')) ≀ ↑(TileStructure.Forest.C7_5_9_1 a) * (↑(nndist x x') / ↑(defaultD a) ^ ↑(𝔰 p)) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                    Part 2 of Lemma 7.5.9

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

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

                    Equations
                    Instances For
                      source
                      theorem TileStructure.Forest.C7_5_10_def (a : β„•) :
                      TileStructure.Forest.C7_5_10 a = 2 ^ (155 * ↑a ^ 3)
                      source
                      theorem TileStructure.Forest.global_tree_control2 {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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
                      ↑(⨆ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚Š) ≀ β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), ↑‖TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) f xβ€–β‚Š + ↑(TileStructure.Forest.C7_5_10 a) * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                      Lemma 7.5.10

                      source
                      theorem TileStructure.Forest.C7_5_4_def (a : β„•) :
                      TileStructure.Forest.C7_5_4 a = 2 ^ (535 * ↑a ^ 3)
                      source
                      @[irreducible]
                      def TileStructure.Forest.C7_5_4 (a : β„•) :
                      NNReal

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

                      Equations
                      Instances For
                        source
                        theorem TileStructure.Forest.holder_correlation_tree {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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f₁ fβ‚‚ : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) :
                        HolderOnWith (TileStructure.Forest.C7_5_4 a * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f₁ xβ€–) x).toNNReal) * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) fβ‚‚ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–fβ‚‚ xβ€–) x).toNNReal)) (nnΟ„ X) (t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))

                        Lemma 7.5.4.

                        Subsection 7.5.3 and Lemma 7.4.5 #

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

                        The constant used in lower_oscillation_bound. Has value 2 ^ (Z * n / 2 - 201 * a ^ 3) in the blueprint.

                        Equations
                        Instances For
                          source
                          theorem TileStructure.Forest.C7_5_11_def (a n : β„•) :
                          TileStructure.Forest.C7_5_11 a n = 2 ^ (↑(defaultZ a) * ↑n / 2 - 201 * ↑a ^ 3)
                          source
                          theorem TileStructure.Forest.lower_oscillation_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 : TileStructure.Forest X n} {u₁ uβ‚‚ : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
                          ↑(TileStructure.Forest.C7_5_11 a n) ≀ dist (𝒬 u₁) (𝒬 uβ‚‚)

                          Lemma 7.5.11

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

                          The constant used in correlation_distant_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_5_def (a n : β„•) :
                            TileStructure.Forest.C7_4_5 a n = 2 ^ (541 * ↑a ^ 3 - ↑(defaultZ a) * ↑n / (4 * ↑a ^ 2 + 2 * ↑a ^ 3))
                            source
                            theorem TileStructure.Forest.correlation_distant_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 : TileStructure.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), TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(TileStructure.Forest.C7_4_5 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.5