Source indexedlemma · leanprover/lean4:v4.32.0

norm_oscillatory_integral_le_integral_deriv_div_abs

PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:159 to 186

Source documentation

The |T| variant of the oscillatory-integral decay bound: for T ≠ 0, ‖∫ g y · exp(T·i·y)‖ ≤ (∫ ‖deriv g x‖) / |T|.

Exact Lean statement

lemma norm_oscillatory_integral_le_integral_deriv_div_abs
    (g : ℝ → ℂ) (hg : Integrable g) (hdiff : Differentiable ℝ g)
    (hg' : Integrable (deriv g)) {T : ℝ} (hT : T ≠ 0) :
    ‖∫ y, g y * exp ((T : ℂ) * Complex.I * (y : ℂ)) ∂volume‖ ≤
      (∫ x, ‖deriv g x‖ ∂volume) / |T|

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_oscillatory_integral_le_integral_deriv_div_abs    (g : ℝ → ℂ) (hg : Integrable g) (hdiff : Differentiable ℝ g)    (hg' : Integrable (deriv g)) {T : ℝ} (hT : T ≠ 0) :    ‖∫ y, g y * exp ((T : ℂ) * Complex.I * (y : ℂ)) ∂volume‖ ≤      (∫ x, ‖deriv g x‖ ∂volume) / |T| := by  have hw : -T / (2 * Real.pi) ≠ 0 := by    exact div_ne_zero (neg_ne_zero.mpr hT) (mul_ne_zero two_ne_zero Real.pi_ne_zero)  have hfourier := norm_fourier_le_integral_deriv_div g hg hdiff hg' hw  have heq :      (∫ y, g y * exp ((T : ℂ) * Complex.I * (y : ℂ)) ∂volume) =        𝓕 g (-T / (2 * Real.pi)) := by    rw [Real.fourier_real_eq_integral_exp_smul]    apply integral_congr_ae    filter_upwards with y    rw [smul_eq_mul]    rw [mul_comm (g y)]    congr 1    congr 1    push_cast    field_simp [Real.pi_ne_zero]  rw [heq]  refine hfourier.trans_eq ?_  congr 1  have hden : (2 * Real.pi) * |-T / (2 * Real.pi)| = |T| := by    have htwopi_pos : 0 < 2 * Real.pi := by positivity    rw [abs_div, abs_neg, abs_of_pos htwopi_pos]    field_simp [Real.pi_ne_zero]  rw [hden]