Source indexedlemma · leanprover/lean4:v4.32.0

hasProd_inv_unconditional

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanProductBound.lean:52 to 68

Mathematical statement

Exact Lean statement

lemma hasProd_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_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 hprod :      Tendsto (fun s : Finset α => ∏ x ∈ s, fac x)        (SummationFilter.unconditional α).filter (𝓝 F) := by    simpa [HasProd] using hfac  have hinv :      Tendsto (fun s : Finset α => (∏ x ∈ s, fac x)⁻¹)        (SummationFilter.unconditional α).filter (𝓝 (F⁻¹)) :=    hprod.inv₀ hF  refine hinv.congr' (Filter.Eventually.of_forall ?_)  intro s  simp [Finset.prod_inv_distrib]