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

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 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 foobar {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] (f : X → ℝ) : ∫ (x : X), ↑(f x) = ↑(∫ (x : X), f x)

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} (ϕ : X → ℂ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) (h2ϕ : HolderWith C (nnτ X) ϕ) (hτ : 0 < nnτ X) (ht : t ∈ Set.Ioc 0 1) (x : X) : dist (ϕ x) (holderApprox R t ϕ x) ≤ (t * R) ^ defaultτ a * ↑C

Part of Lemma 8.0.1.

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) {C : NNReal} (ϕ : X → ℂ) (hϕ : Function.support ϕ ⊆ Metric.ball z R) (h2ϕ : HolderWith C (nnτ X) ϕ) (ht : t ∈ Set.Ioc 0 1) : LipschitzWith (C8_0_1 ↑a ⟨t, ⋯⟩) (holderApprox R t ϕ)

Part of Lemma 8.0.1.

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ϕ : hnorm ϕ 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) * hnorm ϕ z R * (1 + ↑(nndist f g)) ^ (2 * ↑a ^ 2 + ↑a ^ 3)⁻¹

Proposition 2.0.5.