Documentation

Carleson.ForestOperator.Forests

Lemma 7.4.4 #

source
theorem TileStructure.Forest.estimate_C7_4_5 {a : β„•} (n : β„•) (ha : 4 ≀ a) :
C7_4_5 a n ≀ 2 ^ ((4 * 𝕔 + 11 + 4 * (𝕔 / 4)) * a ^ 3) * 2 ^ (-(4 * ↑n))
source
theorem TileStructure.Forest.estimate_C7_4_6 {a : β„•} (n : β„•) (ha : 4 ≀ a) :
C7_4_6 a n ≀ 2 ^ ((2 * 𝕔 + 9 + 𝕔 / 4) * a ^ 3) * 2 ^ (-(4 * ↑n))
source
@[irreducible]
def TileStructure.Forest.C7_4_4 (a n : β„•) :
NNReal

The constant used in correlation_separated_trees. Has value 2 ^ (512 * a ^ 3 - 4 * n) in the blueprint.

Equations
Instances For
    source
    theorem TileStructure.Forest.C7_4_4_def (a n : β„•) :
    C7_4_4 a n = 2 ^ ((4 * 𝕔 + 12 + 4 * (𝕔 / 4)) * a ^ 3) * 2 ^ (-(4 * ↑n))
    source
    theorem TileStructure.Forest.le_C7_4_4 {a n : β„•} (ha : 4 ≀ a) :
    C7_4_5 a n + C7_4_6 a n ≀ C7_4_4 a n
    source
    theorem TileStructure.Forest.correlation_separated_trees_of_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₁ uβ‚‚ : 𝔓 X} {g₁ gβ‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hg₁ : MeasureTheory.BoundedCompactSupport g₁ MeasureTheory.volume) (hgβ‚‚ : MeasureTheory.BoundedCompactSupport gβ‚‚ MeasureTheory.volume) :
    β€–βˆ« (x : X), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) gβ‚‚ x)β€–β‚‘ ≀ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator u₁ g₁) x) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x) 2 MeasureTheory.volume
    source
    theorem TileStructure.Forest.cst_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)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {g₁ gβ‚‚ : X β†’ β„‚} (hd : Disjoint ↑(π“˜ u₁) ↑(π“˜ uβ‚‚)) (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (x : X) :
    adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) gβ‚‚ x) = 0
    source
    theorem TileStructure.Forest.correlation_separated_trees {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} {g₁ gβ‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (hg₁ : MeasureTheory.BoundedCompactSupport g₁ MeasureTheory.volume) (hgβ‚‚ : MeasureTheory.BoundedCompactSupport gβ‚‚ MeasureTheory.volume) :
    β€–βˆ« (x : X), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) gβ‚‚ x)β€–β‚‘ ≀ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator u₁ g₁) x) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x) 2 MeasureTheory.volume

    Lemma 7.4.4

    Section 7.7 #

    source
    def TileStructure.Forest.rowDecomp_zornset {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)] (s : Set (𝔓 X)) :
    Set (Set (𝔓 X))
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TileStructure.Forest.mem_rowDecomp_zornset_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)] (s s' : Set (𝔓 X)) :
      s' ∈ rowDecomp_zornset s ↔ s' βŠ† s ∧ (s'.PairwiseDisjoint fun (x : 𝔓 X) => ↑(π“˜ x)) ∧ βˆ€ u ∈ s', Maximal (fun (x : Grid X) => x ∈ π“˜ '' s) (π“˜ u)
      source
      theorem TileStructure.Forest.rowDecomp_zornset_chain_Union_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)] (s' : Set (𝔓 X)) {c : Set (Set (𝔓 X))} (hc : c βŠ† rowDecomp_zornset s') (hc_chain : IsChain (fun (x1 x2 : Set (𝔓 X)) => x1 βŠ† x2) c) :
      ⋃ s ∈ c, s ∈ rowDecomp_zornset s' ∧ βˆ€ s ∈ c, s βŠ† ⋃ s'' ∈ c, s''
      source
      @[irreducible]
      def TileStructure.Forest.rowDecomp_π”˜ {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) (j : β„•) :
      Set (𝔓 X)
      Equations
      Instances For
        source
        theorem TileStructure.Forest.rowDecomp_π”˜_def {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) (j : β„•) :
        Maximal (fun (x : Set (𝔓 X)) => x ∈ rowDecomp_zornset (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i)) (t.rowDecomp_π”˜ j)
        source
        theorem TileStructure.Forest.rowDecomp_π”˜_mem_zornset {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) (j : β„•) :
        t.rowDecomp_π”˜ j ∈ rowDecomp_zornset (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i)
        source
        theorem TileStructure.Forest.rowDecomp_π”˜_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) (j : β„•) :
        t.rowDecomp_π”˜ j βŠ† t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i
        source
        theorem TileStructure.Forest.rowDecomp_π”˜_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) (j : β„•) :
        (t.rowDecomp_π”˜ j).PairwiseDisjoint fun (x : 𝔓 X) => ↑(π“˜ x)
        source
        theorem TileStructure.Forest.mem_rowDecomp_π”˜_maximal {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) (j : β„•) (x : 𝔓 X) :
        x ∈ t.rowDecomp_π”˜ j β†’ Maximal (fun (x : Grid X) => x ∈ π“˜ '' (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), t.rowDecomp_π”˜ i)) (π“˜ x)
        source
        theorem TileStructure.Forest.rowDecomp_π”˜_subset_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) (j : β„•) :
        t.rowDecomp_π”˜ j βŠ† t.π”˜
        source
        def TileStructure.Forest.rowDecomp {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) (j : β„•) :
        Row X n

        The row-decomposition of a tree, defined in the proof of Lemma 7.7.1. The indexing is off-by-one compared to the blueprint.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem TileStructure.Forest.mem_forest_of_mem {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} {j : β„•} {x : 𝔓 X} (hx : x ∈ t.rowDecomp j) :
          x ∈ t
          source
          theorem TileStructure.Forest.rowDecomp_π”˜_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) (j : β„•) :
          (t.rowDecomp j).π”˜ = t.rowDecomp_π”˜ j
          source
          theorem TileStructure.Forest.mem_rowDecomp_iff_mem_rowDecomp_π”˜ {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) (j : β„•) (x : 𝔓 X) :
          x ∈ t.rowDecomp j ↔ x ∈ t.rowDecomp_π”˜ j
          source
          theorem TileStructure.Forest.stackSize_remainder_ge_one_of_exists {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) (j : β„•) (x : X) (hx : βˆƒ 𝔲' ∈ (t.rowDecomp j).π”˜, x ∈ π“˜ 𝔲') :
          1 ≀ stackSize ((t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), (t.rowDecomp i).π”˜) ∩ (t.rowDecomp j).π”˜) x
          source
          theorem TileStructure.Forest.remainder_stackSize_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) (j : β„•) (x : X) :
          stackSize (t.π”˜ \ ⋃ (i : β„•), ⋃ (_ : i < j), (t.rowDecomp i).π”˜) x ≀ 2 ^ n - j
          source
          @[simp]
          theorem TileStructure.Forest.biUnion_rowDecomp {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} :
          ⋃ (j : β„•), ⋃ (_ : j < 2 ^ n), (t.rowDecomp j).π”˜ = t.π”˜

          Part of Lemma 7.7.1

          source
          theorem TileStructure.Forest.pairwiseDisjoint_rowDecomp {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} :
          (Set.Iio (2 ^ n)).PairwiseDisjoint fun (x : β„•) => (t.rowDecomp x).π”˜

          Part of Lemma 7.7.1

          source
          @[simp]
          theorem TileStructure.Forest.rowDecomp_apply {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 j : β„•} {t : Forest X n} {u : 𝔓 X} :
          (fun (x : 𝔓 X) => (t.rowDecomp j).𝔗 x) u = (fun (x : 𝔓 X) => t.𝔗 x) u
          source
          def TileStructure.Forest.carlesonRowSum {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) (j : β„•) (f : X β†’ β„‚) (x : X) :
          β„‚

          The definition of T_{β„œ_j}f(x), defined above Lemma 7.7.2.

          Equations
          Instances For
            source
            def TileStructure.Forest.adjointCarlesonRowSum {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) (j : β„•) (f : X β†’ β„‚) (x : X) :
            β„‚

            The definition of T_{β„œ_j}*f(x), defined above Lemma 7.7.2.

            Equations
            Instances For
              source
              theorem TileStructure.Forest.adjointCarlesonRowSum_adjoint {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} {f g : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (j : β„•) :
              ∫ (x : X), (starRingEnd β„‚) (g x) * t.carlesonRowSum j f x = ∫ (x : X), (starRingEnd β„‚) (t.adjointCarlesonRowSum j g x) * f x

              adjointCarlesonRowSum is the adjoint of carlesonRowSum.

              source
              theorem TileStructure.Forest.row_bound_common {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 j : β„•} {t : Forest X n} {g : X β†’ β„‚} (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) {A : Set X} (mA : MeasurableSet A) {C : ENNReal} (hC : βˆ€ u ∈ t.rowDecomp j, MeasureTheory.eLpNorm (A.indicator (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) ((↑(π“˜ u)).indicator g))) 2 MeasureTheory.volume ≀ C * MeasureTheory.eLpNorm ((↑(π“˜ u)).indicator g) 2 MeasureTheory.volume) :
              MeasureTheory.eLpNorm (A.indicator (t.adjointCarlesonRowSum j g)) 2 MeasureTheory.volume ≀ C * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

              Common proof structure for the two parts of Lemma 7.7.2.

              source
              theorem TileStructure.Forest.C7_7_2_1_def (a n : β„•) :
              C7_7_2_1 a n = 2 ^ ((𝕔 + 7 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3) * 2 ^ (-(↑n / 2))
              source
              @[irreducible]
              def TileStructure.Forest.C7_7_2_1 (a n : β„•) :
              NNReal

              The constant used in row_bound. Has value 2 ^ (182 * a ^ 3 - n / 2) in the blueprint.

              Equations
              Instances For
                source
                theorem TileStructure.Forest.le_C7_7_2_1 {a n : β„•} (a4 : 4 ≀ a) :
                C7_3_1_1 a * (2 ^ (4 * ↑a - ↑n + 1)) ^ 2⁻¹ ≀ C7_7_2_1 a n
                source
                theorem TileStructure.Forest.C7_7_2_2_def (a n : β„•) :
                C7_7_2_2 a n = 2 ^ ((2 * 𝕔 + 8 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3) * 2 ^ (-(↑n / 2))
                source
                @[irreducible]
                def TileStructure.Forest.C7_7_2_2 (a n : β„•) :
                NNReal

                The constant used in indicator_row_bound. Has value 2 ^ (283 * a ^ 3 - n / 2) in the blueprint.

                Equations
                Instances For
                  source
                  theorem TileStructure.Forest.le_C7_7_2_2 {a n : β„•} (a4 : 4 ≀ a) :
                  C7_3_1_2 a * (2 ^ (4 * ↑a - ↑n + 1)) ^ 2⁻¹ ≀ C7_7_2_2 a n
                  source
                  theorem TileStructure.Forest.row_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 j : β„•} {t : Forest X n} {g : X β†’ β„‚} (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (h2g : Function.support g βŠ† G) :
                  MeasureTheory.eLpNorm (t.adjointCarlesonRowSum j g) 2 MeasureTheory.volume ≀ ↑(C7_7_2_1 a n) * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
                  source
                  theorem TileStructure.Forest.indicator_row_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 j : β„•} {t : Forest X n} {g : X β†’ β„‚} (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (h2g : Function.support g βŠ† G) :
                  MeasureTheory.eLpNorm (F.indicator (t.adjointCarlesonRowSum j g)) 2 MeasureTheory.volume ≀ ↑(C7_7_2_2 a n) * densβ‚‚ (⋃ u ∈ t, (fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
                  source
                  theorem TileStructure.Forest.row_correlation_aux {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 j j' : β„•} {t : Forest X n} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (nf : Function.support f βŠ† G) :
                  (βˆ‘ u : 𝔓 X with u ∈ t.rowDecomp j, βˆ‘ u' : 𝔓 X with u' ∈ t.rowDecomp j', MeasureTheory.eLpNorm (fun (x : X) => (↑(π“˜ u) ∩ ↑(π“˜ u')).indicator (t.adjointBoundaryOperator u ((↑(π“˜ u)).indicator f)) x) 2 MeasureTheory.volume ^ 2) ^ 2⁻¹ ≀ ↑(C7_4_3 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume
                  source
                  @[irreducible]
                  def TileStructure.Forest.C7_7_3 (a n : β„•) :
                  NNReal

                  The constant used in row_correlation. Has value 2 ^ (876 * a ^ 3 - 4 * n) in the blueprint.

                  Equations
                  Instances For
                    source
                    theorem TileStructure.Forest.C7_7_3_def (a n : β„•) :
                    C7_7_3 a n = C7_4_3 a ^ 2 * C7_4_4 a n
                    source
                    theorem TileStructure.Forest.row_correlation {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 j j' : β„•} {t : Forest X n} {f₁ fβ‚‚ : X β†’ β„‚} (lj : j < 2 ^ n) (lj' : j' < 2 ^ n) (hn : j β‰  j') (hf₁ : MeasureTheory.BoundedCompactSupport f₁ MeasureTheory.volume) (nf₁ : Function.support f₁ βŠ† G) (hfβ‚‚ : MeasureTheory.BoundedCompactSupport fβ‚‚ MeasureTheory.volume) (nfβ‚‚ : Function.support fβ‚‚ βŠ† G) :
                    β€–βˆ« (x : X), t.adjointCarlesonRowSum j f₁ x * (starRingEnd β„‚) (t.adjointCarlesonRowSum j' fβ‚‚ x)β€–β‚‘ ≀ ↑(C7_7_3 a n) * MeasureTheory.eLpNorm f₁ 2 MeasureTheory.volume * MeasureTheory.eLpNorm fβ‚‚ 2 MeasureTheory.volume

                    Lemma 7.7.3.

                    source
                    def TileStructure.Forest.rowSupport {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) (j : β„•) :
                    Set X

                    The definition of Eβ±Ό defined above Lemma 7.7.4.

                    Equations
                    Instances For
                      source
                      theorem TileStructure.Forest.disjoint_impl {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 p' : 𝔓 X} :
                      Disjoint (Ξ© p) (Ξ© p') β†’ Disjoint (E p) (E p')
                      source
                      theorem TileStructure.Forest.disjoint_of_ne_of_mem {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} {i j : β„•} {u u' : 𝔓 X} (hne : u β‰  u') (hu : u ∈ t.rowDecomp i) (hu' : u' ∈ t.rowDecomp j) {p p' : 𝔓 X} (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hp' : p' ∈ (fun (x : 𝔓 X) => t.𝔗 x) u') :
                      Disjoint (E p) (E p')
                      source
                      theorem TileStructure.Forest.measurableSet_rowSupport {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 j : β„•} {t : Forest X n} :
                      MeasurableSet (t.rowSupport j)
                      source
                      theorem TileStructure.Forest.pairwiseDisjoint_rowSupport {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} :
                      (Set.Iio (2 ^ n)).PairwiseDisjoint t.rowSupport

                      Lemma 7.7.4

                      source
                      theorem TileStructure.Forest.forest_operator_g_prelude {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} {f g : X β†’ β„‚} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hg : Measurable g) (h2g : βˆ€ (x : X), β€–g xβ€– ≀ G.indicator 1 x) :
                      β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * βˆ‘ u : 𝔓 X with u ∈ t, carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f xβ€–β‚‘ ≀ MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => βˆ‘ u : 𝔓 X with u ∈ t, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) g x) 2 MeasureTheory.volume
                      source
                      theorem TileStructure.Forest.adjointCarlesonRowSum_rowSupport {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 j : β„•} {t : Forest X n} {f : X β†’ β„‚} :
                      t.adjointCarlesonRowSum j f = t.adjointCarlesonRowSum j ((t.rowSupport j).indicator f)
                      source
                      def TileStructure.Forest.G2_0_4 (a n : β„•) :
                      NNReal

                      The constant on the g side of Proposition 2.0.4. Has value 2 ^ (440 * a ^ 3) in the blueprint.

                      Equations
                      Instances For
                        source
                        theorem TileStructure.Forest.le_sq_G2_0_4 {a n : β„•} (a4 : 4 ≀ a) :
                        C7_7_2_1 a n ^ 2 + C7_7_3 a n * 2 ^ n ≀ G2_0_4 a n ^ 2
                        source
                        theorem TileStructure.Forest.support_subset_of_norm_le_indicator {X : Type u_1} {f : X β†’ β„‚} {g : X β†’ ℝ} {A : Set X} (h2f : βˆ€ (x : X), β€–f xβ€– ≀ A.indicator g x) :
                        Function.support f βŠ† A
                        source
                        theorem TileStructure.Forest.forest_operator_g_main {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} {g : X β†’ β„‚} (hg : Measurable g) (h2g : βˆ€ (x : X), β€–g xβ€– ≀ G.indicator 1 x) :
                        MeasureTheory.eLpNorm (fun (x : X) => βˆ‘ u : 𝔓 X with u ∈ t, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) g x) 2 MeasureTheory.volume ^ 2 ≀ (↑(G2_0_4 a n) * MeasureTheory.eLpNorm g 2 MeasureTheory.volume) ^ 2
                        source
                        theorem TileStructure.Forest.forest_operator_g {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 : β„•} {f g : X β†’ β„‚} (t : Forest X n) (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hg : Measurable g) (h2g : βˆ€ (x : X), β€–g xβ€– ≀ G.indicator 1 x) :
                        β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * βˆ‘ u : 𝔓 X with u ∈ t, carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f xβ€–β‚‘ ≀ ↑(G2_0_4 a n) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

                        The g side of Proposition 2.0.4.

                        source
                        theorem TileStructure.Forest.carlesonRowSum_rowSupport {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 j : β„•} {t : Forest X n} {f : X β†’ β„‚} :
                        t.carlesonRowSum j f = (t.rowSupport j).indicator (t.carlesonRowSum j f)
                        source
                        theorem TileStructure.Forest.forest_operator_f_prelude {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} {f g : X β†’ β„‚} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hg : Measurable g) (h2g : βˆ€ (x : X), β€–g xβ€– ≀ G.indicator 1 x) :
                        β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * βˆ‘ u : 𝔓 X with u ∈ t, carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f xβ€–β‚‘ ≀ MeasureTheory.eLpNorm g 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => G.indicator (fun (x : X) => βˆ‘ u : 𝔓 X with u ∈ t, carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f x) x) 2 MeasureTheory.volume
                        source
                        theorem TileStructure.Forest.forest_operator_f_inner {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 j : β„•} {t : Forest X n} {f : X β†’ β„‚} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) :
                        MeasureTheory.eLpNorm (G.indicator (t.carlesonRowSum j f)) 2 MeasureTheory.volume ≀ ↑(C7_7_2_2 a n) * densβ‚‚ (⋃ u ∈ t, (fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

                        https://leanprover.zulipchat.com/#narrow/channel/442935-Carleson/topic/Problems.20in.20the.20forest.20operator.20proposition/near/522771057

                        source
                        def TileStructure.Forest.C2_0_4_aux (a : β„•) :
                        NNReal

                        The constant in the f side of Proposition 2.0.4. Has value 2 ^ (283 * a ^ 3) in the blueprint.

                        Equations
                        Instances For
                          source
                          theorem TileStructure.Forest.forest_operator_f_main {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} {f : X β†’ β„‚} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) :
                          MeasureTheory.eLpNorm (fun (x : X) => G.indicator (fun (x : X) => βˆ‘ u : 𝔓 X with u ∈ t, carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f x) x) 2 MeasureTheory.volume ^ 2 ≀ (↑(C2_0_4_aux a) * densβ‚‚ (⋃ u ∈ t, (fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume) ^ 2
                          source
                          theorem TileStructure.Forest.forest_operator_f {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 : β„•} {f g : X β†’ β„‚} (t : Forest X n) (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hg : Measurable g) (h2g : βˆ€ (x : X), β€–g xβ€– ≀ G.indicator 1 x) :
                          β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * βˆ‘ u : 𝔓 X with u ∈ t, carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f xβ€–β‚‘ ≀ ↑(C2_0_4_aux a) * densβ‚‚ (⋃ u ∈ t, (fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

                          The f side of Proposition 2.0.4.

                          Proposition 2.0.4 #

                          source
                          theorem C2_0_4_base_def (a : β„•) :
                          C2_0_4_base a = 2 ^ ((3 * 𝕔 + 15 + 5 * (𝕔 / 4)) * a ^ 3)
                          source
                          @[irreducible]
                          def C2_0_4_base (a : β„•) :
                          NNReal
                          Equations
                          Instances For
                            source
                            @[irreducible]
                            def C2_0_4 (a : β„•) (q : ℝ) (n : β„•) :
                            NNReal

                            The constant used in forest_operator. Has value 2 ^ (440 * a ^ 3 - (q - 1) / q * n) in the blueprint.

                            Equations
                            Instances For
                              source
                              theorem C2_0_4_def (a : β„•) (q : ℝ) (n : β„•) :
                              C2_0_4 a q n = C2_0_4_base a * 2 ^ (-(q - 1) / q * ↑n)
                              source
                              theorem forest_operator {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 : β„•} (𝔉 : TileStructure.Forest X n) {f g : X β†’ β„‚} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hg : Measurable g) (h2g : βˆ€ (x : X), β€–g xβ€– ≀ G.indicator 1 x) :
                              β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * βˆ‘ u : 𝔓 X with u ∈ 𝔉, carlesonSum ((fun (x : 𝔓 X) => 𝔉.𝔗 x) u) f xβ€–β‚‘ ≀ ↑(C2_0_4 a q n) * densβ‚‚ (⋃ u ∈ 𝔉, (fun (x : 𝔓 X) => 𝔉.𝔗 x) u) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
                              source
                              theorem forest_operator' {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 : β„•} (𝔉 : TileStructure.Forest X n) {f : X β†’ β„‚} {A : Set X} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hA : MeasurableSet A) (sA : A βŠ† G) :
                              ∫⁻ (x : X) in A, β€–βˆ‘ u : 𝔓 X with u ∈ 𝔉, carlesonSum ((fun (x : 𝔓 X) => 𝔉.𝔗 x) u) f xβ€–β‚‘ ≀ ↑(C2_0_4 a q n) * densβ‚‚ (⋃ u ∈ 𝔉, (fun (x : 𝔓 X) => 𝔉.𝔗 x) u) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.volume A ^ (1 / 2)

                              Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.

                              source
                              theorem forest_operator_le_volume {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 : β„•} (𝔉 : TileStructure.Forest X n) {f : X β†’ β„‚} {A : Set X} (hf : Measurable f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hA : MeasurableSet A) (sA : A βŠ† G) :
                              ∫⁻ (x : X) in A, β€–βˆ‘ u : 𝔓 X with u ∈ 𝔉, carlesonSum ((fun (x : 𝔓 X) => 𝔉.𝔗 x) u) f xβ€–β‚‘ ≀ ↑(C2_0_4 a q n) * densβ‚‚ (⋃ u ∈ 𝔉, (fun (x : 𝔓 X) => 𝔉.𝔗 x) u) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.volume F ^ (1 / 2) * MeasureTheory.volume A ^ (1 / 2)

                              Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function, and with the upper bound in terms of volume F and volume G.