Documentation

Carleson.ForestOperator

Section 7.1 and Lemma 7.1.3 #

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

The definition Οƒ(u, x) given in Section 7.1. We may assume u ∈ t whenever proving things about this definition.

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

    The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2

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

      The definition of `𝓙(𝔖), defined above Lemma 7.1.2

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

        The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2

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

          The definition of `𝓛(𝔖), defined above Lemma 7.1.2

          Equations
          Instances For
            source
            def TileStructure.Forest.approxOnCube {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (C : Set (Grid X)) (f : X β†’ E') (x : X) :
            E'

            The projection operator P_𝓒 f(x), given above Lemma 7.1.3. In lemmas the c will be pairwise disjoint on C.

            Equations
            Instances For
              source
              def TileStructure.Forest.cubeOf {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (i : β„€) (x : X) :
              Grid X

              The definition I_i(x), given above Lemma 7.1.3. The cube of scale s that contains x. There is at most 1 such cube, if it exists.

              Equations
              Instances For
                source
                def TileStructure.Forest.nontangentialMaximalFunction {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (ΞΈ : Θ X) (f : X β†’ β„‚) (x : X) :
                ENNReal

                The definition T_𝓝^ΞΈ f(x), given in (7.1.3). For convenience, the suprema are written a bit differently than in the blueprint (avoiding cubeOf), but this should be equivalent. This is 0 if x doesn't lie in a cube.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def TileStructure.Forest.boundaryOperator {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : TileStructure.Forest X n) (u : 𝔓 X) (f : X β†’ β„‚) (x : X) :
                  ENNReal

                  The operator S_{1,𝔲} f(x), given in (7.1.4).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def TileStructure.Forest.𝓑 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                    Set (β„• Γ— Grid X)

                    The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3.

                    Equations
                    Instances For
                      source
                      def TileStructure.Forest.c𝓑 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (z : β„• Γ— Grid X) :
                      X

                      The center function for the collection of balls 𝓑.

                      Equations
                      Instances For
                        source
                        def TileStructure.Forest.r𝓑 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (z : β„• Γ— Grid X) :
                        ℝ

                        The radius function for the collection of balls 𝓑.

                        Equations
                        Instances For
                          source
                          theorem TileStructure.Forest.convex_scales {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {x : X} (hu : u ∈ t) :
                          (↑(t.Οƒ u x)).OrdConnected

                          Lemma 7.1.1, freely translated.

                          source
                          @[simp]
                          theorem TileStructure.Forest.biUnion_𝓙 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔖 : Set (𝔓 X)} :
                          ⋃ J ∈ TileStructure.Forest.𝓙 𝔖, ↑J = ⋃ (I : Grid X), ↑I

                          Part of Lemma 7.1.2

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

                          Part of Lemma 7.1.2

                          source
                          @[simp]
                          theorem TileStructure.Forest.biUnion_𝓛 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔖 : Set (𝔓 X)} :
                          ⋃ J ∈ TileStructure.Forest.𝓛 𝔖, ↑J = ⋃ (I : Grid X), ↑I

                          Part of Lemma 7.1.2

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

                          Part of Lemma 7.1.2

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

                          The constant used in first_tree_pointwise. Has value 10 * 2 ^ (105 * a ^ 3) in the blueprint.

                          Equations
                          Instances For
                            source
                            theorem TileStructure.Forest.first_tree_pointwise {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {x : X} {x' : X} {f : X β†’ β„‚} {L : Grid X} (hu : u ∈ t) (hL : L ∈ TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) (hx : x ∈ L) (hx' : x' ∈ L) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                            β†‘β€–βˆ‘ i ∈ t.Οƒ u x, ∫ (y : X), (Complex.exp (Complex.I * (-↑((𝒬 u) y) + ↑((Q x) y) + ↑((𝒬 u) x) - ↑((Q x) x))) - 1) * Ks i x y * f yβ€–β‚Š ≀ ↑(TileStructure.Forest.C7_1_4 a) * MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => β€–f xβ€–) x'

                            Lemma 7.1.4

                            source
                            theorem TileStructure.Forest.second_tree_pointwise {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {x : X} {x' : X} {f : X β†’ β„‚} {L : Grid X} (hu : u ∈ t) (hL : L ∈ TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) (hx : x ∈ L) (hx' : x' ∈ L) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                            β†‘β€–βˆ‘ i ∈ t.Οƒ u x, ∫ (y : X), Ks i x y * TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f yβ€–β‚Š ≀ TileStructure.Forest.nontangentialMaximalFunction (𝒬 u) (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f) x'

                            Lemma 7.1.5

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

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

                            Equations
                            Instances For
                              source
                              theorem TileStructure.Forest.third_tree_pointwise {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {x : X} {x' : X} {f : X β†’ β„‚} {L : Grid X} (hu : u ∈ t) (hL : L ∈ TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) (hx : x ∈ L) (hx' : x' ∈ L) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                              β†‘β€–βˆ‘ i ∈ t.Οƒ u x, ∫ (y : X), Ks i x y * (f y - TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f y)β€–β‚Š ≀ ↑(TileStructure.Forest.C7_1_6 a) * t.boundaryOperator u (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ↑‖f xβ€–) x'

                              Lemma 7.1.6

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

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

                              Equations
                              Instances For
                                source
                                theorem TileStructure.Forest.pointwise_tree_estimate {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {x : X} {x' : X} {f : X β†’ β„‚} {L : Grid X} (hu : u ∈ t) (hL : L ∈ TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) (hx : x ∈ L) (hx' : x' ∈ L) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                ↑‖carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) (fun (y : X) => Complex.exp (Complex.I * -↑((𝒬 u) y)) * f y) xβ€–β‚Š ≀ ↑(TileStructure.Forest.C7_1_3 a) * (MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => β€–f xβ€–) x' + t.boundaryOperator u (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ↑‖f xβ€–) x' + TileStructure.Forest.nontangentialMaximalFunction (𝒬 u) (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f) x')

                                Lemma 7.1.3.

                                Section 7.2 and Lemma 7.2.1 #

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

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

                                Equations
                                Instances For
                                  source
                                  theorem TileStructure.Forest.nontangential_operator_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f : X β†’ β„‚} (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (ΞΈ : Θ X) :
                                  MeasureTheory.eLpNorm (fun (x : X) => (TileStructure.Forest.nontangentialMaximalFunction ΞΈ f x).toReal) 2 MeasureTheory.volume ≀ MeasureTheory.eLpNorm f 2 MeasureTheory.volume

                                  Lemma 7.2.2.

                                  source
                                  theorem TileStructure.Forest.boundary_overlap {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (I : Grid X) :
                                  (Finset.filter (fun (J : Grid X) => s J = s I ∧ Β¬Disjoint (Metric.ball (c I) (4 * ↑(defaultD a) ^ s I)) (Metric.ball (c J) (4 * ↑(defaultD a) ^ s J))) Finset.univ).card ≀ 2 ^ (9 * a)

                                  Lemma 7.2.4.

                                  source
                                  theorem TileStructure.Forest.boundary_operator_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (hu : u ∈ t) :
                                  MeasureTheory.eLpNorm (fun (x : X) => (t.boundaryOperator u f x).toReal) 2 MeasureTheory.volume ≀ MeasureTheory.eLpNorm f 2 MeasureTheory.volume

                                  Lemma 7.2.3.

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

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

                                  Equations
                                  Instances For
                                    source
                                    theorem TileStructure.Forest.tree_projection_estimate {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} {g : X β†’ β„‚} (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (hg : Bornology.IsBounded (Set.range g)) (h2g : HasCompactSupport g) (hu : u ∈ t) :
                                    β†‘β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f xβ€–β‚Š ≀ ↑(TileStructure.Forest.C7_2_1 a) * MeasureTheory.eLpNorm (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => β€–f xβ€–) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => β€–g xβ€–) 2 MeasureTheory.volume

                                    Lemma 7.2.1.

                                    Section 7.3 and Lemma 7.3.1 #

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

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

                                    Equations
                                    Instances For
                                      source
                                      theorem TileStructure.Forest.local_dens1_tree_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {L : Grid X} (hu : u ∈ t) (hL : L ∈ TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) :
                                      MeasureTheory.volume (↑L ∩ ⋃ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u, E p) ≀ ↑(TileStructure.Forest.C7_3_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) * MeasureTheory.volume ↑L

                                      Lemma 7.3.2.

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

                                      The constant used in local_dens2_tree_bound. Has value 2 ^ (200 * a ^ 3 + 19) in the blueprint.

                                      Equations
                                      Instances For
                                        source
                                        theorem TileStructure.Forest.local_dens2_tree_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q✝ K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {J : Grid X} (hJ : J ∈ TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) {q : 𝔓 X} (hq : q ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hJq : Β¬Disjoint ↑J ↑(π“˜ q)) :
                                        MeasureTheory.volume (F ∩ ↑J) ≀ ↑(TileStructure.Forest.C7_3_3 a) * densβ‚‚ ((fun (x : 𝔓 X) => t.𝔗 x) u) * MeasureTheory.volume ↑J

                                        Lemma 7.3.3.

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

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

                                        Equations
                                        Instances For
                                          source
                                          theorem TileStructure.Forest.density_tree_bound1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} {g : X β†’ β„‚} (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (hg : Bornology.IsBounded (Set.range g)) (h2g : HasCompactSupport g) (hu : u ∈ t) :
                                          β†‘β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f xβ€–β‚Š ≀ ↑(TileStructure.Forest.C7_3_1_1 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

                                          First part of Lemma 7.3.1.

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

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

                                          Equations
                                          Instances For
                                            source
                                            theorem TileStructure.Forest.density_tree_bound2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} {g : X β†’ β„‚} (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (h3f : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hg : Bornology.IsBounded (Set.range g)) (h2g : HasCompactSupport g) (hu : u ∈ t) :
                                            β†‘β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f xβ€–β‚Š ≀ ↑(TileStructure.Forest.C7_3_1_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * densβ‚‚ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

                                            Second part of Lemma 7.3.1.

                                            Section 7.4 except Lemmas 4-6 #

                                            source
                                            def TileStructure.Forest.adjointCarleson {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {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 β†’ β„‚) (x : X) :
                                            β„‚

                                            The definition of `Tβ‚š*g(x), defined above Lemma 7.4.1

                                            Equations
                                            Instances For
                                              source
                                              def TileStructure.Forest.adjointCarlesonSum {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (β„­ : Set (𝔓 X)) (f : X β†’ β„‚) (x : X) :
                                              β„‚

                                              The definition of `T_β„­*g(x), defined at the bottom of Section 7.4

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

                                                The operator S_{2,𝔲} f(x), given above Lemma 7.4.3.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  def TileStructure.Forest.𝔖₀ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : TileStructure.Forest X n) (u₁ : 𝔓 X) (uβ‚‚ : 𝔓 X) :
                                                  Set (𝔓 X)

                                                  The set 𝔖 defined in the proof of Lemma 7.4.4. We append a subscript 0 to distinguish it from the section variable.

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem TileStructure.Forest.adjoint_tile_support1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {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 β†’ β„‚} (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                    TileStructure.Forest.adjointCarleson p f = (Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)).indicator (TileStructure.Forest.adjointCarleson p ((↑(π“˜ p)).indicator f))

                                                    Part 1 of Lemma 7.4.1. Todo: update blueprint with precise properties needed on the function.

                                                    source
                                                    theorem TileStructure.Forest.adjoint_tile_support2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {p : 𝔓 X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                    TileStructure.Forest.adjointCarleson p f = (↑(π“˜ p)).indicator (TileStructure.Forest.adjointCarleson p ((↑(π“˜ p)).indicator f))

                                                    Part 2 of Lemma 7.4.1. Todo: update blueprint with precise properties needed on the function.

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

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

                                                    Equations
                                                    Instances For
                                                      source
                                                      theorem TileStructure.Forest.adjoint_tree_estimate {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                      MeasureTheory.eLpNorm (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f) 2 MeasureTheory.volume ≀ ↑(TileStructure.Forest.C7_4_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

                                                      Lemma 7.4.2.

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

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

                                                      Equations
                                                      Instances For
                                                        source
                                                        theorem TileStructure.Forest.adjoint_tree_control {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hu : u ∈ t) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                        MeasureTheory.eLpNorm (fun (x : X) => (t.adjointBoundaryOperator u f x).toReal) 2 MeasureTheory.volume ≀ ↑(TileStructure.Forest.C7_4_3 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

                                                        Lemma 7.4.3.

                                                        source
                                                        theorem TileStructure.Forest.𝔗_subset_𝔖₀ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) :
                                                        (fun (x : 𝔓 X) => t.𝔗 x) u₁ βŠ† t.𝔖₀ u₁ uβ‚‚

                                                        Part 2 of Lemma 7.4.7.

                                                        source
                                                        theorem TileStructure.Forest.overlap_implies_distance {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {p : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u₁ βˆͺ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) (hpu₁ : Β¬Disjoint ↑(π“˜ p) ↑(π“˜ u₁)) :
                                                        p ∈ t.𝔖₀ u₁ uβ‚‚

                                                        Part 1 of Lemma 7.4.7.

                                                        Section 7.5 #

                                                        source
                                                        def TileStructure.Forest.𝓙₅ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : TileStructure.Forest X n) (u₁ : 𝔓 X) (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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (J : Grid X) (x : X) :
                                                          NNReal

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

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

                                                                Subsection 7.5.1 and Lemma 7.5.2 #

                                                                source
                                                                theorem TileStructure.Forest.union_𝓙₅ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) :
                                                                (t.𝓙₅ u₁ uβ‚‚).PairwiseDisjoint fun (I : Grid X) => ↑I

                                                                Part of Lemma 7.5.1.

                                                                source
                                                                theorem TileStructure.Forest.moderate_scale_change {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {J : Grid X} {J' : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hJ' : J' ∈ t.𝓙₅ u₁ uβ‚‚) (h : Β¬Disjoint ↑J ↑J') :
                                                                s J + 1 ≀ s J'

                                                                Lemma 7.5.3 (stated somewhat differently).

                                                                source
                                                                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.sum_Ο‡ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (x : X) :
                                                                  βˆ‘ J ∈ Finset.filter (fun (I : Grid X) => I ∈ t.𝓙₅ u₁ uβ‚‚) Finset.univ, t.Ο‡ u₁ uβ‚‚ J x = (↑(π“˜ u₁)).indicator 1 x

                                                                  Part of Lemma 7.5.2.

                                                                  source
                                                                  theorem TileStructure.Forest.Ο‡_mem_Icc {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {x : X} {I : Grid X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hx : x ∈ π“˜ u₁) :
                                                                  t.Ο‡ u₁ uβ‚‚ J x ∈ Set.Icc 0 ((Metric.ball (c I) (8 * ↑(defaultD a) ^ s I)).indicator 1 x)

                                                                  Part of Lemma 7.5.2.

                                                                  source
                                                                  theorem TileStructure.Forest.dist_Ο‡_Ο‡_le {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {x : X} {x' : X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hx : x ∈ π“˜ u₁) (hx' : x' ∈ π“˜ u₁) :
                                                                  dist (t.Ο‡ u₁ uβ‚‚ J x) (t.Ο‡ u₁ uβ‚‚ J x) ≀ ↑(TileStructure.Forest.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
                                                                  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.holder_correlation_tile {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {p : 𝔓 X} {x : X} {x' : X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                                    ↑(nndist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * TileStructure.Forest.adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * TileStructure.Forest.adjointCarleson p f x')) ≀ ↑(TileStructure.Forest.C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (↑(nndist x x') / ↑(defaultD a) ^ ↑(𝔰 p)) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, ↑‖f xβ€–β‚Š

                                                                    Lemma 7.5.5.

                                                                    source
                                                                    theorem TileStructure.Forest.limited_scale_impact {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {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
                                                                    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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {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 : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                                      ↑(⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚Š) ≀ ↑(TileStructure.Forest.C7_5_7 a) * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                                                                      Lemma 7.5.7.

                                                                      source
                                                                      theorem TileStructure.Forest.scales_impacting_interval {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {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
                                                                      def TileStructure.Forest.C7_5_9_1 (a : β„•) :
                                                                      NNReal

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

                                                                      Equations
                                                                      Instances For
                                                                        source
                                                                        def TileStructure.Forest.C7_5_9_2 (a : β„•) :
                                                                        NNReal

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

                                                                        Equations
                                                                        Instances For
                                                                          source
                                                                          theorem TileStructure.Forest.global_tree_control1_1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {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 : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                                          ↑(⨆ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum β„­ f xβ€–β‚Š) ≀ ↑(β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum β„­ f xβ€–β‚Š) + ↑(TileStructure.Forest.C7_5_9_1 a) * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                                                                          Part 1 of Lemma 7.5.9

                                                                          source
                                                                          theorem TileStructure.Forest.global_tree_control1_2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {p : 𝔓 X} {x : X} {x' : 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 : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) :
                                                                          ↑(nndist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * TileStructure.Forest.adjointCarlesonSum β„­ f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * TileStructure.Forest.adjointCarlesonSum β„­ f x')) ≀ ↑(TileStructure.Forest.C7_5_9_1 a) * (↑(nndist x x') / ↑(defaultD a) ^ ↑(𝔰 p)) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                                                                          Part 2 of Lemma 7.5.9

                                                                          source
                                                                          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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {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 : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                                            ↑(⨆ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚Š) ≀ β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), ↑‖TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) f xβ€–β‚Š + ↑(TileStructure.Forest.C7_5_10 a) * β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x

                                                                            Lemma 7.5.10

                                                                            source
                                                                            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.holder_correlation_tree {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {f₁ : X β†’ β„‚} {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 (TileStructure.Forest.C7_5_4 a * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f₁ xβ€–) x).toNNReal) * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) fβ‚‚ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.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
                                                                              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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
                                                                                ↑(TileStructure.Forest.C7_5_11 a n) ≀ dist (𝒬 u₁) (𝒬 uβ‚‚)

                                                                                Lemma 7.5.11

                                                                                source
                                                                                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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {f₁ : X β†’ β„‚} {fβ‚‚ : X β†’ β„‚} {g₁ : X β†’ β„‚} {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), TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(TileStructure.Forest.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

                                                                                  Section 7.6 and Lemma 7.4.6 #

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

                                                                                    Part of Lemma 7.6.1.

                                                                                    source
                                                                                    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_pos {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} [ProofData a q K σ₁ Οƒβ‚‚ F G] (h : 1 ≀ n) :
                                                                                      0 < TileStructure.Forest.C7_6_3 a n
                                                                                      source
                                                                                      theorem TileStructure.Forest.thin_scale_impact {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {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₁) (h : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) :
                                                                                      ↑(𝔰 p) ≀ ↑(s J) - TileStructure.Forest.C7_6_3 a n

                                                                                      Lemma 7.6.3.

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

                                                                                      The constant used in square_function_count. Has value Z * n / (202 * a ^ 3) - 2 in the blueprint.

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

                                                                                        Lemma 7.6.4.

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

                                                                                        The constant used in bound_for_tree_projection. Has value 2 ^ (118 * a ^ 3 - 100 / (202 * a) * Z * n * ΞΊ) in the blueprint.

                                                                                        Equations
                                                                                        Instances For
                                                                                          source
                                                                                          theorem TileStructure.Forest.bound_for_tree_projection {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                                                          MeasureTheory.eLpNorm (TileStructure.Forest.approxOnCube (t.𝓙₆ u₁) fun (x : X) => β€–TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–) 2 MeasureTheory.volume ≀ ↑(TileStructure.Forest.C7_6_2 a n) * MeasureTheory.eLpNorm ((↑(π“˜ u₁)).indicator fun (x : X) => (MB MeasureTheory.volume TileStructure.Forest.𝓑 TileStructure.Forest.c𝓑 TileStructure.Forest.r𝓑 (fun (x : X) => β€–f xβ€–) x).toReal) 2 MeasureTheory.volume

                                                                                          Lemma 7.6.2. Todo: add needed hypothesis to LaTeX

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

                                                                                          The constant used in correlation_near_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_near_tree_parts {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {f₁ : X β†’ β„‚} {fβ‚‚ : X β†’ β„‚} {g₁ : X β†’ β„‚} {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), TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(TileStructure.Forest.C7_4_6 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.6

                                                                                            Lemmas 7.4.4 #

                                                                                            source
                                                                                            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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {f₁ : X β†’ β„‚} {fβ‚‚ : X β†’ β„‚} {g₁ : X β†’ β„‚} {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), TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(TileStructure.Forest.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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u₁ : 𝔓 X} {uβ‚‚ : 𝔓 X} {f₁ : X β†’ β„‚} {fβ‚‚ : X β†’ β„‚} {g₁ : X β†’ β„‚} {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), TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) gβ‚‚ x)β€–β‚Š ≀ ↑(TileStructure.Forest.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 and Proposition 2.0.4 #

                                                                                              source
                                                                                              def TileStructure.Forest.rowDecomp {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : TileStructure.Forest X n) (j : β„•) :
                                                                                              TileStructure.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
                                                                                              Instances For
                                                                                                source
                                                                                                @[simp]
                                                                                                theorem TileStructure.Forest.biUnion_rowDecomp {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {j : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} :
                                                                                                (fun (x : 𝔓 X) => (t.rowDecomp j).𝔗 x) u = (fun (x : 𝔓 X) => t.𝔗 x) u
                                                                                                source
                                                                                                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
                                                                                                  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.row_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {j : β„•} {t : TileStructure.Forest X n} {f : X β†’ β„‚} (hj : j < 2 ^ n) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                                                                    MeasureTheory.eLpNorm (βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f) 2 MeasureTheory.volume ≀ ↑(TileStructure.Forest.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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {j : β„•} {t : TileStructure.Forest X n} {u : 𝔓 X} {f : X β†’ β„‚} (hj : j < 2 ^ n) (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) :
                                                                                                    MeasureTheory.eLpNorm ((βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, F.indicator) (TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f)) 2 MeasureTheory.volume ≀ ↑(TileStructure.Forest.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
                                                                                                    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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {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 : TileStructure.Forest X n} {f₁ : X β†’ β„‚} {fβ‚‚ : X β†’ β„‚} (hjj' : j < j') (hj' : j' < 2 ^ n) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) :
                                                                                                      β†‘β€–βˆ« (x : X), (βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f₁ x) * βˆ‘ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j') Finset.univ, TileStructure.Forest.adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) fβ‚‚ xβ€–β‚Š ≀ ↑(TileStructure.Forest.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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : TileStructure.Forest X n) (j : β„•) :
                                                                                                      Set X

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

                                                                                                      Equations
                                                                                                      • t.rowSupport j = ⋃ u ∈ t.rowDecomp j, ⋃ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u, E p
                                                                                                      Instances For
                                                                                                        source
                                                                                                        theorem TileStructure.Forest.pairwiseDisjoint_rowSupport {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} :
                                                                                                        (Set.Iio (2 ^ n)).PairwiseDisjoint t.rowSupport

                                                                                                        Lemma 7.7.4

                                                                                                        source
                                                                                                        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 β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {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 β†’ β„‚} {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