This should roughly contain the contents of chapter 8.

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

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

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 → ℤ} {σ₂ : X → ℤ} {F : Set X} {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 support_holderApprox_subset {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {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) : 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 → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {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) (x : X) : dist (ϕ x) (holderApprox R t ϕ x) ≤ t ^ defaultτ a * ↑C

Part of Lemma 8.0.1.

theorem lipschitzWith_holderApprox {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {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 → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {z : X} {R : NNReal} (hR : 0 < R) {ϕ : X → ℂ} (hϕ : Function.support ϕ ⊆ Metric.ball z ↑R) (h2ϕ : hnorm ϕ z R < ⊤) {f : Θ X} {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.