Source indexedlemma · leanprover/lean4:v4.32.0

approxHilbertTransform_eq_dirichletApprox

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:425 to 454

Source documentation

Lemma 11.3.5, part 3.

Exact Lean statement

lemma approxHilbertTransform_eq_dirichletApprox {f : ℝ → ℂ} (hf : MemLp f ∞ volume)
    {n : ℕ} {x : ℝ} :
    approxHilbertTransform n f x =
      (2 * π)⁻¹ * ∫ y in (0)..2 * π, f y * dirichletApprox n (x - y)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma approxHilbertTransform_eq_dirichletApprox {f : ℝ → ℂ} (hf : MemLp f ∞ volume)    {n : ℕ} {x : ℝ} :    approxHilbertTransform n f x =      (2 * π)⁻¹ * ∫ y in (0)..2 * π, f y * dirichletApprox n (x - y) := by  simp only [approxHilbertTransform, Finset.mul_sum, mul_inv_rev, ofReal_mul, ofReal_inv,    ofReal_ofNat, dirichletApprox, ofReal_sub]  rw [intervalIntegral.integral_finsetSum]; swap  · intro i hi    apply IntervalIntegrable.mul_continuousOn ?_ (by fun_prop)    rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp [Real.pi_nonneg])]    exact (hf.restrict _).integrable le_top  simp only [Finset.mul_sum]  congr with i  simp only [modulationOperator, Int.cast_natCast]  rw [partialFourierSum_eq_conv_dirichletKernel]; swap  · apply IntervalIntegrable.mul_continuousOn ?_ (by fun_prop)    rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp [Real.pi_nonneg])]    exact (hf.restrict _).integrable le_top  simp only [one_div, mul_inv_rev]  calc    _ = (↑π)⁻¹ * 2⁻¹ * ((↑n)⁻¹ * cexp (I * ↑i * ↑x) * ∫ (y : ℝ) in 0..2 * π, modulationOperator (-↑i) f y * dirichletKernel i (x - y)) := by      ring    _ = (↑π)⁻¹ * 2⁻¹ * ∫ (y : ℝ) in (0 : ℝ)..2 * π, (↑n : ℂ)⁻¹ * cexp (I * ↑i * ↑x) * (modulationOperator (-↑i) f y * dirichletKernel i (x - y)) := by      congr      exact (intervalIntegral.integral_const_mul _ _).symm    _ = (↑π)⁻¹ * 2⁻¹ * ∫ (x_1 : ℝ) in 0..2 * π, f x_1 * ((↑n)⁻¹ * (dirichletKernel i (x - x_1) * cexp (I * ↑i * (↑x - ↑x_1)))) := by      congr      ext y      simp [modulationOperator, mul_sub, exp_sub, div_eq_inv_mul, exp_neg]      ring