The function ψ

def ψ (D : ℕ) (x : ℝ) : ℝ

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

Equations

• ψ D x = max 0 (min 1 (min (4 * ↑D * x - 1) (2 - 4 * x)))

def ShortVariables.termψ : Lean.ParserDescr

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

Equations

• ShortVariables.termψ = Lean.ParserDescr.node `ShortVariables.termψ 1024 (Lean.ParserDescr.symbol "ψ")

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 enorm_ψ_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 continuous_ψ {D : ℕ} : Continuous (ψ D)

theorem support_ψ {D : ℕ} (hD : 1 < ↑D) : Function.support (ψ D) = Set.Ioo (4 * ↑D)⁻¹ 2⁻¹

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

noncomputable def nonzeroS (D : ℕ) (x : ℝ) : Finset ℤ

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

Equations

• nonzeroS D x = Finset.Icc ⌊1 + Real.logb (↑D) (2 * x)⌋ ⌈Real.logb (↑D) (4 * x)⌉

theorem sum_ψ {D : ℕ} {x : ℝ} (hD : 1 < ↑D) (hx : 0 < x) : ∑ s ∈ nonzeroS 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 ↔ s ∉ nonzeroS 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) : ∑ s ∈ S, ψ D (↑D ^ (-s) * x) ≤ 1

noncomputable def Ks {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] (s : ℤ) (x y : X) : ℂ

K_s in the blueprint

Equations

• Ks s x y = K x y * ↑(ψ (defaultD a) (↑(defaultD a) ^ (-s) * dist x y))

theorem Ks_def {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] (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 : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] {x y : X} [KernelProofData a K] {t : Finset ℤ} (hs : nonzeroS (defaultD a) (dist x y) ⊆ t) (hD : 1 < ↑(defaultD a)) (h : 0 < dist x y) : ∑ i ∈ t, Ks i x y = K x y

theorem dist_mem_Ioo_of_Ks_ne_zero {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {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 : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} {x y : X} (h : Ks s x y ≠ 0) : dist x y ∈ Set.Icc (↑(defaultD a) ^ (s - 1) / 4) (↑(defaultD a) ^ s / 2)

Lemma 2.1.3 part 1, equation (2.1.2)

theorem dist_mem_Icc_of_mem_tsupport_Ks {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} {x : X × X} (h : x ∈ tsupport fun (x : X × X) => Ks s x.1 x.2) : dist x.1 x.2 ∈ 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. Equal to 2 ^ (102 * a ^ 3) in the blueprint.

Equations

• C2_1_3 a = 2 ^ ((𝕔 + 2) * a ^ 3)

def D2_1_3 (a : ℕ) : NNReal

The constant appearing in part 3 of Lemma 2.1.3. Equal to 2 ^ (127 * a ^ 3) in the blueprint.

Equations

• D2_1_3 a = 2 ^ ((𝕔 + 2 + 𝕔 / 4) * a ^ 3)

theorem kernel_bound {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} {x y : X} : ‖Ks s x y‖ₑ ≤ ↑(C_K ↑a) / vol x y

Equation (1.1.11) in the blueprint

theorem DoublingMeasure.volume_ball_two_le_same_repeat {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] (x : X) (r : ℝ) (n : ℕ) : MeasureTheory.volume (Metric.ball x (2 ^ n * r)) ≤ ↑(defaultA a) ^ n * MeasureTheory.volume (Metric.ball x r)

Apply volume_ball_two_le_same n times.

theorem Metric.measure_ball_pos_nnreal {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] (x : X) (r : ℝ) (hr : r > 0) : (MeasureTheory.volume (ball x r)).toNNReal > 0

theorem Metric.measure_ball_pos_real {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] (x : X) (r : ℝ) (hr : r > 0) : MeasureTheory.volume.real (ball x r) > 0

theorem enorm_K_le {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} {x y : X} (n : ℕ) (hxy : dist x y ≥ ↑(defaultD a) ^ (s - 1) / 4) : ‖K x y‖ₑ ≤ 2 ^ ((2 + n) * a + (𝕔 + 1) * a ^ 3) / MeasureTheory.volume (Metric.ball x (2 ^ n * ↑(defaultD a) ^ s))

theorem enorm_Ks_le {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} {x y : X} : ‖Ks s x y‖ₑ ≤ ↑(C2_1_3 a) / MeasureTheory.volume (Metric.ball x (↑(defaultD a) ^ s))

Lemma 2.1.3 part 2, equation (2.1.3)

theorem enorm_Ks_le' {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {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 Bornology.IsBounded.exists_bound_of_norm_Ks {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {A : Set X} (hA : IsBounded A) (s : ℤ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x y : X), x ∈ A → ‖Ks s x y‖ ≤ C

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

theorem enorm_Ks_sub_Ks_le_of_nonzero {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {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 (Metric.ball x (↑(defaultD a) ^ s)) * (edist y y' / ↑(defaultD a) ^ s) ^ (↑a)⁻¹

theorem enorm_Ks_sub_Ks_le {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {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)) * (edist y y' / ↑(defaultD a) ^ s) ^ (↑a)⁻¹

Lemma 2.1.3 part 3, equation (2.1.4)

theorem stronglyMeasurable_Ks {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} : MeasureTheory.StronglyMeasurable fun (x : X × X) => Ks s x.1 x.2

theorem measurable_Ks {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} : Measurable fun (x : X × X) => Ks s x.1 x.2

theorem aestronglyMeasurable_Ks {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} : MeasureTheory.AEStronglyMeasurable (fun (x : X × X) => Ks s x.1 x.2) MeasureTheory.volume

theorem integrable_Ks_x {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {s : ℤ} {x : X} (hD : 1 < ↑(defaultD a)) : MeasureTheory.Integrable (Ks s x) MeasureTheory.volume

The function y ↦ Ks s x y is integrable.

theorem Ks_eq_zero_of_dist_le (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : ℤ} {x y : X} (hxy : x ≠ y) (h : dist x y ≤ ↑(defaultD a) ^ (s - 1) / 4) : Ks s x y = 0

theorem Ks_eq_zero_of_le_dist (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : ℤ} {x y : X} (h : ↑(defaultD a) ^ s / 2 ≤ dist x y) : Ks s x y = 0