@[reducible]

noncomputable def doublingMeasure_real_two : MeasureTheory.DoublingMeasure ℝ 2

The volume measure on the real line is doubling.

Equations

• doublingMeasure_real_two = MeasureTheory.DoublingMeasure.mono doublingMeasure_real_two._proof_1

@[instance_reducible]

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

Equations

• doublingMeasure_real_16 = MeasureTheory.DoublingMeasure.mono doublingMeasure_real_16._proof_1

theorem czOperator_comp_add {g k : ℝ → ℂ} {r a : ℝ} : (czOperator (fun (x y : ℝ) => k (x - y)) r g ∘ fun (x : ℝ) => x + a) = czOperator (fun (x y : ℝ) => k (x - y)) r (g ∘ fun (x : ℝ) => x + a)

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

theorem Measurable.modulationOperator (n : ℤ) {g : ℝ → ℂ} (hg : Measurable g) : Measurable (_root_.modulationOperator n g)

theorem AEMeasurable.modulationOperator (n : ℤ) {g : ℝ → ℂ} (hg : AEMeasurable g MeasureTheory.volume) : AEMeasurable (_root_.modulationOperator n g) MeasureTheory.volume

noncomputable 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

noncomputable 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 min r⁻¹ (1 + r / Complex.normSq (1 - Complex.exp (Complex.I * ↑x)))

theorem niceKernel_pos {r x : ℝ} (hr : 0 < r) : 0 < niceKernel r x

theorem niceKernel_le_inv {r x : ℝ} : niceKernel r x ≤ r⁻¹

theorem one_le_niceKernel {r x : ℝ} (hr : 0 < r) (h'r : r < 1) : 1 ≤ niceKernel r x

theorem niceKernel_neg {r x : ℝ} : niceKernel r (-x) = niceKernel r x

theorem niceKernel_periodic (r : ℝ) : Function.Periodic (niceKernel r) (2 * Real.pi)

theorem measurable_niceKernel {r : ℝ} : Measurable (niceKernel r)

theorem niceKernel_intervalIntegrable {r : ℝ} (a b : ℝ) (hr : r > 0) : IntervalIntegrable (niceKernel r) MeasureTheory.volume a b

theorem niceKernel_eq_inv {r x : ℝ} (hr : 0 < r ∧ r < Real.pi) (hx : 0 ≤ x ∧ x ≤ r) : niceKernel r x = r⁻¹

theorem niceKernel_eq_inv' {r x : ℝ} (hr : 0 < r ∧ r < Real.pi) (hx : |x| ≤ r) : niceKernel r x = r⁻¹

theorem niceKernel_upperBound_aux {r x : ℝ} (hr : 0 < r) (hx : r ≤ x ∧ x ≤ Real.pi) : 1 + r / ‖1 - Complex.exp (Complex.I * ↑x)‖ ^ 2 ≤ 1 + 4 * r / x ^ 2

theorem niceKernel_upperBound {r x : ℝ} (hr : 0 < r) (hx : r ≤ x ∧ x ≤ Real.pi) : niceKernel r x ≤ 1 + 4 * r / x ^ 2

theorem niceKernel_lowerBound {r x : ℝ} (hr : 0 < r) (h'r : r < 1) (hx : r ≤ x ∧ x ≤ Real.pi) : 1 + r / ‖1 - Complex.exp (Complex.I * ↑x)‖ ^ 2 ≤ 5 * niceKernel r x

theorem niceKernel_lowerBound' {r x : ℝ} (hr : 0 < r) (h'r : r < 1) (hx : r ≤ |x| ∧ |x| ≤ Real.pi) : 1 + r / ‖1 - Complex.exp (Complex.I * ↑x)‖ ^ 2 ≤ 5 * niceKernel r 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 AddCircle.haarAddCircle_eq_smul_volume {T : ℝ} [hT : Fact (0 < T)] : haarAddCircle = (ENNReal.ofReal T)⁻¹ • MeasureTheory.volume

theorem instFactLtRealOfNatHMulPi_carleson_2 : Fact (0 < 2 * Real.pi)

theorem spectral_projection_bound {f : ℝ → ℂ} {n : ℕ} (hmf : AEMeasurable f MeasureTheory.volume) : MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator (partialFourierSum n f)) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator f) 2 MeasureTheory.volume

Lemma 11.1.10.

theorem modulated_averaged_projection {g : ℝ → ℂ} {n : ℕ} (hmg : AEMeasurable g MeasureTheory.volume) : MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator (approxHilbertTransform n g)) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm ((Set.Ioc 0 (2 * Real.pi)).indicator g) 2 MeasureTheory.volume

Lemma 11.3.1.

theorem modulated_averaged_projection' {g : ℝ → ℂ} {n : ℕ} (hmg : AEMeasurable g MeasureTheory.volume) : MeasureTheory.eLpNorm (approxHilbertTransform n g) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ MeasureTheory.eLpNorm g 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))

theorem instFactLtRealOfNatHMulPi_carleson_3 : Fact (0 < 2 * Real.pi)

theorem young_convolution {f g : ℝ → ℝ} (hmf : AEMeasurable f MeasureTheory.volume) (hmg : AEMeasurable g MeasureTheory.volume) (periodic_g : Function.Periodic g (2 * Real.pi)) : MeasureTheory.eLpNorm (fun (x : ℝ) => ∫ (y : ℝ) in 0..2 * Real.pi, f y * g (x - y)) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) * MeasureTheory.eLpNorm g 1 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))

Lemma 11.3.3.

theorem integrable_bump_convolution {f g : ℝ → ℝ} (hf : MeasureTheory.MemLp f ⊤ MeasureTheory.volume) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) (periodic_g : Function.Periodic g (2 * Real.pi)) {r : ℝ} (hr : r ∈ Set.Ioo 0 Real.pi) (hle : ∀ (x : ℝ), |g x| ≤ niceKernel r x) : MeasureTheory.eLpNorm (fun (x : ℝ) => ∫ (y : ℝ) in 0..2 * Real.pi, f y * g (x - y)) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ 17 * MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))

Lemma 11.3.4.

noncomputable 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 norm_dirichletApprox_le {n : ℕ} {x : ℝ} : ‖dirichletApprox n x‖ ≤ 4 * ↑n

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

Lemma 11.3.5, part 2.

theorem approxHilbertTransform_eq_dirichletApprox {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f ⊤ MeasureTheory.volume) {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.

theorem eLpNorm_convolution_dirichletApprox {g : ℝ → ℂ} {n : ℕ} (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (x : ℝ) => ∫ (y : ℝ) in 0..2 * Real.pi, g y * dirichletApprox n (x - y)) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ 7 * MeasureTheory.eLpNorm g 2 (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))

The convolution with dirichletApprox is controlled on (0, 2π] in L^2 norm. This follows from the fact that it coincides (up to a constant) with approxHilbertTransform, which is essentially an average of Fourier projections (which are all contractions in L^2).

noncomputable def dirichletApproxAux (n : ℕ) (x : ℝ) : ℂ

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

Equations

• dirichletApproxAux n x = (↑n)⁻¹ * Complex.exp (Complex.I * 2 * ↑n * ↑x) / (1 - Complex.exp (-Complex.I * ↑x)) * ∑ k ∈ Finset.Ico 0 n, Complex.exp (Complex.I * 2 * ↑k * ↑x)

theorem dirichletApprox_eq_add_dirichletApproxAux {n : ℕ} {x : ℝ} (hx : Complex.exp (Complex.I * ↑x) ≠ 1) (hn : n ≠ 0) : dirichletApprox n x = (1 - Complex.exp (Complex.I * ↑x))⁻¹ + dirichletApproxAux n x

theorem norm_dirichletApproxAux_le_of_re_nonneg {n : ℕ} {x r : ℝ} (hx : Complex.exp (Complex.I * ↑x) ≠ 1) (h'x : 0 ≤ (Complex.exp (Complex.I * ↑x)).re) (hn : r⁻¹ ≤ ↑n) (hr : 0 < r) : ‖dirichletApproxAux n x‖ ≤ 2 * (1 + r / ‖1 - Complex.exp (Complex.I * ↑x)‖ ^ 2)

theorem norm_dirichletApproxAux_le_of_re_nonpos {n : ℕ} {x r : ℝ} (h'x : (Complex.exp (Complex.I * ↑x)).re ≤ 0) (hr : 0 < r) : ‖dirichletApproxAux n x‖ ≤ 2 * (1 + r / ‖1 - Complex.exp (Complex.I * ↑x)‖ ^ 2)

theorem norm_dirichletApproxAux_le {n : ℕ} {x r : ℝ} (hx : Complex.exp (Complex.I * ↑x) ≠ 1) (hxr : r ≤ |x|) (hxpi : |x| ≤ Real.pi) (hn : r⁻¹ ≤ ↑n) (hr : 0 < r) (h'r : r < 1) : ‖dirichletApproxAux n x‖ ≤ 10 * niceKernel r x

theorem norm_sub_indicator_k {x r : ℝ} (hxr : r ≤ |x|) (hxpi : |x| ≤ Real.pi) (hr : 0 < r) (h'r : r < 1) : ‖(1 - Complex.exp (Complex.I * ↑x))⁻¹ - {y : ℝ | |y| ∈ Set.Ico r 1}.indicator k x‖ ≤ 2 * niceKernel r x

theorem dist_dirichletApprox_le {r : ℝ} (hr : r ∈ Set.Ioo 0 1) {n : ℕ} (hn : n = ⌈r⁻¹⌉₊) {x : ℝ} (hx : x ∈ Set.Icc (-Real.pi) Real.pi) : dist (dirichletApprox n x) ({y : ℝ | |y| ∈ Set.Ico r 1}.indicator k x) ≤ 12 * niceKernel r x

Lemma 11.3.5, part 4.

The kernel dirichletApprox approximates well the kernel of the Hilbert transform, on [-π, π], up to an error which is uniformly bounded in L^1 (as it is bounded by a constant multiple of niceKernel).

theorem norm_czOperator_le_add {g : ℝ → ℂ} {r x : ℝ} (hr : r ∈ Set.Ioo 0 1) {n : ℕ} (hn : n = ⌈r⁻¹⌉₊) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) (hx : 2 ≤ x) (h'x : x ≤ 3) (h'g : Function.support g ⊆ Set.Icc 1 4) : ‖czOperator K r g x‖ ≤ ‖∫ (y : ℝ) in 0..2 * Real.pi, g y * dirichletApprox n (x - y)‖ + 12 * ∫ (y : ℝ) in Set.Ioc 0 (2 * Real.pi), ‖g y‖ * niceKernel r (x - y)

As the kernel of the Hilbert transform is well approximated by dirichletApprox, up to an error controlled by 12 * niceKernel r, we may bound czOperator K in terms of these. As the approximation only works in the interval [-π, π], this statement is only true for a point x in [2, 3] and a function supported in [1, 4], as this means all values of the approximation that will show up will be in [-2, 2] ⊆ [-π, π].

theorem eLpNorm_czOperator_restrict_two_three_of_support_subset {g : ℝ → ℂ} {r : ℝ} (hr : r ∈ Set.Ioo 0 1) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) (h'g : Function.support g ⊆ Set.Icc 1 4) : MeasureTheory.eLpNorm (czOperator K r g) 2 (MeasureTheory.volume.restrict (Set.Ioc 2 3)) ≤ 2 ^ 8 * MeasureTheory.eLpNorm g 2 (MeasureTheory.volume.restrict (Set.Ioc 1 4))

The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]), uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is bounded by the sum of two operators which are both bounded: one is the convolution with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has a kernel uniformly bounded in L^1 and is therefore controlled by Young inequality.

In this version, we assume that the function is supported in [1, 4], but we will drop this assumption just after this lemma, in eLpNorm_czOperator_restrict_two_three.

theorem eLpNorm_czOperator_restrict_two_three {g : ℝ → ℂ} {r : ℝ} (hr : r ∈ Set.Ioo 0 1) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) : MeasureTheory.eLpNorm (czOperator K r g) 2 (MeasureTheory.volume.restrict (Set.Ioc 2 3)) ≤ 2 ^ 8 * MeasureTheory.eLpNorm g 2 (MeasureTheory.volume.restrict (Set.Ioc 1 4))

The operator czOperator K r is bounded from L^2 [1, 4] to L^2 [2, 3], uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is bounded by the sum of two operators which are both bounded: one is the convolution with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has a kernel uniformly bounded in L^1 and is therefore controlled by Young inequality.

theorem eLpNorm_czOperator_restrict {g : ℝ → ℂ} {r a : ℝ} (hr : r ∈ Set.Ioo 0 1) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) : MeasureTheory.eLpNorm (czOperator K r g) 2 (MeasureTheory.volume.restrict (Set.Ioc a (a + 1))) ≤ 2 ^ 8 * MeasureTheory.eLpNorm g 2 (MeasureTheory.volume.restrict (Set.Ioc (a - 1) (a + 2)))

The operator czOperator K r is bounded from L^2 [a - 1, a + 2] to L^2 [a, a + 1], uniformly in r and a. This follows from the same fact from L^2 [1, 4] to L^2 [2, 3] proved using Fourier series, and translation invariance.

theorem eLpNorm_czOperator_sq {g : ℝ → ℂ} {r : ℝ} (hr : r ∈ Set.Ioo 0 1) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) : MeasureTheory.eLpNorm (czOperator K r g) 2 MeasureTheory.volume ^ 2 ≤ 2 ^ 18 * MeasureTheory.eLpNorm g 2 MeasureTheory.volume ^ 2

theorem eLpNorm_czOperator {g : ℝ → ℂ} {r : ℝ} (hr : 0 < r) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) : MeasureTheory.eLpNorm (czOperator K r g) 2 MeasureTheory.volume ≤ 2 ^ 9 * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

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