Source indexedlemma · leanprover/lean4:v4.32.0

norm_fourier_le_integral_deriv_div

PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:98 to 123

Source documentation

Fourier-transform decay from an integrable derivative: for integrable, differentiable g with integrable derivative, ‖𝓕 g w‖ ≤ (∫ ‖deriv g x‖) / (2π·|w|).

Exact Lean statement

lemma norm_fourier_le_integral_deriv_div
    (g : ℝ → ℂ) (hg : Integrable g) (hdiff : Differentiable ℝ g)
    (hg' : Integrable (deriv g)) {w : ℝ} (hw : w ≠ 0) :
    ‖𝓕 g w‖ ≤ (∫ x, ‖deriv g x‖ ∂volume) / ((2 * Real.pi) * |w|)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_fourier_le_integral_deriv_div    (g : ℝ → ℂ) (hg : Integrable g) (hdiff : Differentiable ℝ g)    (hg' : Integrable (deriv g)) {w : ℝ} (hw : w ≠ 0) :    ‖𝓕 g w‖ ≤ (∫ x, ‖deriv g x‖ ∂volume) / ((2 * Real.pi) * |w|) := by  have hmul :      𝓕 (deriv g) w = (2 * Real.pi * Complex.I * (w : ℂ)) * 𝓕 g w := by    have h := congrFun (Real.fourier_deriv hg hdiff hg') w    simpa [smul_eq_mul, mul_assoc] using h  have h_fourier :      ‖𝓕 (deriv g) w‖ ≤ ∫ x, ‖deriv g x‖ ∂volume := by    exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 volume (innerₗ ℝ)      (deriv g) w  have hleft :      ((2 * Real.pi) * |w|) * ‖𝓕 g w‖ =        ‖(2 * Real.pi * Complex.I * (w : ℂ)) * 𝓕 g w‖ := by    have htwopi : ‖(2 * ↑Real.pi : ℂ)‖ = 2 * Real.pi := by      rw [norm_mul, Complex.norm_two, Complex.norm_of_nonneg Real.pi_pos.le]    have hwc : ‖(w : ℂ)‖ = |w| := by rw [norm_real, Real.norm_eq_abs]    rw [norm_mul, norm_mul, norm_mul, htwopi, norm_I, hwc]    ring  have hmain : ((2 * Real.pi) * |w|) * ‖𝓕 g w‖ ≤ ∫ x, ‖deriv g x‖ ∂volume := by    rw [hleft, ← hmul]    exact h_fourier  have hpos : 0 < (2 * Real.pi) * |w| := by    positivity  exact (le_div_iff₀ hpos).mpr (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmain)