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
      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
        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_distance_between_centers {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 J' : Grid X} (subset : ↑J βŠ† ↑J') :
          dist (c J) (c J') < 4 * ↑(defaultD a) ^ s J'
          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
          @[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.C7_5_2_def (a : β„•) :
            C7_5_2 a = 2 ^ (226 * ↑a ^ 3)
            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) * ↑(Finset.filter (fun (J' : Grid X) => Β¬Disjoint (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (Metric.ball (c J') (8 * ↑(defaultD a) ^ s J'))) (t.𝓙₅ u₁ uβ‚‚).toFinset).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 ^ (151 * ↑a ^ 3)
            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.ψ_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 ≀ 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.volume_xDsp_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} {x : X} (hx : x ∈ π“˜ p) :
              MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) / 2 ^ (3 * a) ≀ MeasureTheory.volume (Metric.ball x (↑(defaultD a) ^ 𝔰 p))

              This bound is used in both nontrivial cases of Lemma 7.5.5.

              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) (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.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) :
              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
              @[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.Q7_5_5_def (a : β„•) :
                Q7_5_5 a = 10 * 2 ^ (6 * a)
                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) * (↑(nndist 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) (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) :
                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β‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
                ↑(⨆ 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 ∈ Finset.filter (fun (p : 𝔓 X) => 𝔰 p = k ∧ Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))) Finset.univ, ⨆ 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 : Measurable fun (x : X) => β€–f xβ€–β‚‘) :
                ⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarleson p f xβ€–β‚‘ ≀ 2 ^ (103 * 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 ^ (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 : 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), β€–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) (8 * ↑(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) (8 * ↑(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) (8 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) :
                  βˆ‘ p ∈ Finset.filter (fun (p : 𝔓 X) => Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) ∧ 𝔰 p = k) β„­.toFinset, ∫⁻ (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) (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(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
                  @[irreducible]
                  def TileStructure.Forest.C7_5_9d (a : β„•) :
                  NNReal

                  The constant used in global_tree_control1_edist.

                  Equations
                  Instances For
                    source
                    theorem TileStructure.Forest.C7_5_9d_def (a : β„•) :
                    C7_5_9d a = C7_5_5 a * 2 ^ (4 * a + 1)
                    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) (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(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) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(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) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(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 + 2)
                    source
                    @[irreducible]
                    def TileStructure.Forest.C7_5_9s (a : β„•) :
                    NNReal

                    The constant used in global_tree_control1_supbound.

                    Equations
                    Instances For
                      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) :
                      ⨆ x ∈ Metric.ball (c J) (8 * ↑(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
                      theorem TileStructure.Forest.C7_5_10_def (a : β„•) :
                      C7_5_10 a = 2 ^ (155 * ↑a ^ 3)
                      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.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) :
                        ↑(⨆ x ∈ Metric.ball (c J) (8 * ↑(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𝓑 (fun (x : X) => β€–f xβ€–) x

                        Lemma 7.5.10

                        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.C7_5_4_def (a : β„•) :
                          C7_5_4 a = 2 ^ (535 * ↑a ^ 3)
                          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₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) :
                          HolderOnWith (C7_5_4 a * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 (fun (x : X) => β€–f₁ xβ€–) x).toNNReal) * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) fβ‚‚ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 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
                          theorem TileStructure.Forest.C7_5_11_def (a n : β„•) :
                          C7_5_11 a n = 2 ^ (↑(defaultZ a) * ↑n / 2 - 201 * ↑a ^ 3)
                          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.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.C7_4_5_def (a n : β„•) :
                            C7_4_5 a n = 2 ^ (541 * ↑a ^ 3 - ↑(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 ^ (541 * a ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3)) in the blueprint.

                            Equations
                            Instances For
                              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β‚‚ 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_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