The function ψ

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

Equations

• ψ D x = 0 ⊔ 1 ⊓ ((4 * ↑D * x - 1) ⊓ (2 - 4 * x))

def ShortVariables.termψ : Lean.ParserDescr

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 ψ_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

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

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

def Ks {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (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 : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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) : ∑ i ∈ t, Ks i x y = K x y

theorem dist_mem_Ioo_of_Ks_ne_zero {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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) : NNReal

The constant appearing in part 2 of Lemma 2.1.3.

Equations

• C2_1_3 a = 2 ^ (102 * ↑a ^ 3)

def D2_1_3 (a : NNReal) : NNReal

The constant appearing in part 3 of Lemma 2.1.3.

Equations

• D2_1_3 a = 2 ^ (150 * ↑a ^ 3)

theorem kernel_bound {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : ℤ} {x y : X} : ‖Ks s x y‖₊ ≤ 2 ^ a ^ 3 / MeasureTheory.volume.nnreal (Metric.ball x (dist x y))

theorem DoublingMeasure.volume_ball_two_le_same_repeat {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (x : X) (r : ℝ) (n : ℕ) : MeasureTheory.volume.real (Metric.ball x (2 ^ n * r)) ≤ ↑(defaultA a) ^ n * MeasureTheory.volume.real (Metric.ball x r)

Apply volume_ball_two_le_same n times.

theorem Metric.measure_ball_pos_nnreal {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (x : X) (r : ℝ) (hr : r > 0) : MeasureTheory.volume.nnreal (ball x r) > 0

theorem Metric.measure_ball_pos_real {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (x : X) (r : ℝ) (hr : r > 0) : MeasureTheory.volume.real (ball x r) > 0

theorem K_eq_K_of_dist_eq_zero {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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.real (Metric.ball x (↑(defaultD a) ^ s))

theorem nnnorm_Ks_le {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : 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))

theorem enorm_Ks_le {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 ∈ A → ‖Ks 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : 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 : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : ℤ} : MeasureTheory.AEStronglyMeasurable (fun (x : X × X) => Ks s x.1 x.2) MeasureTheory.volume

theorem integrable_Ks_x {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s : ℤ} {x : X} (hD : 1 < ↑(defaultD a)) : MeasureTheory.Integrable (Ks s x) MeasureTheory.volume

The function y ↦ Ks s x y is integrable.