Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_pointwise_inversion

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:812 to 869

Source documentation

The single-point truncated-limit inverse Laplace identity at y = log n (\cite{Kadiri2005}, the displayed equation just before eq.~(11)): for φ of class C¹ with the strip decay of (B), and any 0 < a < b with n ≥ 1,

= \lim_{T \to \infty} \frac{1}{2\pi i} \int_{-(1+a)-iT}^{-(1+a)+iT} \Phi(s)\, n^{s}\, ds,$$ with `Φ(s) = ∫ y, φ y e^{-s y}`. This is the truncated-window Fourier/Laplace inversion theorem from `PrimeNumberTheoremAnd.LaplaceInversion`, specialized to the contour `σ = -(1+a)` and the point `x = n` (so `n^s = exp (s log n)`). It discharges the `hinv` hypothesis carried by the eq.~(11) reduction lemmas above.

Exact Lean statement

theorem kadiri_thm_3_1_q1_pointwise_inversion {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)
    {b : ℝ} (hb : 0 < b)
    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))
        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))
    {a : ℝ} (ha : 0 < a) (hab : a < b) :
    ∀ n : Nat, 1 ≤ n →
      let Φ : ℂ → ℂ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem kadiri_thm_3_1_q1_pointwise_inversion {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)    {b : ℝ} (hb : 0 < b)    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    {a : ℝ} (ha : 0 < a) (hab : a < b) :    ∀ n : Nat, 1 ≤ n →      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume      Tendsto        (fun T : ℝ =>          (1 / (2 * (Real.pi : ℂ))) *            ∫ t in (-T)..T,              Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))        atTop (𝓝 (φ (Real.log n))) := by  intro n hn Φ  -- Reduce to the multiplication-form truncated inverse Laplace integral.  have hx : (0 : ℝ) < (n : ℝ) := by exact_mod_cast hn  -- The exponentially weighted source `g y = exp (-(σ y)) φ y` with `σ = -(1+a)`.  set g : ℝ → ℂ :=    fun y : ℝ => exp (-(((-(1 + a) : ℝ) : ℂ) * (y : ℂ))) * φ y with hg_def  have hg_int : Integrable g :=    kadiri_laplace_source_integrable_of_decay      (φ := φ) hφ (b := b) hb hφ_decay (a := a) ha hab  have hgdiff : Differentiable ℝ g :=    kadiri_weighted_source_differentiable (φ := φ) hφ (a := a)  -- Interval integrability of the local difference quotient of `g` at `x = log n`.  have hq : IntervalIntegrable      (fun u : ℝ =>        if u = 0 then 0 else          (1 / (Real.pi * u) : ℂ) • (g (Real.log (n : ℝ) - u) - g (Real.log (n : ℝ))))      volume (-(1 : ℝ)) (1 : ℝ) :=    intervalIntegrable_local_quotient_of_differentiableAt      (E := ℂ) (f := g) (x := Real.log (n : ℝ)) (R := (1 : ℝ)) zero_lt_one      hgdiff.continuous.continuousOn hgdiff.differentiableAt  -- The master truncated-limit inverse Laplace theorem applied with `σ = -(1+a)`,  -- source `φ`, point `x = n`, window radius `R = 1`.  have hmaster :=    laplaceIntegralCpowTrunc_tendsto_of_integrable_local_quotient      (sigma := (-(1 + a) : ℝ)) (f := φ) (x := (n : ℝ)) (R := (1 : ℝ))      hx zero_lt_one hg_int hq  -- The truncated integral defining `hinv` is exactly `laplaceIntegralCpowTrunc`.  have hreindex :      (fun T : ℝ =>        (1 / (2 * (Real.pi : ℂ))) *          ∫ t in (-T)..T,            Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *              (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) =        fun T : ℝ => laplaceIntegralCpowTrunc φ (-(1 + a)) (n : ℝ) T := by    funext T    simp only [Φ, laplaceIntegralCpowTrunc, laplaceIntegral]    congr 1    apply intervalIntegral.integral_congr    intro t _ht    push_cast    ring_nf  -- The target value `φ (log n)` matches the master theorem's `φ (log x)` at `x = n`.  rw [hreindex]  simpa using hmaster