Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.analyticOrderNatAt_comp_add_const

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:47 to 58

Source documentation

Translating the input moves the origin order to the order at the translation center.

Exact Lean statement

lemma analyticOrderNatAt_comp_add_const (f : ℂ → ℂ) (c : ℂ) :
    analyticOrderNatAt (fun w : ℂ => f (w + c)) 0 = analyticOrderNatAt f c

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma analyticOrderNatAt_comp_add_const (f : ℂ → ℂ) (c : ℂ) :    analyticOrderNatAt (fun w : ℂ => f (w + c)) 0 = analyticOrderNatAt f c := by  let g : ℂ → ℂ := fun w => w + c  have hg : AnalyticAt ℂ g 0 := by fun_prop  have hg' : deriv g 0 ≠ 0 := by    simp [g]  have h :=    analyticOrderAt_comp_of_deriv_ne_zero (f := f) (g := g) (z₀ := (0 : ℂ)) hg hg'  have h' :      analyticOrderAt ((fun x : ℂ => f x) ∘ g) 0 = analyticOrderAt f c := by    simpa [g] using h  simpa [analyticOrderNatAt, g] using! congrArg ENat.toNat h'