fpvandoorn/carleson
Source indexedlemma · leanprover/lean4:v4.32.0
norm_czOperator_le_add
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:693 to 758
Source documentation
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] ⊆ [-π, π].
Exact Lean statement
lemma norm_czOperator_le_add
{g : ℝ → ℂ} {r x : ℝ} (hr : r ∈ Ioo 0 1) {n : ℕ} (hn : n = ⌈r⁻¹⌉₊)
(hg : MemLp g ∞ volume)
(hx : 2 ≤ x) (h'x : x ≤ 3)
(h'g : support g ⊆ Icc 1 4) :
‖czOperator K r g x‖ ≤ ‖∫ y in (0)..(2 * π), g y * dirichletApprox n (x - y)‖
+ 12 * ∫ y in Ioc 0 (2 * π), ‖g y‖ * niceKernel r (x - y)Complete declaration
Lean source
Full Lean sourceLean 4
lemma norm_czOperator_le_add {g : ℝ → ℂ} {r x : ℝ} (hr : r ∈ Ioo 0 1) {n : ℕ} (hn : n = ⌈r⁻¹⌉₊) (hg : MemLp g ∞ volume) (hx : 2 ≤ x) (h'x : x ≤ 3) (h'g : support g ⊆ Icc 1 4) : ‖czOperator K r g x‖ ≤ ‖∫ y in (0)..(2 * π), g y * dirichletApprox n (x - y)‖ + 12 * ∫ y in Ioc 0 (2 * π), ‖g y‖ * niceKernel r (x - y) := by have rpos : 0 < r := hr.1 have := Real.pi_gt_three let U := {y : ℝ | |y| ∈ Ico r 1}.indicator k - dirichletApprox n have A : czOperator K r g x = ∫ y in Ioc 0 (2 * π), g y * {y : ℝ | |y| ∈ Ico r 1}.indicator k (x - y) := by simp only [czOperator, K, mul_comm] rw [← integral_indicator measurableSet_ball.compl] rw [← integral_indicator measurableSet_Ioc] congr with y rw [indicator_mul_right, indicator_mul_left] congr 1 · simp only [indicator, mem_Ioc, left_eq_ite_iff] intro h contrapose! h exact ⟨by linarith [(h'g h).1, (h'g h).2], by linarith [(h'g h).1, (h'g h).2]⟩ · simp only [indicator, mem_compl_iff, Metric.mem_ball, dist_eq_norm, Real.norm_eq_abs, abs_sub_comm, not_lt, mem_Ico, mem_setOf_eq] by_cases h : r ≤ |x - y| · simpa only [↓reduceIte, h, true_and, left_eq_ite_iff, not_lt] using k_of_one_le_abs simp [h] have B : {y : ℝ | |y| ∈ Ico r 1}.indicator k = dirichletApprox n + U := by simp [U] simp only [A, B, Pi.add_apply, mul_add] have I0 : IntegrableOn (fun y ↦ ‖g y‖ * niceKernel r (x - y)) (Ioc 0 (2 * π)) := by apply (MemLp.restrict _ _).integrable le_top apply MemLp.mul (q := ⊤) (p := ⊤) _ hg.norm · suffices A : MemLp (niceKernel r) ⊤ volume from A.comp_measurePreserving (Measure.measurePreserving_sub_left volume x) apply memLp_top_of_bound (by fun_prop) (r⁻¹) (Eventually.of_forall (fun y ↦ ?_)) simp [abs_of_nonneg (niceKernel_pos hr.1).le, niceKernel_le_inv] have J (y) : ‖g y * U (x - y)‖ ≤ 12 * (‖g y‖ * niceKernel r (x - y)) := by rcases eq_or_ne (g y) 0 with hy | hy · simp [hy] simp only [norm_mul] rw [mul_comm 12, mul_assoc, mul_comm _ 12] gcongr simp only [U, Pi.sub_apply, ← dist_eq_norm] rw [dist_comm] apply dist_dirichletApprox_le hr hn _ exact ⟨by linarith [(h'g hy).1, (h'g hy).2], by linarith [(h'g hy).1, (h'g hy).2]⟩ have I1 : IntegrableOn (fun y ↦ g y * U (x - y)) (Ioc 0 (2 * π)) := by apply (I0.const_mul 12).mono · apply (hg.restrict _).aestronglyMeasurable.mul apply AEStronglyMeasurable.restrict apply AEStronglyMeasurable.comp_measurePreserving ?_ (Measure.measurePreserving_sub_left volume x) apply AEStronglyMeasurable.sub ?_ (by fun_prop) exact AEStronglyMeasurable.indicator (by fun_prop) (measurable_norm measurableSet_Ico) · filter_upwards [self_mem_ae_restrict measurableSet_Ioc] with y h'y simpa [abs_of_nonneg (niceKernel_pos hr.1).le] using J y rw [integral_add _ I1]; rotate_left · rw [restrict_Ioc_eq_restrict_Icc] exact IntegrableOn.mul_continuousOn ((hg.restrict _).integrable le_top ) (by fun_prop) isCompact_Icc apply (norm_add_le _ _).trans rw [intervalIntegral.integral_of_le (by linarith)] gcongr apply (norm_integral_le_integral_norm _).trans rw [← integral_const_mul] exact setIntegral_mono_on I1.norm (I0.const_mul _) measurableSet_Ioc (fun y hy ↦ J y)