Source indexedtheorem · leanprover/lean4:v4.32.0

MellinOfDeltaSpike

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:663 to 677

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "MellinOfDeltaSpike")
  (statement := /--
  For any $\epsilon>0$, the Mellin transform of $\nu_\epsilon$ is
  $$\mathcal{M}(\nu_\epsilon)(s) = \mathcal{M}(\nu)\left(\epsilon s\right).$$
  -/)
  (proof := /-- Substitute $y=x^{1/\epsilon}$, use Haar measure; direct calculation. -/)]
theorem MellinOfDeltaSpike (ν : ℝ → ℝ) {ε : ℝ} (εpos : ε > 0) (s : ℂ) :
    𝓜 (fun x ↦ (DeltaSpike ν ε x : ℂ)) s = 𝓜 (fun x ↦ (ν x : ℂ)) (ε * s)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "MellinOfDeltaSpike")  (statement := /--  For any $\epsilon>0$, the Mellin transform of $\nu_\epsilon$ is  $$\mathcal{M}(\nu_\epsilon)(s) = \mathcal{M}(\nu)\left(\epsilon s\right).$$  -/)  (proof := /-- Substitute $y=x^{1/\epsilon}$, use Haar measure; direct calculation. -/)]theorem MellinOfDeltaSpike (ν : ℝ → ℝ) {ε : ℝ} (εpos : ε > 0) (s : ℂ) :    𝓜 (fun x ↦ (DeltaSpike ν ε x : ℂ)) s = 𝓜 (fun x ↦ (ν x : ℂ)) (ε * s) := by  unfold DeltaSpike  push_cast  rw [mellin_div_const, mellin_comp_rpow (fun x ↦ (ν x : ℂ)), abs_of_nonneg (by positivity)]  simp only [one_div, inv_inv, ofReal_inv, div_inv_eq_mul, real_smul]  rw [mul_div_cancel_left₀ _ (ne_zero_of_re_pos εpos)]  ring_nf