Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_neg_line_weight_norm_eq

PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:68 to 84

Source documentation

Norm shape of the weighted source: peeling off the exp (x/2) factor.

Exact Lean statement

lemma kadiri_laplace_neg_line_weight_norm_eq {ψ : ℝ → ℂ} (sigma x : ℝ) :
    ‖exp (-((sigma : ℂ) * (x : ℂ))) * ψ x‖ =
      Real.exp (-(sigma + 1 / 2) * x) * ‖ψ x * exp ((x : ℂ) / 2)‖

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_neg_line_weight_norm_eq {ψ : ℝ → ℂ} (sigma x : ℝ) :    ‖exp (-((sigma : ℂ) * (x : ℂ))) * ψ x‖ =      Real.exp (-(sigma + 1 / 2) * x) * ‖ψ x * exp ((x : ℂ) / 2)‖ := by  rw [norm_mul, norm_mul, Complex.norm_exp, Complex.norm_exp]  have h1 : (-(↑sigma * ↑x) : ℂ).re = -sigma * x := by    norm_num [Complex.mul_re]  have h2 : ((x : ℂ) / 2).re = x / 2 := by    norm_num  rw [h1, h2]  calc    Real.exp (-sigma * x) * ‖ψ x‖        = (Real.exp (-(sigma + 1 / 2) * x) * Real.exp (x / 2)) * ‖ψ x‖ := by          rw [← Real.exp_add]          congr 1          ring_nf    _ = Real.exp (-(sigma + 1 / 2) * x) * (‖ψ x‖ * Real.exp (x / 2)) := by          ring_nf