Source indexedlemma · leanprover/lean4:v4.32.0

first_fourier

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:110 to 163

Mathematical statement

Exact Lean statement

@[blueprint "first-fourier"
  (title := "first-fourier")
  (statement := /--
  If $\psi: \R \to \C$ is integrable and $x > 0$, then for any $\sigma>1$
  $$ \sum_{n=1}^\infty \frac{f(n)}{n^\sigma} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) =
  \int_\R F(\sigma + it) \psi(t) x^{it}\ dt.$$
  -/)
  (proof := /--
    By the definition of the Fourier transform, the left-hand side expands as
  $$ \sum_{n=1}^\infty \int_\R \frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log
  \frac{n}{x})\ dt$$
  while the right-hand side expands as
  $$ \int_\R \sum_{n=1}^\infty \frac{f(n)}{n^{\sigma+it}} \psi(t) x^{it}\ dt.$$
  Since
  $$\frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log \frac{n}{x}) =
  \frac{f(n)}{n^{\sigma+it}} \psi(t) x^{it}$$
  the claim then follows from Fubini's theorem.
  -/)
  (latexEnv := "lemma")]
lemma first_fourier (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))
    (hsupp : Integrable ψ) (hx : 0 < x) (hσ : 1 < σ') :
    ∑' n : ℕ, term f σ' n * (𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x))) =
    ∫ t : ℝ, LSeries f (σ' + t * I) * ψ t * x ^ (t * I)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "first-fourier"  (title := "first-fourier")  (statement := /--  If $\psi: \R \to \C$ is integrable and $x > 0$, then for any $\sigma>1$  $$ \sum_{n=1}^\infty \frac{f(n)}{n^\sigma} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) =  \int_\R F(\sigma + it) \psi(t) x^{it}\ dt.$$  -/)  (proof := /--    By the definition of the Fourier transform, the left-hand side expands as  $$ \sum_{n=1}^\infty \int_\R \frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log  \frac{n}{x})\ dt$$  while the right-hand side expands as  $$ \int_\R \sum_{n=1}^\infty \frac{f(n)}{n^{\sigma+it}} \psi(t) x^{it}\ dt.$$  Since  $$\frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log \frac{n}{x}) =  \frac{f(n)}{n^{\sigma+it}} \psi(t) x^{it}$$  the claim then follows from Fubini's theorem.  -/)  (latexEnv := "lemma")]lemma first_fourier (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))    (hsupp : Integrable ψ) (hx : 0 < x) (hσ : 1 < σ') :    ∑' n : ℕ, term f σ' n * (𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x))) =    ∫ t : ℝ, LSeries f (σ' + t * I) * ψ t * x ^ (t * I) := by   calc    _ = ∑' n, term f σ' n * ∫ (v : ℝ), 𝐞 (-(v * ((1 : ℝ) /        ((2 : ℝ) * π) * Real.log (n / x)))) • ψ v := by      simp only [Real.fourier_eq]      simp only [one_div, mul_inv_rev, RCLike.inner_apply', conj_trivial]    _ = ∑' n, ∫ (v : ℝ), term f σ' n * 𝐞 (-(v * ((1 : ℝ) /        ((2 : ℝ) * π) * Real.log (n / x)))) • ψ v := by      simp [integral_const_mul]    _ = ∫ (v : ℝ), ∑' n, term f σ' n * 𝐞 (-(v * ((1 : ℝ) /        ((2 : ℝ) * π) * Real.log (n / x)))) • ψ v := by      refine (integral_tsum ?_ ?_).symm      · refine fun _ ↦ AEMeasurable.aestronglyMeasurable ?_        have := hsupp.aemeasurable        fun_prop      · simp only [enorm_mul]        simp_rw [lintegral_const_mul'' _ (first_fourier_aux1 hsupp.aemeasurable _)]        calc          _ = (∑' (i : ℕ), ‖term f σ' i‖ₑ) * ∫⁻ (a : ℝ), ‖ψ a‖ₑ ∂volume := by            simp [ENNReal.tsum_mul_right, enorm_eq_nnnorm]          _ ≠ ⊤ := ENNReal.mul_ne_top (hf_coe1 hf hσ)            (ne_top_of_lt hsupp.2)    _ = _ := by      congr 1; ext y      simp_rw [mul_assoc (LSeries _ _), ← smul_eq_mul (a := (LSeries _ _)), LSeries]      rw [← Summable.tsum_smul_const]      · simp_rw [first_fourier_aux2 hx]      · apply Summable.of_norm        convert hf σ' hσ with n        rw [norm_term_eq_nterm_re]        simp