Documentation

Carleson.Psi

The function ψ

def ψ (D : ) (x : ) :

The function ψ used as a basis for a dyadic partition of unity.

Equations
Instances For

    The function ψ used as a basis for a dyadic partition of unity.

    Equations
    Instances For
      theorem zero_le_ψ (D : ) (x : ) :
      0 ψ D x
      theorem ψ_le_one (D : ) (x : ) :
      ψ D x 1
      theorem abs_ψ_le_one (D : ) (x : ) :
      |ψ D x| 1
      theorem ψ_formula₀ {D : } {x : } (hx : x 1 / (4 * D)) :
      ψ D x = 0
      theorem ψ_formula₁ {D : } (hD : 1 < D) {x : } (hx : 1 / (4 * D) x x 1 / (2 * D)) :
      ψ D x = 4 * D * x - 1
      theorem ψ_formula₂ {D : } (hD : 1 < D) {x : } (hx : 1 / (2 * D) x x 1 / 4) :
      ψ D x = 1
      theorem ψ_formula₃ {D : } (hD : 1 < D) {x : } (hx : 1 / 4 x x 1 / 2) :
      ψ D x = 2 - 4 * x
      theorem ψ_formula₄ {D : } {x : } (hx : x 1 / 2) :
      ψ D x = 0
      theorem psi_zero {D : } :
      ψ D 0 = 0
      theorem support_ψ {D : } (hD : 1 < D) :
      theorem lipschitzWith_ψ {D : } (hD : 1 D) :
      LipschitzWith (4 * D) (ψ D)
      theorem lipschitzWith_ψ' {D : } (hD : 1 D) (a b : ) :
      ψ D a - ψ D b 4 * D * dist a b
      def nonzeroS (D : ) (x : ) :

      the one or two numbers s where ψ (D ^ (-s) * x) is possibly nonzero

      Equations
      Instances For
        theorem sum_ψ {D : } {x : } (hD : 1 < D) (hx : 0 < x) :
        snonzeroS D x, ψ D (D ^ (-s) * x) = 1
        theorem mem_nonzeroS_iff {D : } (hD : 1 < D) {i : } {x : } (hx : 0 < x) :
        i nonzeroS D x D ^ (-i) * x Set.Ioo (4 * D)⁻¹ 2⁻¹
        theorem psi_ne_zero_iff {D : } {s : } (hD : 1 < D) {x : } (hx : 0 < x) :
        ψ D (D ^ (-s) * x) 0 s nonzeroS D x
        theorem psi_eq_zero_iff {D : } {s : } (hD : 1 < D) {x : } (hx : 0 < x) :
        ψ D (D ^ (-s) * x) = 0 snonzeroS D x
        theorem support_ψS {D : } {x : } (hD : 1 < D) (hx : 0 < x) :
        (Function.support fun (s : ) => ψ D (D ^ (-s) * x)) = (nonzeroS D x)
        theorem support_ψS_subset_Icc {D : } (hD : 1 < D) {b c : } {x : } (h : x Set.Icc (D ^ (b - 1) / 2) (D ^ c / 4)) :
        (Function.support fun (s : ) => ψ D (D ^ (-s) * x)) Set.Icc b c
        theorem finsum_ψ {D : } {x : } (hD : 1 < D) (hx : 0 < x) :
        ∑ᶠ (s : ), ψ D (D ^ (-s) * x) = 1
        theorem sum_ψ_le {D : } {x : } (hD : 1 < D) (S : Finset ) (hx : 0 < x) :
        sS, ψ D (D ^ (-s) * x) 1
        def Ks {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ) (x y : X) :

        K_s in the blueprint

        Equations
        Instances For
          theorem Ks_def {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ) (x y : X) :
          Ks s x y = K x y * (ψ (defaultD a) ((defaultD a) ^ (-s) * dist x y))
          theorem sum_Ks {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y : X} {t : Finset } (hs : nonzeroS (defaultD a) (dist x y) t) (hD : 1 < (defaultD a)) (h : 0 < dist x y) :
          it, Ks i x y = K x y
          theorem dist_mem_Ioo_of_Ks_ne_zero {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} (h : Ks s x y 0) :
          dist x y Set.Ioo ((defaultD a) ^ (s - 1) / 4) ((defaultD a) ^ s / 2)
          theorem dist_mem_Icc_of_Ks_ne_zero {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} (h : Ks s x y 0) :
          dist x y Set.Icc ((defaultD a) ^ (s - 1) / 4) ((defaultD a) ^ s / 2)
          def C2_1_3 (a : NNReal) :

          The constant appearing in part 2 of Lemma 2.1.3.

          Equations
          Instances For
            def D2_1_3 (a : NNReal) :

            The constant appearing in part 3 of Lemma 2.1.3.

            Equations
            Instances For
              theorem kernel_bound_old {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} :

              preferably use kernel_bound instead.

              theorem kernel_bound {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} :
              Ks s x y‖ₑ (C_K a) / vol x y
              theorem DoublingMeasure.volume_ball_two_le_same_repeat {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (x : X) (r : ) (n : ) :

              Apply volume_ball_two_le_same n times.

              theorem Metric.measure_ball_pos_nnreal {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (x : X) (r : ) (hr : r > 0) :
              theorem Metric.measure_ball_pos_real {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (x : X) (r : ) (hr : r > 0) :
              theorem K_eq_K_of_dist_eq_zero {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y y' : X} (hyy' : dist y y' = 0) :
              K x y = K x y'
              theorem K_eq_zero_of_dist_eq_zero {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y : X} (hxy : dist x y = 0) :
              K x y = 0
              theorem norm_K_le {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} (n : ) (hxy : dist x y (defaultD a) ^ (s - 1) / 4) :
              K x y 2 ^ ((2 + n) * a + 101 * a ^ 3) / MeasureTheory.volume.real (Metric.ball x (2 ^ n * (defaultD a) ^ s))
              theorem enorm_K_le {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} (n : ) (hxy : dist x y (defaultD a) ^ (s - 1) / 4) :
              K x y‖ₑ 2 ^ ((2 + n) * a + 101 * a ^ 3) / MeasureTheory.volume (Metric.ball x (2 ^ n * (defaultD a) ^ s))
              theorem norm_Ks_le {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} :
              theorem enorm_Ks_le {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} :
              theorem enorm_Ks_le' {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y : X} :
              Ks s x y‖ₑ (C2_1_3 a) / MeasureTheory.volume (Metric.ball x ((defaultD a) ^ s)) * ψ (defaultD a) ((defaultD a) ^ (-s) * dist x y)‖ₑ

              Needed for Lemma 7.5.5.

              theorem norm_Ks_le_of_dist_le {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y x₀ : X} {r₀ : } (hr₀ : 0 < r₀) (hx : dist x x₀ r₀) (s : ) :
              Ks s x y (C2_1_3 a) * (MeasureTheory.As (↑(defaultA a)) (2 * r₀ / (defaultD a) ^ s)) / MeasureTheory.volume.real (Metric.ball x₀ r₀)

              Ks is bounded uniformly in x, y assuming x is in a fixed closed ball.

              theorem Bornology.IsBounded.exists_bound_of_norm_Ks {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {A : Set X} (hA : IsBounded A) (s : ) :
              ∃ (C : ), 0 C ∀ (x y : X), x AKs s x y C

              ‖Ks x y‖ is bounded if x is in a bounded set

              theorem norm_Ks_sub_Ks_le_of_nonzero {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y y' : X} (hK : Ks s x y 0) :
              Ks s x y - Ks s x y' (D2_1_3 a) / MeasureTheory.volume.real (Metric.ball x ((defaultD a) ^ s)) * (dist y y' / (defaultD a) ^ s) ^ (↑a)⁻¹
              theorem norm_Ks_sub_Ks_le {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ) (x y y' : X) :
              Ks s x y - Ks s x y' (D2_1_3 a) / MeasureTheory.volume.real (Metric.ball x ((defaultD a) ^ s)) * (dist y y' / (defaultD a) ^ s) ^ (↑a)⁻¹
              theorem nnnorm_Ks_sub_Ks_le {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x y y' : X} :
              Ks s x y - Ks s x y'‖₊ (D2_1_3 a) / MeasureTheory.volume (Metric.ball x ((defaultD a) ^ s)) * ((nndist y y') / (defaultD a) ^ s) ^ (↑a)⁻¹
              theorem stronglyMeasurable_Ks {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } :
              MeasureTheory.StronglyMeasurable fun (x : X × X) => Ks s x.1 x.2
              theorem measurable_Ks {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } :
              Measurable fun (x : X × X) => Ks s x.1 x.2
              theorem aestronglyMeasurable_Ks {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } :
              theorem integrable_Ks_x {X : Type u_1} {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : } {x : X} (hD : 1 < (defaultD a)) :

              The function y ↦ Ks s x y is integrable.