Documentation

Carleson.ForestOperator.PointwiseEstimate

Section 7.1 and Lemma 7.1.3 #

source
def TileStructure.Forest.Οƒ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : 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 β†’ β„€} {F 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 β†’ β„€} {F 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
        theorem TileStructure.Forest.𝓙_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)] {𝔖 : Set (𝔓 X)} :
        TileStructure.Forest.𝓙 𝔖 βŠ† TileStructure.Forest.𝓙₀ 𝔖
        source
        def TileStructure.Forest.𝓛₀ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔖 : 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 β†’ β„€} {F 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
            theorem TileStructure.Forest.𝓛_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)] {𝔖 : Set (𝔓 X)} :
            TileStructure.Forest.𝓛 𝔖 βŠ† TileStructure.Forest.𝓛₀ 𝔖
            source
            def TileStructure.Forest.approxOnCube {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)] {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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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.𝓑_finite {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)] :
                          TileStructure.Forest.𝓑.Finite
                          source
                          theorem TileStructure.Forest.convex_scales {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 : 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                          theorem TileStructure.Forest.C7_1_4_def (a : β„•) :
                          TileStructure.Forest.C7_1_4 a = 10 * 2 ^ (105 * ↑a ^ 3)
                          source
                          @[irreducible]
                          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 β†’ β„€} {F 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} {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 : MeasureTheory.BoundedCompactSupport 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 β†’ β„€} {F 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} {f : X β†’ β„‚} {L : Grid X} (hu : u ∈ t) (hL : L ∈ TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) (hx : x ∈ L) (hx' : x' ∈ L) :
                            β†‘β€–βˆ‘ 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
                            theorem TileStructure.Forest.C7_1_6_def (a : β„•) :
                            TileStructure.Forest.C7_1_6 a = 2 ^ (151 * ↑a ^ 3)
                            source
                            @[irreducible]
                            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 β†’ β„€} {F 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} {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 : MeasureTheory.BoundedCompactSupport 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
                              @[irreducible]
                              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.C7_1_3_def (a : β„•) :
                                TileStructure.Forest.C7_1_3 a = 2 ^ (151 * ↑a ^ 3)
                                source
                                theorem TileStructure.Forest.pointwise_tree_estimate {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : TileStructure.Forest X n} {u : 𝔓 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 : MeasureTheory.BoundedCompactSupport 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.