This should roughly contain the contents of chapter 8.

noncomputable 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 = max 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 : max a b ≠ a) : a < b

theorem leq_of_max_neq_right {a b : ℝ} (h : max 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

noncomputable 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)), ⋯⟩

noncomputable 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 support_holderApprox_subset_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 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 (R + R')

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) (h't : t ≤ 1) {φ : X → ℂ} (hφ : Function.support φ ⊆ Metric.ball z R) (h2φ : HolderOnWith C (nnτ X) φ (Metric.ball z (2 * R))) (x : X) : dist (φ x) (holderApprox R t φ x) ≤ (t / 2) ^ defaultτ a * ((2 * 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., on the ball B (z, 2 * R), it is (2 * R) ^ τ times the best Hölder constant of φ, so the Lean statement corresponds to the blueprint statement.

theorem enorm_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) {φ : X → ℂ} (hφ : Function.support φ ⊆ Metric.ball z R) (x : X) : ‖φ x - holderApprox R t φ x‖ₑ ≤ ENNReal.ofReal (t / 2) ^ defaultτ a * iHolENorm φ z (2 * R) (defaultτ a)

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' / (2 * 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' / (2 * 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 lipschitzWith_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 : ℝ} (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) : LipschitzWith (2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - ↑a) * ↑C / (2 * R)).toNNReal (holderApprox R t φ)

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 (2 * R) ≤ 2 ^ (4 * a) * ENNReal.ofReal t ^ (-1 - ↑a) * ↑C

theorem iLipENorm_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 : ℝ} (ht : 0 < t) (h't : t ≤ 1) {φ : X → ℂ} (hφ : Function.support φ ⊆ Metric.ball z R) : iLipENorm (holderApprox R t φ) z (2 * R) ≤ 2 ^ (4 * a) * ENNReal.ofReal t ^ (-1 - ↑a) * iHolENorm φ z (2 * R) (defaultτ a)

noncomputable def C2_0_5 (a : ℝ) : NNReal

The constant occurring in Proposition 2.0.5. Has value 2 ^ (7 * a) in the blueprint.

Equations

• C2_0_5 a = 2 ^ (7 * 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 : ℝ} {φ : X → ℂ} (φ_supp : Function.support φ ⊆ Metric.ball 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 (2 * R) (defaultτ a) * (1 + edist_{z, R} f g) ^ (-(2 * ↑a ^ 2 + ↑a ^ 3)⁻¹)

Proposition 2.0.5.