@[reducible]

def doublingMeasure_real_two : MeasureTheory.DoublingMeasure ℝ 2

Equations

• doublingMeasure_real_two = MeasureTheory.DoublingMeasure.mono doublingMeasure_real_two.proof_2

instance doublingMeasure_real_16 : MeasureTheory.DoublingMeasure ℝ ↑(2 ^ 4)

Equations

• doublingMeasure_real_16 = MeasureTheory.DoublingMeasure.mono doublingMeasure_real_16.proof_2

def modulationOperator (n : ℤ) (g : ℝ → ℂ) (x : ℝ) : ℂ

The modulation operator M_n g, defined in (11.3.1)

Equations

• modulationOperator n g x = g x * Complex.exp (Complex.I * ↑n * ↑x)

def approxHilbertTransform (n : ℕ) (g : ℝ → ℂ) (x : ℝ) : ℂ

The approximate Hilbert transform L_N g, defined in (11.3.2). defined slightly differently.

Equations

• approxHilbertTransform n g x = (↑n)⁻¹ * ∑ k ∈ Finset.Ico n (2 * n), modulationOperator (-↑k) (partialFourierSum k (modulationOperator (↑k) g)) x

def niceKernel (r x : ℝ) : ℝ

The kernel k_r(x) defined in (11.3.11). When used, we may assume that r ∈ Ioo 0 1. Todo: find better name?

Equations

• niceKernel r x = if Complex.exp (Complex.I * ↑x) = 1 then r⁻¹ else r⁻¹ ⊓ (1 + r / Complex.normSq (1 - Complex.exp (Complex.I * ↑x)))

theorem mean_zero_oscillation {n : ℤ} (hn : n ≠ 0) : ∫ (x : ℝ) in 0 ..2 * Real.pi, Complex.exp (Complex.I * ↑n * ↑x) = 0

Lemma 11.1.8

theorem partial_sum_projection {f : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (periodic_f : Function.Periodic f (2 * Real.pi)) {x : ℝ} : partialFourierSum n (partialFourierSum n f) x = partialFourierSum n f x

Lemma 11.5.1 Note: might not be used if we can use spectral_projection_bound_lp below.

theorem partial_sum_selfadjoint {f g : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (periodic_f : Function.Periodic f (2 * Real.pi)) (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (periodic_g : Function.Periodic g (2 * Real.pi)) : ∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (partialFourierSum n f x) * g x = ∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (f x) * partialFourierSum n g x

Lemma 11.5.2. Note: might not be used if we can use spectral_projection_bound_lp below.

theorem spectral_projection_bound {f : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (periodic_f : Function.Periodic f (2 * Real.pi)) : (fun (p : ENNReal) => MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator (partialFourierSum n f)) p MeasureTheory.volume) ≤ fun (p : ENNReal) => MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator f) p MeasureTheory.volume

Lemma 11.1.11. The blueprint states this on [-π, π], but I think we can consistently change this to (0, 2π].

theorem modulated_averaged_projection {g : ℝ → ℂ} {n : ℕ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (periodic_g : Function.Periodic g (2 * Real.pi)) : (fun (p : ENNReal) => MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator (approxHilbertTransform n g)) p MeasureTheory.volume) ≤ fun (p : ENNReal) => MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator g) p MeasureTheory.volume

Lemma 11.3.1. The blueprint states this on [-π, π], but I think we can consistently change this to (0, 2π].

theorem young_convolution {f g : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (periodic_f : Function.Periodic f (2 * Real.pi)) (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (periodic_g : Function.Periodic g (2 * Real.pi)) : MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator fun (x : ℝ) => ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * g (x - y)) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator f) 2 MeasureTheory.volume * MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator g) 1 MeasureTheory.volume

Lemma 11.3.3. The blueprint states this on [-π, π], but I think we can consistently change this to (0, 2π].

Bonus points if you generalize to https://en.wikipedia.org/wiki/Young%27s_convolution_inequality first, using MeasureTheory.convolution from Mathlib. To applying the general version, you have to apply it with functions with AddCircle as domain.

theorem integrable_bump_convolution {f g : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (periodic_f : Function.Periodic f (2 * Real.pi)) (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (periodic_g : Function.Periodic g (2 * Real.pi)) {r : ℝ} (hr : r ∈ Set.Ioo 0 Real.pi) : (∀ (x : ℝ), ‖g x‖ ≤ niceKernel r x) → MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator fun (x : ℝ) => ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * g (x - y)) 2 MeasureTheory.volume ≤ 2 ^ 5 * MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator f) 2 MeasureTheory.volume

Lemma 11.3.4. The blueprint states this on [-π, π], but I think we can consistently change this to (0, 2π].

def dirichletApprox (n : ℕ) (x : ℝ) : ℂ

The function L', defined in the Proof of Lemma 11.3.5.

Equations

• dirichletApprox n x = (↑n)⁻¹ * ∑ k ∈ Finset.Ico n (2 * n), dirichletKernel k x * Complex.exp (-Complex.I * ↑k * ↑x)

theorem continuous_dirichletApprox {n : ℕ} : Continuous (dirichletApprox n)

Lemma 11.3.5, part 1.

theorem periodic_dirichletApprox (n : ℕ) : Function.Periodic (dirichletApprox n) (2 * Real.pi)

Lemma 11.3.5, part 2.

theorem approxHilbertTransform_eq_dirichletApprox {f : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (periodic_f : Function.Periodic f (2 * Real.pi)) {n✝ : ℕ} {x : ℝ} : approxHilbertTransform n✝ f x = ↑(2 * Real.pi)⁻¹ * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletApprox n✝ (x - y)

Lemma 11.3.5, part 3. The blueprint states this on [-π, π], but I think we can consistently change this to (0, 2π].

theorem dist_dirichletApprox_le {f : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (periodic_f : Function.Periodic f (2 * Real.pi)) {r : ℝ} (hr : r ∈ Set.Ioo 0 1) {n✝ : ℕ} (hn : n✝ = ⌈r⁻¹⌉₊) {x : ℝ} : dist (dirichletApprox n✝ x) ({y : ℂ | ‖y‖ ∈ Set.Ioo r 1}.indicator 1 ↑x) ≤ 2 ^ 5 * niceKernel r x

Lemma 11.3.5, part 4. The blueprint states this on [-π, π], but I think we can consistently change this to (0, 2π].

theorem Hilbert_strong_2_2 ⦃r : ℝ⦄ (hr : 0 < r) : MeasureTheory.HasBoundedStrongType (CZOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts 4)