Source indexedlemma · leanprover/lean4:v4.32.0

analyticAt_finset_prod_sub_pow

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:456 to 466

Mathematical statement

Exact Lean statement

lemma analyticAt_finset_prod_sub_pow (s : Finset ℂ) (g : ℂ → ℕ) (w : ℂ) :
    AnalyticAt ℂ (fun z => ∏ ρ ∈ s, (z - ρ) ^ g ρ) w

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma analyticAt_finset_prod_sub_pow (s : Finset ℂ) (g : ℂ → ℕ) (w : ℂ) :    AnalyticAt ℂ (fun z => ∏ ρ ∈ s, (z - ρ) ^ g ρ) w := by  induction s using Finset.induction with  | empty =>    simp only [Finset.prod_empty]    exact analyticAt_const  | @insert a s' hne ih =>    have : (fun z => ∏ ρ ∈ insert a s', (z - ρ) ^ g ρ) = fun z => (z - a) ^ g a * ∏ ρ ∈ s', (z - ρ) ^ g ρ :=      funext fun z => Finset.prod_insert hne    rw [this]    exact ((analyticAt_id.sub analyticAt_const).pow _).mul ih