Source indexedlemma · leanprover/lean4:v4.32.0

hasProd_norm_inv_unconditional

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanProductBound.lean:70 to 79

Mathematical statement

Exact Lean statement

lemma hasProd_norm_inv_unconditional {α : Type} {fac : α → ℂ} {F : ℂ}
    (hfac : HasProd fac F (SummationFilter.unconditional α)) (hF : F ≠ 0) :
    HasProd (fun x => ‖(fac x)⁻¹‖) ‖F⁻¹‖ (SummationFilter.unconditional α)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasProd_norm_inv_unconditional {α : Type} {fac : α → ℂ} {F : ℂ}    (hfac : HasProd fac F (SummationFilter.unconditional α)) (hF : F ≠ 0) :    HasProd (fun x => ‖(fac x)⁻¹‖) ‖F⁻¹‖ (SummationFilter.unconditional α) := by  change    Tendsto (fun s : Finset α => ∏ x ∈ s, ‖(fac x)⁻¹‖)      (SummationFilter.unconditional α).filter (𝓝 ‖F⁻¹‖)  have hnorm := (hasProd_inv_unconditional hfac hF).norm  refine hnorm.congr' (Filter.Eventually.of_forall ?_)  intro s  simp [norm_inv, Finset.prod_inv_distrib]