This should roughly contain the contents of chapter 8.

def cutoff {X : Type u_1} [MetricSpace X] (R t : ℝ) (x y : X) : ℝ

cutoff R t x y is L(x, y) in the proof of Lemma 8.0.1.

Equations

• cutoff R t x y = 0 ⊔ (1 - dist x y / (t * R))

theorem cutoff_nonneg {X : Type u_1} [MetricSpace X] {R t : ℝ} {x y : X} : 0 ≤ cutoff R t x y

theorem cutoff_comm {X : Type u_1} [MetricSpace X] {R t : ℝ} {x y : X} : cutoff R t x y = cutoff R t y x

theorem cutoff_Lipschitz {X : Type u_1} [MetricSpace X] {R t : ℝ} {x : X} (hR : 0 < R) (ht : 0 < t) : LipschitzWith ⟨1 / (t * R), ⋯⟩ fun (y : X) => cutoff R t x y

theorem cutoff_continuous {X : Type u_1} [MetricSpace X] {R t : ℝ} {x : X} (hR : 0 < R) (ht : 0 < t) : Continuous fun (y : X) => cutoff R t x y

theorem cutoff_measurable {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {R t : ℝ} {x : X} (hR : 0 < R) (ht : 0 < t) : Measurable fun (y : X) => cutoff R t x y

cutoff R t x is measurable in y.

theorem cutoff_eq_zero {X : Type u_1} [MetricSpace X] {R t : ℝ} (hR : 0 < R) (ht : 0 < t) {x y : X} (hy : y ∉ Metric.ball x (t * R)) : cutoff R t x y = 0

theorem hasCompactSupport_cutoff {X : Type u_1} [MetricSpace X] {R t : ℝ} [ProperSpace X] (hR : 0 < R) (ht : 0 < t) {x : X} : HasCompactSupport fun (y : X) => cutoff R t x y

theorem integrable_cutoff {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {R t : ℝ} (hR : 0 < R) (ht : 0 < t) {x : X} : MeasureTheory.Integrable (fun (y : X) => cutoff R t x y) MeasureTheory.volume

theorem integrable_cutoff_mul {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {R t : ℝ} {z : X} (hR : 0 < R) (ht : 0 < t) {x : X} {ϕ : X → ℂ} (hc : Continuous ϕ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) : MeasureTheory.Integrable (fun (y : X) => ↑(cutoff R t x y) * ϕ y) MeasureTheory.volume

theorem leq_of_max_neq_left {a b : ℝ} (h : a ⊔ b ≠ a) : a < b

theorem leq_of_max_neq_right {a b : ℝ} (h : a ⊔ b ≠ b) : b < a

theorem aux_8_0_4 {X : Type u_1} [MetricSpace X] {R t : ℝ} {x y : X} (hR : 0 < R) (ht : 0 < t) (h : cutoff R t x y ≠ 0) : y ∈ Metric.ball x (t * R)

Equation 8.0.4 from the blueprint

theorem aux_8_0_5 {X : Type u_1} [MetricSpace X] {R t : ℝ} {x y : X} (hR : 0 < R) (ht : 0 < t) (h : y ∈ Metric.ball x (2⁻¹ * t * R)) : 2⁻¹ ≤ cutoff R t x y

theorem aux_8_0_6 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {R t : ℝ} {x : X} (hR : 0 < R) (ht : 0 < t) : 2⁻¹ * MeasureTheory.volume.real (Metric.ball x (2⁻¹ * t * R)) ≤ ∫ (y : X), cutoff R t x y

theorem integral_cutoff_pos {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) : 0 < ∫ (y : X), cutoff R t x y

def C8_0_1 (a : ℝ) (t : NNReal) : NNReal

The constant occurring in Lemma 8.0.1.

Equations

• C8_0_1 a t = ⟨2 ^ (4 * a) * ↑t ^ (-(a + 1)), ⋯⟩

def holderApprox {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] (R t : ℝ) (ϕ : X → ℂ) (x : X) : ℂ

ϕ ↦ \tilde{ϕ} in the proof of Lemma 8.0.1.

Equations

• holderApprox R t ϕ x = (∫ (y : X), ↑(cutoff R t x y) * ϕ y) / ↑(∫ (y : X), cutoff R t x y)

theorem integral_mul_holderApprox {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (ϕ : X → ℂ) : ↑(∫ (y : X), cutoff R t x y) * holderApprox R t ϕ x = ∫ (y : X), ↑(cutoff R t x y) * ϕ y

theorem foo {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {φ : X → ℂ} (hf : ∫ (x : X), φ x ≠ 0) : ∃ (z : X), φ z ≠ 0

theorem support_holderApprox_subset {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {z : X} {R t : ℝ} (hR : 0 < R) (ϕ : X → ℂ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) (ht : t ∈ Set.Ioc 0 1) : Function.support (holderApprox R t ϕ) ⊆ Metric.ball z (2 * R)

Part of Lemma 8.0.1.

theorem dist_holderApprox_le {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {z : X} {R t : ℝ} (hR : 0 < R) {C : NNReal} (ht : 0 < t) (ϕ : X → ℂ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) (h2ϕ : HolderWith C (nnτ X) ϕ) (hτ : 0 < nnτ X) (x : X) : dist (ϕ x) (holderApprox R t ϕ x) ≤ t ^ defaultτ a * (R ^ defaultτ a * ↑C)

Part of Lemma 8.0.1: Equation (8.0.1). Note that the norm ||ϕ||_C^τ is normalized by definition, i.e., it is R ^ τ times the best Hölder constant of ϕ, so the Lean statement corresponds to the blueprint statement. We assume that ϕ is globally Hölder for simplicity, but this is equivalent to being Hölder on ball z R as ϕ is supported there.

theorem holderApprox_le {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {R t : ℝ} (hR : 0 < R) {C : NNReal} (ht : 0 < t) {ϕ : X → ℂ} (hC : ∀ (x : X), ‖ϕ x‖ ≤ ↑C) (x : X) : ‖holderApprox R t ϕ x‖ ≤ ↑C

Part of Lemma 8.0.1: sup norm control in Equation (8.0.2). Note that it only uses the sup norm of ϕ, no need for a Hölder control.

theorem norm_holderApprox_sub_le_aux {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1) {C : NNReal} {ϕ : X → ℂ} (hc : Continuous ϕ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) (hC : ∀ (x : X), ‖ϕ x‖ ≤ ↑C) {x x' : X} (h : dist x x' < R) : ‖holderApprox R t ϕ x' - holderApprox R t ϕ x‖ ≤ 2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - ↑a) * ↑C * dist x x' / R

Auxiliary lemma: part of the Lipschitz control in Equation (8.0.2), when the distance between the points is at most R.

theorem norm_holderApprox_sub_le {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1) {C : NNReal} {ϕ : X → ℂ} (hc : Continuous ϕ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) (hC : ∀ (x : X), ‖ϕ x‖ ≤ ↑C) {x x' : X} : ‖holderApprox R t ϕ x - holderApprox R t ϕ x'‖ ≤ 2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - ↑a) * ↑C * dist x x' / R

Part of Lemma 8.0.1: Lipschitz norm control in Equation (8.0.2). Note that it only uses the sup norm of ϕ, no need for a Hölder control.

theorem iLipENorm_holderApprox' {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1) {C : NNReal} {ϕ : X → ℂ} (hc : Continuous ϕ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) (hC : ∀ (x : X), ‖ϕ x‖ ≤ ↑C) : iLipENorm (holderApprox R t ϕ) z R ≤ 2 ^ (4 * a) * ENNReal.ofReal t ^ (-1 - ↑a) * ↑C

theorem iLipENorm_holderApprox {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1) {ϕ : X → ℂ} (hϕ : tsupport ϕ ⊆ Metric.ball z R) : iLipENorm (holderApprox R t ϕ) z R ≤ 2 ^ (4 * a) * ENNReal.ofReal t ^ (-1 - ↑a) * iHolENorm ϕ z R

def C2_0_5 (a : ℝ) : NNReal

The constant occurring in Proposition 2.0.5.

Equations

• C2_0_5 a = 2 ^ (8 * a)

theorem holder_van_der_corput {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {z : X} {R : NNReal} (hR : 0 < R) {ϕ : X → ℂ} (hϕ : Function.support ϕ ⊆ Metric.ball z ↑R) (h2ϕ : iHolENorm ϕ z ↑R < ⊤) {f g : Θ X} : ↑‖∫ (x : X), Complex.exp (Complex.I * (↑(f x) - ↑(g x))) * ϕ x‖₊ ≤ ↑(C2_0_5 ↑a) * MeasureTheory.volume (Metric.ball z ↑R) * iHolENorm ϕ z ↑R * (1 + ↑(nndist_{z ,↑R} f g)) ^ (2 * ↑a ^ 2 + ↑a ^ 3)⁻¹

Proposition 2.0.5.