Documentation

Carleson.ForestOperator.RemainingTiles

Section 7.6 and Lemma 7.4.6 #

source
def TileStructure.Forest.𝓙₆ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : Forest X n) (u₁ : 𝔓 X) :
Set (Grid X)

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

Equations
Instances For
    source
    theorem TileStructure.Forest.union_𝓙₆ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ : 𝔓 X} (hu₁ : u₁ ∈ t) :
    ⋃ J ∈ t.𝓙₆ u₁, ↑J = ↑(π“˜ u₁)

    Part of Lemma 7.6.1.

    source
    theorem TileStructure.Forest.pairwiseDisjoint_𝓙₆ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ : 𝔓 X} :
    (t.𝓙₆ u₁).PairwiseDisjoint fun (I : Grid X) => ↑I

    Part of Lemma 7.6.1.

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

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

    Equations
    Instances For
      source
      theorem TileStructure.Forest.C7_6_3_def (a n : β„•) :
      C7_6_3 a n = ↑(defaultZ a) * ↑n / ((2 * ↑𝕔 + 2) * ↑a ^ 3) - 2
      source
      theorem TileStructure.Forest.nonneg_C7_6_3_add_two {a n : β„•} :
      0 ≀ C7_6_3 a n + 2
      source
      theorem TileStructure.Forest.thin_scale_impact_prelims {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ p : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (hJ : J ∈ t.𝓙₆ u₁) (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) (h : ↑(s J) - C7_6_3 a n < ↑(𝔰 p)) :
      dist (𝔠 p) (c J) < 16 * ↑(defaultD a) ^ (↑(𝔰 p) + C7_6_3 a n + 2) ∧ βˆƒ (J' : Grid X), J < J' ∧ s J' = s J + 1 ∧ βˆƒ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u₁, ↑(π“˜ p) βŠ† Metric.ball (c J') (100 * ↑(defaultD a) ^ (s J' + 1))

      Some preliminary relations for Lemma 7.6.3.

      source
      theorem TileStructure.Forest.thin_scale_impact_key {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₆ u₁) (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) (h : ↑(s J) - C7_6_3 a n < ↑(𝔰 p)) :
      2 ^ (defaultZ a * (n + 1) - 1) < 2 ^ (↑a * (↑𝕔 * ↑a ^ 2 * (C7_6_3 a n + 2 + 1) + 9)) * 2 ^ (↑(defaultZ a) * ↑n / 2)

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

      source
      theorem TileStructure.Forest.thin_scale_impact {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₆ u₁) (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) :
      ↑(𝔰 p) ≀ ↑(s J) - C7_6_3 a n

      Lemma 7.6.3.

      source
      theorem TileStructure.Forest.thin_scale_impact' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₆ u₁) (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) :
      𝔰 p ≀ s J - ⌊C7_6_3 a nβŒ‹

      Lemma 7.6.3 with a floor on the constant to avoid casting.

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

      The constant used in square_function_count.

      Equations
      Instances For
        source
        theorem TileStructure.Forest.C7_6_4_def (a : β„•) (s : β„€) :
        C7_6_4 a s = 2 ^ (14 * ↑a + 1) * (8 * ↑(defaultD a) ^ (-s)) ^ defaultΞΊ a
        source
        theorem TileStructure.Forest.square_function_count {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ : 𝔓 X} {J : Grid X} (hJ : J ∈ t.𝓙₆ u₁) {s' : β„€} :
        ⨍⁻ (x : X) in ↑J, (βˆ‘ I : Grid X with s I = s J - s' ∧ Disjoint ↑I ↑(π“˜ u₁) ∧ Β¬Disjoint (↑J) (Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)), (Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)).indicator 1 x) ^ 2 βˆ‚MeasureTheory.volume ≀ ↑(C7_6_4 a s')

        Lemma 7.6.4.

        source
        theorem TileStructure.Forest.sum_𝓙₆_indicator_sq_eq {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} {f : Grid X β†’ X β†’ ENNReal} :
        (βˆ‘ J ∈ (t.𝓙₆ u₁).toFinset, (↑J).indicator (f J) x) ^ 2 = βˆ‘ J ∈ (t.𝓙₆ u₁).toFinset, (↑J).indicator (fun (x : X) => f J x ^ 2) x
        source
        theorem TileStructure.Forest.btp_expansion {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 β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) :
        MeasureTheory.eLpNorm (approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–) 2 MeasureTheory.volume = (βˆ‘ J ∈ (t.𝓙₆ u₁).toFinset, (MeasureTheory.volume ↑J)⁻¹ * (∫⁻ (y : X) in ↑J, β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f yβ€–β‚‘) ^ 2) ^ 2⁻¹
        source
        theorem TileStructure.Forest.e763 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) :
        MeasureTheory.eLpNorm (approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–) 2 MeasureTheory.volume ≀ βˆ‘ k ∈ Finset.Icc ⌊C7_6_3 a nβŒ‹ (2 * ↑(defaultS X)), (βˆ‘ J ∈ (t.𝓙₆ u₁).toFinset, (MeasureTheory.volume ↑J)⁻¹ * (∫⁻ (y : X) in ↑J, βˆ‘ p ∈ ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚).toFinset with Β¬Disjoint (↑J) (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) ∧ 𝔰 p = s J - k, β€–adjointCarleson p f yβ€–β‚‘) ^ 2) ^ 2⁻¹

        Equation (7.6.3) of Lemma 7.6.2.

        source
        theorem TileStructure.Forest.btp_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)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {I J : Grid X} :
        ∫⁻ (y : X) in ↑J, βˆ‘ p ∈ ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚).toFinset with Β¬Disjoint (↑J) (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) ∧ π“˜ p = I, β€–adjointCarleson p f yβ€–β‚‘ ≀ ↑(C2_1_3 a) * 2 ^ (4 * a) * ∫⁻ (y : X) in ↑J, (Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)).indicator 1 y * MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f y

        The critical bound on the integral in Equation (7.6.3). It holds for any cubes I, J.

        source
        theorem TileStructure.Forest.e764_preCS {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) :
        MeasureTheory.eLpNorm (approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–) 2 MeasureTheory.volume ≀ ↑(C2_1_3 a) * 2 ^ (4 * a) * βˆ‘ k ∈ Finset.Icc ⌊C7_6_3 a nβŒ‹ (2 * ↑(defaultS X)), (βˆ‘ J ∈ (t.𝓙₆ u₁).toFinset, (MeasureTheory.volume ↑J)⁻¹ * (βˆ‘ I : Grid X with s I = s J - k ∧ Disjoint ↑I ↑(π“˜ u₁) ∧ Β¬Disjoint (↑J) (Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)), ∫⁻ (y : X) in ↑J, (Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)).indicator 1 y * MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f y) ^ 2) ^ 2⁻¹

        Equation (7.6.4) of Lemma 7.6.2 (before applying Cauchy–Schwarz).

        source
        theorem TileStructure.Forest.e764_postCS {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) :
        MeasureTheory.eLpNorm (approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–) 2 MeasureTheory.volume ≀ (↑(C2_1_3 a) * 2 ^ (11 * a + 2) * βˆ‘ k ∈ Finset.Icc ⌊C7_6_3 a nβŒ‹ (2 * ↑(defaultS X)), ↑(defaultD a) ^ (-↑k * defaultΞΊ a / 2)) * MeasureTheory.eLpNorm ((↑(π“˜ u₁)).indicator fun (x : X) => MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x) 2 MeasureTheory.volume

        Equation (7.6.4) of Lemma 7.6.2 (after applying Cauchy–Schwarz and simplification).

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

        The constant used in bound_for_tree_projection.

        Equations
        Instances For
          source
          theorem TileStructure.Forest.C7_6_2_def (a n : β„•) :
          C7_6_2 a n = C2_1_3 a * 2 ^ (21 * a + 5) * 2 ^ (-(↑𝕔 / ((4 * ↑𝕔 + 4) * ↑a) * ↑(defaultZ a) * ↑n * defaultΞΊ a))
          source
          theorem TileStructure.Forest.btp_constant_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {n : β„•} :
          ↑(C2_1_3 a) * 2 ^ (11 * a + 2) * βˆ‘ k ∈ Finset.Icc ⌊C7_6_3 a nβŒ‹ (2 * ↑(defaultS X)), ↑(defaultD a) ^ (-↑k * defaultΞΊ a / 2) ≀ ↑(C7_6_2 a n)
          source
          theorem TileStructure.Forest.bound_for_tree_projection {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) :
          MeasureTheory.eLpNorm (approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–) 2 MeasureTheory.volume ≀ ↑(C7_6_2 a n) * MeasureTheory.eLpNorm ((↑(π“˜ u₁)).indicator fun (x : X) => MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x) 2 MeasureTheory.volume

          Lemma 7.6.2.

          source
          theorem TileStructure.Forest.cntp_approxOnCube_eq {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {fβ‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) :
          (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u₁)) fun (x : X) => β€–(↑(π“˜ u₁)).indicator (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) fβ‚‚) xβ€–) = approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) fβ‚‚ xβ€–
          source
          @[irreducible]
          def TileStructure.Forest.C7_4_6 (a n : β„•) :
          NNReal

          The constant used in correlation_near_tree_parts. Has value 2 ^ (232 * a ^ 3 + 21 * a + 5- 25/(101a) * Z n ΞΊ) in the blueprint.

          Equations
          Instances For
            source
            theorem TileStructure.Forest.C7_4_6_def (a n : β„•) :
            C7_4_6 a n = C7_2_1 a * C7_6_2 a n
            source
            theorem TileStructure.Forest.correlation_near_tree_parts {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f₁ fβ‚‚ : 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_6 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.6