Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_line_weight_differentiable

PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:163 to 171

Mathematical statement

Exact Lean statement

lemma kadiri_laplace_line_weight_differentiable {φ : ℝ → ℂ}
    (hφ : ContDiff ℝ 1 φ) (sigma : ℝ) :
    Differentiable ℝ (fun z : ℝ => exp (-((sigma : ℂ) * (z : ℂ))) * φ z)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_line_weight_differentiable {φ : ℝ → ℂ}    (hφ : ContDiff ℝ 1 φ) (sigma : ℝ) :    Differentiable ℝ (fun z : ℝ => exp (-((sigma : ℂ) * (z : ℂ))) * φ z) := by  intro y  have hofReal : DifferentiableAt ℝ (fun z : ℝ => (z : ℂ)) y :=    Complex.ofRealCLM.differentiable.differentiableAt  have hlin : DifferentiableAt ℝ (fun z : ℝ => -((sigma : ℂ) * (z : ℂ))) y := by    simpa only [neg_mul] using hofReal.const_mul (-(sigma : ℂ))  exact hlin.cexp.mul ((hφ.differentiable (by norm_num)).differentiableAt)