Documentation

Carleson.Psi

The function ψ

def ψ (D : ) (x : ) :

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

Equations

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

Equations
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
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
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
def D2_1_3 (a : NNReal) :

The constant appearing in part 3 of Lemma 2.1.3.

Equations
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.