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 : 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) (u₁ : 𝔓 X) :
    X β†’ NNReal

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

    Equations
    Instances For
      source
      theorem TileStructure.Forest.Ο‡tilde_pos_iff {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)] {u₁ : 𝔓 X} {x : X} {J : Grid X} :
      0 < Ο‡tilde J u₁ x ↔ x ∈ π“˜ u₁ ∧ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)
      source
      theorem TileStructure.Forest.Ο‡tilde_le_eight {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)] {u₁ : 𝔓 X} {x : X} {J : Grid X} :
      Ο‡tilde J u₁ x ≀ 8
      source
      theorem TileStructure.Forest.four_lt_Ο‡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)] {u₁ : 𝔓 X} {x : X} {J : Grid X} (xJ : x ∈ J) (xu : x ∈ π“˜ u₁) :
      4 < Ο‡tilde J u₁ x
      source
      theorem TileStructure.Forest.dist_Ο‡tilde_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)] {u₁ : 𝔓 X} {x x' : X} {J : Grid X} (mx : x ∈ π“˜ u₁) (mx' : x' ∈ π“˜ u₁) :
      dist (Ο‡tilde J u₁ x) (Ο‡tilde J u₁ x') ≀ dist x x' / ↑(defaultD a) ^ s J
      source
      theorem TileStructure.Forest.stronglyMeasurable_Ο‡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)] {u₁ : 𝔓 X} {J : Grid X} :
      MeasureTheory.StronglyMeasurable (Ο‡tilde J u₁)
      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) (J : Grid X) (x : X) :
      NNReal

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

      Equations
      Instances For
        source
        theorem TileStructure.Forest.stronglyMeasurable_Ο‡ {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} {J : Grid X} :
        MeasureTheory.StronglyMeasurable (t.Ο‡ u₁ uβ‚‚ J)
        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 : 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
          source
          theorem TileStructure.Forest.IF_subset_THEN_not_disjoint {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)] {A B : Grid X} (h : ↑A βŠ† ↑B) :
          Β¬Disjoint ↑B ↑A
          source
          theorem TileStructure.Forest.IF_disjoint_with_ball_THEN_distance_bigger_than_radius {X : Type u_1} [MetricSpace X] {J : X} {r : ℝ} {pSet : Set X} {p : X} (belongs : p ∈ pSet) (h : Disjoint (Metric.ball J r) pSet) :
          dist J p β‰₯ r
          source
          theorem TileStructure.Forest.dist_triangle5 {X : Type u_1} [MetricSpace X] (a b c d e : X) :
          dist a e ≀ dist a b + dist b c + dist c d + dist d e
          source
          theorem TileStructure.Forest.π“˜_subset_iUnion_𝓙_𝔖₀ {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} :
          ↑(π“˜ u₁) βŠ† ⋃ J ∈ 𝓙 (t.𝔖₀ u₁ uβ‚‚), ↑J

          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 : 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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} :
          (t.𝓙₅ u₁ uβ‚‚).PairwiseDisjoint fun (I : Grid X) => ↑I

          Part of Lemma 7.5.1.

          source
          theorem TileStructure.Forest.four_lt_sum_Ο‡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)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x : X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hx : x ∈ π“˜ u₁) :
          4 < βˆ‘ J' ∈ (t.𝓙₅ u₁ uβ‚‚).toFinset, Ο‡tilde J' u₁ x
          source
          theorem TileStructure.Forest.bigger_than_𝓙_is_not_in_𝓙₀ {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)] {𝔖 : Set (𝔓 X)} {A B : Grid X} (le : A ≀ B) (sle : s A < s B) (A_in : A ∈ 𝓙 𝔖) :
          B βˆ‰ 𝓙₀ 𝔖
          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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {J J' : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hJ' : J' ∈ t.𝓙₅ u₁ uβ‚‚) (hd : Β¬Disjoint (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (Metric.ball (c J') (8 * ↑(defaultD a) ^ s J'))) :
          s J - 1 ≀ s J'

          Lemma 7.5.3 (stated somewhat differently).

          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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (x : X) :
          βˆ‘ J ∈ (t.𝓙₅ u₁ uβ‚‚).toFinset, t.Ο‡ u₁ uβ‚‚ J x = (↑(π“˜ u₁)).indicator 1 x

          Part of Lemma 7.5.2.

          source
          theorem TileStructure.Forest.Ο‡_le_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)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x : X} {J : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
          t.Ο‡ u₁ uβ‚‚ J x ≀ (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)).indicator 1 x

          Part of Lemma 7.5.2.

          source
          theorem TileStructure.Forest.Ο‡_eq_zero_of_notMem_ball {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} {x : X} {J : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (nx : x βˆ‰ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) :
          t.Ο‡ u₁ uβ‚‚ J x = 0
          source
          theorem TileStructure.Forest.boundedCompactSupport_toReal_Ο‡ {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} {J : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
          MeasureTheory.BoundedCompactSupport (fun (x : X) => ↑(t.Ο‡ u₁ uβ‚‚ J x)) MeasureTheory.volume
          source
          theorem TileStructure.Forest.C7_5_2_def (a : β„•) :
          C7_5_2 a = 2 ^ ((2 * 𝕔 + 2 + 𝕔 / 4) * a ^ 3)
          source
          @[irreducible]
          def TileStructure.Forest.C7_5_2 (a : β„•) :
          NNReal

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

          Equations
          Instances For
            source
            theorem TileStructure.Forest.one_le_C7_5_2 {a : β„•} :
            1 ≀ C7_5_2 a
            source
            theorem TileStructure.Forest.quarter_add_two_mul_D_mul_card_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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {J : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
            1 / 4 + 2 * ↑(defaultD a) * ↑{J' ∈ (t.𝓙₅ u₁ uβ‚‚).toFinset | Β¬Disjoint (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (Metric.ball (c J') (8 * ↑(defaultD a) ^ s J'))}.card ≀ ↑(C7_5_2 a)
            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 : 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β‚‚) (mx : x ∈ π“˜ u₁) (mx' : x' ∈ π“˜ u₁) :
            dist (t.Ο‡ u₁ uβ‚‚ J x) (t.Ο‡ u₁ uβ‚‚ J x') ≀ ↑(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
            theorem TileStructure.Forest.C7_5_5_def (a : β„•) :
            C7_5_5 a = 2 ^ ((𝕔 + 3 + 𝕔 / 4) * a ^ 3)
            source
            @[irreducible]
            def TileStructure.Forest.C7_5_5 (a : β„•) :
            NNReal

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

            Equations
            Instances For
              source
              theorem TileStructure.Forest.ψ_le_max {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {x : ℝ} :
              ψ (defaultD a) x ≀ max 0 ((2 - 4 * x) ^ (↑a)⁻¹)
              source
              theorem TileStructure.Forest.le_of_mem_E {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} {x x' y : X} (hy : y ∈ E p) (hx' : x' βˆ‰ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
              2 - 4 * (↑(defaultD a) ^ (-𝔰 p) * dist y x) ≀ dist x x' / ↑(defaultD a) ^ 𝔰 p * 4
              source
              theorem TileStructure.Forest.enorm_ψ_le_edist {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} {x x' y : X} (my : y ∈ E p) (hx' : x' βˆ‰ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
              β€–Οˆ (defaultD a) (↑(defaultD a) ^ (-𝔰 p) * dist y x)β€–β‚‘ ≀ 4 * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹
              source
              theorem TileStructure.Forest.holder_correlation_tile_one {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} {x x' : X} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hx' : x' βˆ‰ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
              β€–adjointCarleson p f xβ€–β‚‘ ≀ ↑(C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘
              source
              theorem TileStructure.Forest.integrable_adjointCarleson_interior {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)] {u p : 𝔓 X} {x : X} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) :
              MeasureTheory.Integrable (fun (y : X) => Complex.exp (Complex.I * ↑((𝒬 u) x)) * ((starRingEnd β„‚) (Ks (𝔰 p) y x) * Complex.exp (Complex.I * (↑((Q y) y) - ↑((Q y) x))) * f y)) (MeasureTheory.volume.restrict (E p))
              source
              theorem TileStructure.Forest.holder_correlation_rearrange {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)] {u p : 𝔓 X} {x x' : X} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) :
              edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarleson p f x') ≀ (∫⁻ (y : X) in E p, β€–f yβ€–β‚‘ * β€–Ks (𝔰 p) y xβ€–β‚‘ * β€–-(Q y) x + (Q y) x' + (𝒬 u) x - (𝒬 u) x'β€–β‚‘) + ∫⁻ (y : X) in E p, β€–f yβ€–β‚‘ * β€–Ks (𝔰 p) y x - Ks (𝔰 p) y x'β€–β‚‘

              Sub-equations (7.5.10) and (7.5.11) in Lemma 7.5.5.

              source
              theorem TileStructure.Forest.Q7_5_5_def (a : β„•) :
              Q7_5_5 a = 10 * 2 ^ (6 * a)
              source
              @[irreducible]
              def TileStructure.Forest.Q7_5_5 (a : β„•) :
              NNReal

              Multiplicative factor for the bound on β€–- Q y x + Q y x' + 𝒬 u x - 𝒬 u x'β€–β‚‘.

              Equations
              Instances For
                source
                theorem TileStructure.Forest.QQQQ_bound_real {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} {x x' y : X} (my : y ∈ E p) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hx : x ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) (hx' : x' ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
                β€–-(Q y) x + (Q y) x' + (𝒬 u) x - (𝒬 u) x'β€– ≀ ↑(Q7_5_5 a) * (dist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹
                source
                theorem TileStructure.Forest.QQQQ_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 p : 𝔓 X} {x x' y : X} (my : y ∈ E p) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hx : x ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) (hx' : x' ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
                β€–-(Q y) x + (Q y) x' + (𝒬 u) x - (𝒬 u) x'β€–β‚‘ ≀ ↑(Q7_5_5 a) * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹
                source
                theorem TileStructure.Forest.holder_correlation_tile_two {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} {x x' : X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hx : x ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) (hx' : x' ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
                edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarleson p f x') ≀ ↑(C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘
                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 : 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 MeasureTheory.volume) :
                edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarleson p f x') ≀ ↑(C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘

                Lemma 7.5.5.

                source
                theorem TileStructure.Forest.limited_scale_impact_first_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₁ 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))) :
                s J ≀ 𝔰 p

                Part of Lemma 7.5.6.

                source
                theorem TileStructure.Forest.limited_scale_impact_second_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₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (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 ≀ s J + 3

                Part of Lemma 7.5.6.

                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 : 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.local_tree_control_sumsumsup {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 β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
                ⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚‘ ≀ βˆ‘ k ∈ Finset.Icc (s J) (s J + 3), βˆ‘ p : 𝔓 X with 𝔰 p = k ∧ Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J)), ⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarleson p f xβ€–β‚‘
                source
                theorem TileStructure.Forest.local_tree_control_sup_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)] {p : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} {k : β„€} (mk : k ∈ Finset.Icc (s J) (s J + 3)) (mp : 𝔰 p = k ∧ Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))) (nfm : AEMeasurable (fun (x : X) => β€–f xβ€–β‚‘) MeasureTheory.volume) :
                ⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarleson p f xβ€–β‚‘ ≀ 2 ^ ((𝕔 + 3) * a ^ 3) * (MeasureTheory.volume (Metric.ball (c J) (16 * ↑(defaultD a) ^ k)))⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘
                source
                theorem TileStructure.Forest.C7_5_7_def (a : β„•) :
                C7_5_7 a = 2 ^ ((𝕔 + 4) * 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 : 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 MeasureTheory.volume) :
                  ⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚‘ ≀ ↑(C7_5_7 a) * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f 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 : 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) (16 * ↑(defaultD a) ^ s J))) :
                  s J ≀ 𝔰 p

                  Lemma 7.5.8.

                  source
                  theorem TileStructure.Forest.volume_cpDsp_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)] {p : 𝔓 X} {J : Grid X} (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (16 * ↑(defaultD a) ^ s J))) (hs : s J ≀ 𝔰 p) :
                  MeasureTheory.volume (Metric.ball (c J) (32 * ↑(defaultD a) ^ 𝔰 p)) / 2 ^ (4 * a) ≀ MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p))
                  source
                  theorem TileStructure.Forest.gtc_integral_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)] {f : X β†’ β„‚} {J : Grid X} {k : β„€} {β„­ : Set (𝔓 X)} (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) :
                  βˆ‘ p ∈ β„­.toFinset with Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) ∧ 𝔰 p = k, ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘ ≀ ∫⁻ (x : X) in Metric.ball (c J) (32 * ↑(defaultD a) ^ k), β€–f xβ€–β‚‘
                  source
                  theorem TileStructure.Forest.global_tree_control1_edist_part1 {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} {x x' : X} {f : X β†’ β„‚} {J : Grid X} (hu : u ∈ t) {β„­ : Set (𝔓 X)} (hβ„­ : β„­ βŠ† (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) (hx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                  edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarlesonSum β„­ f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarlesonSum β„­ f x') ≀ ↑(C7_5_5 a) * 2 ^ (4 * a) * edist x x' ^ (↑a)⁻¹ * βˆ‘ k ∈ Finset.Icc (s J) ↑(defaultS X), ↑(defaultD a) ^ (-↑k / ↑a) * ⨍⁻ (x : X) in Metric.ball (c J) (32 * ↑(defaultD a) ^ k), β€–f xβ€–β‚‘ βˆ‚MeasureTheory.volume

                  Part 1 of equation (7.5.18) of Lemma 7.5.9.

                  source
                  theorem TileStructure.Forest.gtc_sum_Icc_le_two {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} :
                  βˆ‘ k ∈ Finset.Icc (s J) ↑(defaultS X), ↑(defaultD a) ^ ((↑(s J) - ↑k) / ↑a) ≀ 2
                  source
                  theorem TileStructure.Forest.C7_5_9d_def (a : β„•) :
                  C7_5_9d a = C7_5_5 a * 2 ^ (4 * a + 1)
                  source
                  @[irreducible]
                  def TileStructure.Forest.C7_5_9d (a : β„•) :
                  NNReal

                  The constant used in global_tree_control1_edist. Has value 2 ^ (128 * a ^ 3 + 4 * a + 1) in the blueprint.

                  Equations
                  Instances For
                    source
                    theorem TileStructure.Forest.global_tree_control1_edist_part2 {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} {x x' : X} {f : X β†’ β„‚} {J : Grid X} (hu : u ∈ t) {β„­ : Set (𝔓 X)} (hβ„­ : β„­ βŠ† (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) (hx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                    edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarlesonSum β„­ f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarlesonSum β„­ f x') ≀ ↑(C7_5_9d a) * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

                    Part 2 of equation (7.5.18) of Lemma 7.5.9.

                    source
                    theorem TileStructure.Forest.global_tree_control1_edist_left {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} {x x' : 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 MeasureTheory.volume) (hx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                    edist (Complex.exp (Complex.I * ↑((𝒬 u₁) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f x) (Complex.exp (Complex.I * ↑((𝒬 u₁) x')) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f x') ≀ ↑(C7_5_9d a) * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

                    Equation (7.5.18) of Lemma 7.5.9 for β„­ = t u₁.

                    source
                    theorem TileStructure.Forest.global_tree_control1_edist_right {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} {x x' : 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 MeasureTheory.volume) (hx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                    edist (Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f x) (Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x')) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f x') ≀ ↑(C7_5_9d a) * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

                    Equation (7.5.18) of Lemma 7.5.9 for β„­ = t uβ‚‚ ∩ 𝔖₀ t u₁ uβ‚‚.

                    source
                    theorem TileStructure.Forest.C7_5_9s_def (a : β„•) :
                    C7_5_9s a = C7_5_5 a * 2 ^ (4 * a + 3)
                    source
                    @[irreducible]
                    def TileStructure.Forest.C7_5_9s (a : β„•) :
                    NNReal

                    The constant used in global_tree_control1_supbound. Has value 2 ^ (128 * a ^ 3 + 4 * a + 3) in the blueprint.

                    Equations
                    Instances For
                      source
                      theorem TileStructure.Forest.one_le_C7_5_9s {a : β„•} :
                      1 ≀ C7_5_9s a
                      source
                      theorem TileStructure.Forest.C7_5_9d_le_C7_5_9s {a : β„•} :
                      C7_5_9d a ≀ C7_5_9s a
                      source
                      theorem TileStructure.Forest.global_tree_control1_supbound {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 β†’ β„‚} {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 MeasureTheory.volume) :
                      ⨆ x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum β„­ f xβ€–β‚‘ ≀ (β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum β„­ f xβ€–β‚‘) + ↑(C7_5_9s a) * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

                      Equation (7.5.17) 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 ^ (129 * a ^ 3) in the blueprint.

                      Equations
                      Instances For
                        source
                        theorem TileStructure.Forest.C7_5_10_def (a : β„•) :
                        C7_5_10 a = 2 ^ ((𝕔 + 4 + 𝕔 / 4) * a ^ 3)
                        source
                        theorem TileStructure.Forest.le_C7_5_10 {a : β„•} (ha : 4 ≀ a) :
                        C7_5_7 a + C7_5_9s a ≀ C7_5_10 a
                        source
                        theorem TileStructure.Forest.C7_5_9s_le_C7_5_10 {a : β„•} (ha : 4 ≀ a) :
                        C7_5_9s a ≀ C7_5_10 a
                        source
                        theorem TileStructure.Forest.one_le_C7_5_10 {a : β„•} (ha : 4 ≀ a) :
                        1 ≀ C7_5_10 a
                        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 : 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 MeasureTheory.volume) :
                        ⨆ x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚‘ ≀ (β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) f xβ€–β‚‘) + ↑(C7_5_10 a) * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

                        Lemma 7.5.10

                        source
                        def TileStructure.Forest.P7_5_4 {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β‚‚ : X β†’ β„‚) (J : Grid X) :
                        ENNReal

                        The product on the right-hand side of Lemma 7.5.4.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem TileStructure.Forest.P7_5_4_le_adjointBoundaryOperator_mul {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} {x : X} {f₁ fβ‚‚ : X β†’ β„‚} {J : Grid X} (mx : x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J)) :
                          t.P7_5_4 u₁ uβ‚‚ f₁ fβ‚‚ J ≀ t.adjointBoundaryOperator u₁ f₁ x * t.adjointBoundaryOperator uβ‚‚ fβ‚‚ x
                          source
                          theorem TileStructure.Forest.support_holderFunction_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₁ : 𝔓 X} (uβ‚‚ : 𝔓 X) (f₁ fβ‚‚ : X β†’ β„‚) (J : Grid X) (hu₁ : u₁ ∈ t) :
                          Function.support (t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J) βŠ† ↑(π“˜ u₁)

                          The support of holderFunction is in π“˜ u₁.

                          source
                          theorem TileStructure.Forest.enorm_holderFunction_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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x : 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₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) (mx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                          β€–t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J xβ€–β‚‘ ≀ ↑(C7_5_9s a) * ↑(C7_5_10 a) * t.P7_5_4 u₁ uβ‚‚ f₁ fβ‚‚ J
                          source
                          theorem TileStructure.Forest.holder_correlation_tree_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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x x' : 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₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) (mx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (mx' : x' ∈ π“˜ u₁) :
                          edist (t.Ο‡ u₁ uβ‚‚ J x) (t.Ο‡ u₁ uβ‚‚ J x') * β€–Complex.exp (Complex.I * ↑((𝒬 u₁) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ xβ€–β‚‘ * β€–Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) fβ‚‚ xβ€–β‚‘ ≀ ↑(C7_5_2 a) * ↑(C7_5_9s a) * ↑(C7_5_10 a) * t.P7_5_4 u₁ uβ‚‚ f₁ fβ‚‚ J * (edist x x' / ↑(defaultD a) ^ s J)
                          source
                          theorem TileStructure.Forest.holder_correlation_tree_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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x x' : 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₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) (mx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (mx' : x' ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                          ↑(t.Ο‡ u₁ uβ‚‚ J x') * edist (Complex.exp (Complex.I * ↑((𝒬 u₁) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ x) (Complex.exp (Complex.I * ↑((𝒬 u₁) x')) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ x') * β€–Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) fβ‚‚ xβ€–β‚‘ ≀ ↑(C7_5_9d a) * ↑(C7_5_10 a) * t.P7_5_4 u₁ uβ‚‚ f₁ fβ‚‚ J * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹
                          source
                          theorem TileStructure.Forest.holder_correlation_tree_3 {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} {x x' : 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₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) (mx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (mx' : x' ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                          ↑(t.Ο‡ u₁ uβ‚‚ J x') * β€–Complex.exp (Complex.I * ↑((𝒬 u₁) x')) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ x'β€–β‚‘ * edist (Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) fβ‚‚ x) (Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x')) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) fβ‚‚ x') ≀ ↑(C7_5_9s a) * ↑(C7_5_9d a) * t.P7_5_4 u₁ uβ‚‚ f₁ fβ‚‚ J * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹
                          source
                          def TileStructure.Forest.I7_5_4 (a : β„•) :
                          NNReal

                          An intermediate constant in Lemma 7.5.4.

                          Equations
                          Instances For
                            source
                            theorem TileStructure.Forest.le_I7_5_4 {a : β„•} (ha : 4 ≀ a) :
                            32 * C7_5_2 a * C7_5_9s a * C7_5_10 a + C7_5_9d a * C7_5_10 a + C7_5_9s a * C7_5_9d a ≀ I7_5_4 a
                            source
                            theorem TileStructure.Forest.edist_holderFunction_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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x x' : 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₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) (mx : x ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) (mx' : x' ∈ Metric.ball (c J) (16 * ↑(defaultD a) ^ s J)) :
                            edist (t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J x) (t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J x') ≀ ↑(I7_5_4 a) * t.P7_5_4 u₁ uβ‚‚ f₁ fβ‚‚ J * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹
                            source
                            theorem TileStructure.Forest.C7_5_4_def (a : β„•) :
                            C7_5_4 a = 2 ^ ((4 * 𝕔 + 10 + 3 * (𝕔 / 4)) * a ^ 3)
                            source
                            @[irreducible]
                            def TileStructure.Forest.C7_5_4 (a : β„•) :
                            NNReal

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

                            Equations
                            Instances For
                              source
                              theorem TileStructure.Forest.le_C7_5_4 {a : β„•} (ha : 4 ≀ a) :
                              C7_5_9s a * C7_5_10 a + 16 ^ defaultΟ„ a * I7_5_4 a ≀ C7_5_4 a
                              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 : 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₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) :
                              iHolENorm (t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J) (c J) (16 * ↑(defaultD a) ^ s J) (defaultΟ„ a) ≀ ↑(C7_5_4 a) * t.P7_5_4 u₁ uβ‚‚ f₁ fβ‚‚ 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 : β„•) :
                                C7_5_11 a n = 2 ^ (↑(defaultZ a) * ↑n / 2 - (2 * ↑𝕔 + 1) * ↑a ^ 3)
                                source
                                theorem TileStructure.Forest.C7_5_11_binomial_bound {a n : β„•} (a4 : 4 ≀ a) :
                                (1 + ↑(C7_5_11 a n)) ^ (-(2 * ↑a ^ 2 + ↑a ^ 3)⁻¹) ≀ 2 ^ (𝕔 / 4 * a ^ 3 + 7) * 2 ^ (-(↑(defaultZ a) * ↑n) / (4 * ↑a ^ 2 + 2 * ↑a ^ 3))

                                A binomial bound used in Lemma 7.4.5.

                                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 : 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β‚‚) :
                                ↑(C7_5_11 a n) ≀ dist_{c J, 8 * ↑(defaultD a) ^ s J} (𝒬 u₁) (𝒬 uβ‚‚)

                                Lemma 7.5.11

                                source
                                theorem TileStructure.Forest.cdtp_le_iHolENorm {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β‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) :
                                β€–βˆ« (x : X), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) fβ‚‚ x)β€–β‚‘ ≀ βˆ‘ J ∈ (t.𝓙₅ u₁ uβ‚‚).toFinset, ↑(C2_0_5 ↑a) * MeasureTheory.volume (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) * iHolENorm (t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J) (c J) (2 * (8 * ↑(defaultD a) ^ s J)) (defaultΟ„ a) * (1 + edist_{c J, 8 * ↑(defaultD a) ^ s J} (𝒬 uβ‚‚) (𝒬 u₁)) ^ (-(2 * ↑a ^ 2 + ↑a ^ 3)⁻¹)
                                source
                                theorem TileStructure.Forest.C7_4_5_def (a n : β„•) :
                                C7_4_5 a n = 2 ^ ((4 * 𝕔 + 11 + 4 * (𝕔 / 4)) * a ^ 3) * 2 ^ (-(↑(defaultZ a) * ↑n) / (4 * ↑a ^ 2 + 2 * ↑a ^ 3))
                                source
                                @[irreducible]
                                def TileStructure.Forest.C7_4_5 (a n : β„•) :
                                NNReal

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

                                Equations
                                Instances For
                                  source
                                  theorem TileStructure.Forest.le_C7_4_5 {a n : β„•} (a4 : 4 ≀ a) :
                                  C2_0_5 ↑a * C7_5_4 a * 2 ^ (𝕔 / 4 * a ^ 3 + 7 + 6 * a) * 2 ^ (-(↑(defaultZ a) * ↑n) / (4 * ↑a ^ 2 + 2 * ↑a ^ 3)) ≀ C7_4_5 a n
                                  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 : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f₁ fβ‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) :
                                  β€–βˆ« (x : X), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) fβ‚‚ x)β€–β‚‘ ≀ ↑(C7_4_5 a n) * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁)).indicator (t.adjointBoundaryOperator u₁ f₁) x) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁)).indicator (t.adjointBoundaryOperator uβ‚‚ fβ‚‚) x) 2 MeasureTheory.volume

                                  Lemma 7.4.5