Source indexedlemma · leanprover/lean4:v4.32.0

norm_oscillatory_integral_le_integral_deriv_div

PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:127 to 155

Source documentation

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

Exact Lean statement

lemma norm_oscillatory_integral_le_integral_deriv_div
    (g : ℝ → ℂ) (hg : Integrable g) (hdiff : Differentiable ℝ g)
    (hg' : Integrable (deriv g)) {T : ℝ} (hT : 0 < T) :
    ‖∫ 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    (g : ℝ → ℂ) (hg : Integrable g) (hdiff : Differentiable ℝ g)    (hg' : Integrable (deriv g)) {T : ℝ} (hT : 0 < T) :    ‖∫ 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.ne') (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    have hneg : -T / (2 * Real.pi) < 0 := div_neg_of_neg_of_pos (neg_neg_of_pos hT) htwopi_pos    rw [abs_of_neg hneg]    field_simp [Real.pi_ne_zero]  rw [hden]