Documentation

Carleson.ForestOperator.Forests

Lemmas 7.4.4 #

source
theorem TileStructure.Forest.C7_4_4_def (a n : β„•) :
C7_4_4 a n = 2 ^ (550 * ↑a ^ 3 - 3 * ↑n)
source
@[irreducible]
def TileStructure.Forest.C7_4_4 (a n : β„•) :
NNReal

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

Equations
Instances For
    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} {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β‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x).toReal) 2 MeasureTheory.volume
    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} {f₁ fβ‚‚ g₁ gβ‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : 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β‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁) ∩ ↑(π“˜ uβ‚‚)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x).toReal) 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.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) (this : βˆƒ 𝔲' ∈ (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
          @[irreducible]
          def TileStructure.Forest.C7_7_2_1 (a n : β„•) :
          NNReal

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

          Equations
          Instances For
            source
            theorem TileStructure.Forest.C7_7_2_1_def (a n : β„•) :
            C7_7_2_1 a n = 2 ^ (156 * ↑a ^ 3 - ↑n / 2)
            source
            @[irreducible]
            def TileStructure.Forest.C7_7_2_2 (a n : β„•) :
            NNReal

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

            Equations
            Instances For
              source
              theorem TileStructure.Forest.C7_7_2_2_def (a n : β„•) :
              C7_7_2_2 a n = 2 ^ (257 * ↑a ^ 3 - ↑n / 2)
              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} {f : X β†’ β„‚} (hj : j < 2 ^ n) (hg : MeasureTheory.BoundedCompactSupport f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ G.indicator 1 x) :
              MeasureTheory.eLpNorm (βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f) 2 MeasureTheory.volume ≀ ↑(C7_7_2_1 a n) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

              Part of Lemma 7.7.2.

              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} {u : 𝔓 X} {f : X β†’ β„‚} (hj : j < 2 ^ n) (hf : MeasureTheory.BoundedCompactSupport f) (h2f : βˆ€ (x : X), β€–f xβ€– ≀ G.indicator 1 x) :
              MeasureTheory.eLpNorm ((βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, F.indicator) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) 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

              Part of Lemma 7.7.2.

              source
              theorem TileStructure.Forest.C7_7_3_def (a n : β„•) :
              C7_7_3 a n = 2 ^ (862 * ↑a ^ 3 - 2 * ↑n)
              source
              @[irreducible]
              def TileStructure.Forest.C7_7_3 (a n : β„•) :
              NNReal

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

              Equations
              Instances For
                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 β†’ β„‚} (hjj' : j < j') (hj' : j' < 2 ^ n) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (h3f₁ : βˆ€ (x : X), β€–f₁ xβ€– ≀ G.indicator 1 x) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) (h3fβ‚‚ : βˆ€ (x : X), β€–fβ‚‚ xβ€– ≀ G.indicator 1 x) :
                β†‘β€–βˆ« (x : X), (βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f₁ x) * βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j') Finset.univ, adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) 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.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

                  Proposition 2.0.4 #

                  source
                  theorem C2_0_4_base_def (a : ℝ) :
                  C2_0_4_base a = 2 ^ (432 * a ^ 3)
                  source
                  @[irreducible]
                  def C2_0_4_base (a : ℝ) :
                  NNReal
                  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
                    @[irreducible]
                    def C2_0_4 (a q : ℝ) (n : β„•) :
                    NNReal

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

                    Equations
                    Instances For
                      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 : Bornology.IsBounded (Function.support g)) :
                      β†‘β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ 𝔉) Finset.univ, 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) (h'A : Bornology.IsBounded A) :
                      ∫⁻ (x : X) in A, β†‘β€–βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ 𝔉) Finset.univ, 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) (h'A : Bornology.IsBounded A) :
                      ∫⁻ (x : X) in A, β†‘β€–βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ 𝔉) Finset.univ, 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.