Documentation

Carleson.ForestOperator.AlmostOrthogonality

Section 7.4 except Lemmas 4-6 #

source
def TileStructure.Forest.adjointCarleson {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 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 β†’ β„€} {F 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 β†’ β„€} {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_{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 β†’ β„€} {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₁ 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 MeasureTheory.AEStronglyMeasurable.adjointCarleson {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
          MeasureTheory.AEStronglyMeasurable (TileStructure.Forest.adjointCarleson p f) MeasureTheory.volume
          source
          theorem MeasureTheory.AEStronglyMeasurable.adjointCarlesonSum {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)] {f : X β†’ β„‚} {β„­ : Set (𝔓 X)} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
          MeasureTheory.AEStronglyMeasurable (TileStructure.Forest.adjointCarlesonSum β„­ f) MeasureTheory.volume
          source
          theorem TileStructure.Forest.adjoint_eq_adjoint_indicator {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)] {u p : 𝔓 X} {f : X β†’ β„‚} (h : E p βŠ† ↑(π“˜ u)) :
          TileStructure.Forest.adjointCarleson p f = TileStructure.Forest.adjointCarleson p ((↑(π“˜ u)).indicator f)
          source
          theorem TileStructure.Forest.adjoint_tile_support1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} :
          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 β†’ β„€} {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 p : 𝔓 X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) :
          TileStructure.Forest.adjointCarleson p f = (↑(π“˜ u)).indicator (TileStructure.Forest.adjointCarleson p ((↑(π“˜ u)).indicator f))

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

          source
          theorem MeasureTheory.BoundedCompactSupport.adjointCarleson {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f) :
          MeasureTheory.BoundedCompactSupport (TileStructure.Forest.adjointCarleson p f)
          source
          theorem MeasureTheory.BoundedCompactSupport.adjointCarlesonSum {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)] {f : X β†’ β„‚} {β„­ : Set (𝔓 X)} (hf : MeasureTheory.BoundedCompactSupport f) :
          MeasureTheory.BoundedCompactSupport (TileStructure.Forest.adjointCarlesonSum β„­ f)
          source
          theorem TileStructure.Forest.adjointCarleson_adjoint {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f g : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f) (hg : MeasureTheory.BoundedCompactSupport g) (p : 𝔓 X) :
          ∫ (x : X), (starRingEnd β„‚) (g x) * carlesonOn p f x = ∫ (y : X), (starRingEnd β„‚) (TileStructure.Forest.adjointCarleson p g y) * f y

          adjointCarleson is the adjoint of carlesonOn.

          source
          theorem TileStructure.Forest.adjointCarlesonSum_adjoint {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f g : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f) (hg : MeasureTheory.BoundedCompactSupport g) (β„­ : Set (𝔓 X)) :
          ∫ (x : X), (starRingEnd β„‚) (g x) * carlesonSum β„­ f x = ∫ (x : X), (starRingEnd β„‚) (TileStructure.Forest.adjointCarlesonSum β„­ g x) * f x

          adjointCarlesonSum is the adjoint of carlesonSum.

          source
          @[irreducible]
          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.C7_4_2_def (a : β„•) :
            TileStructure.Forest.C7_4_2 a = TileStructure.Forest.C7_3_1_1 a
            source
            theorem TileStructure.Forest.adjoint_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} {f : X β†’ β„‚} (hu : u ∈ t) (hf : MeasureTheory.BoundedCompactSupport 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
            @[irreducible]
            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.C7_4_3_def (a : β„•) :
              TileStructure.Forest.C7_4_3 a = TileStructure.Forest.C7_4_2 a + CMB (↑(defaultA a)) 2 + 1
              source
              theorem TileStructure.Forest.adjoint_tree_control {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 β†’ β„‚} (hu : u ∈ t) (hf : MeasureTheory.BoundedCompactSupport 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.overlap_implies_distance {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₁ uβ‚‚ 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.

              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)] {n : β„•} {t : TileStructure.Forest X n} {u₁ 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.