Improve `Multipliable.inv` / `inv₀` docstrings for `ℂ` (and add `tprod_one_add_ne_zero_of_summable` cross-reference

Description:

Inverting infinite products over ℂ is non-obvious and easy to get wrong:

• Multipliable.inv requires [CommGroup ℂ], which doesn't exist. The failure surfaces as a ~18s heartbeat timeout, not a missing-instance error, so it looks like a performance problem.
• Multipliable.inv₀ exists, but requires proving the tprod limit itself is nonzero, not just each factor. This is not obvious from the signature.
• The missing piece is tprod_one_add_ne_zero_of_summable, which is not discoverable from either docstring.

Failing version (times out):

import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.NumberTheory.SumPrimeReciprocals
import Mathlib.Analysis.SpecialFunctions.Log.Summable

open Nat Complex Finset BigOperators
open scoped Topology

noncomputable def quantumMass (p : ℕ) : ℕ := p * (p - 1)

axiom summable_quantumMass_abs_series {s : ℂ} (hs : 1 / 2 < s.re) :
    Summable (fun p : Nat.Primes => ‖(quantumMass p : ℂ) ^ (-s)‖)

example {s : ℂ} (hs : 1 / 2 < s.re) :
    Multipliable (fun p : Nat.Primes => ((1 : ℂ) - (quantumMass p : ℂ) ^ (-s))⁻¹)
      (L := SummationFilter.unconditional Nat.Primes) := by
  have h_sum := summable_quantumMass_abs_series hs
  have h_neg_norm : Summable (fun p : Nat.Primes => ‖-((quantumMass p : ℂ) ^ (-s))‖) := by
    simpa only [norm_neg] using h_sum
  have h_mult : Multipliable (fun p : Nat.Primes => 1 + (-((quantumMass p : ℂ) ^ (-s))))
      (L := SummationFilter.unconditional Nat.Primes) :=
    multipliable_one_add_of_summable h_neg_norm
  have h_eq : (fun p : Nat.Primes => 1 + (-((quantumMass p : ℂ) ^ (-s)))) =
              (fun p : Nat.Primes => 1 - (quantumMass p : ℂ) ^ (-s)) := by
    funext p; ring
  rw [h_eq] at h_mult
  exact h_mult.inv
  -- error: (deterministic) timeout at `whnf`,
  -- maximum number of heartbeats (200000) has been reached

Working version:

theorem quantumMassZeta_converges {s : ℂ} (hs : 1 / 2 < s.re) :
    Multipliable (fun p : Nat.Primes => ((1 : ℂ) - (quantumMass p : ℂ) ^ (-s))⁻¹)
      (L := SummationFilter.unconditional Nat.Primes) := by
  have h_sum := summable_quantumMass_abs_series hs
  have h_neg_norm : Summable (fun p : Nat.Primes => ‖-((quantumMass p : ℂ) ^ (-s))‖) := by
    simpa only [norm_neg] using h_sum
  have h_mult : Multipliable (fun p : Nat.Primes => 1 + (-((quantumMass p : ℂ) ^ (-s))))
      (L := SummationFilter.unconditional Nat.Primes) :=
    multipliable_one_add_of_summable h_neg_norm
  have h_ne : ∀ p : Nat.Primes, 1 + (-((quantumMass p : ℂ) ^ (-s))) ≠ 0 := by
    intro p h
    have hz : (quantumMass p : ℂ) ^ (-s) = 1 := by
      rw [add_eq_zero_iff_eq_neg] at h
      simpa using h.symm
    have hp2 : 2 ≤ (p : ℕ) := Nat.Prime.two_le p.prop
    have h_qm_ge_nat : 2 ≤ quantumMass (p : ℕ) := by
      unfold quantumMass
      have h1 : 1 ≤ (p : ℕ) - 1 := by omega
      nlinarith
    have h_qm_ge : (2 : ℝ) ≤ quantumMass (p : ℕ) := by exact_mod_cast h_qm_ge_nat
    have h_pos : (0 : ℝ) < quantumMass (p : ℕ) := by linarith
    have h_norm : ‖(quantumMass p : ℂ) ^ (-s)‖ = (quantumMass (p : ℕ) : ℝ) ^ (-s.re) := by
      simpa [Complex.ofReal_natCast] using Complex.norm_cpow_eq_rpow_re_of_pos h_pos (-s)
    rw [hz, norm_one] at h_norm
    have h_lt : (quantumMass (p : ℕ) : ℝ) ^ (-s.re) < 1 := by
      have h2 : (quantumMass (p : ℕ) : ℝ) ^ (-s.re) ≤ (2 : ℝ) ^ (-s.re) := by
        apply Real.rpow_le_rpow_of_nonpos (by norm_num) h_qm_ge
        linarith [hs]
      have h3 : (2 : ℝ) ^ (-s.re) < 1 := by
        rw [show (1 : ℝ) = (2 : ℝ) ^ (0 : ℝ) by norm_num]
        exact Real.rpow_lt_rpow_of_exponent_lt (by norm_num) (by linarith [hs])
      linarith
    linarith
  have h_tprod_ne : ∏' p : Nat.Primes, (1 + (-((quantumMass p : ℂ) ^ (-s)))) ≠ 0 :=
    tprod_one_add_ne_zero_of_summable h_ne h_neg_norm
  have h_eq : (fun p : Nat.Primes => 1 + (-((quantumMass p : ℂ) ^ (-s)))) =
              (fun p : Nat.Primes => 1 - (quantumMass p : ℂ) ^ (-s)) := by
    funext p; ring
  rw [h_eq] at h_mult h_tprod_ne
  exact h_mult.inv₀ h_tprod_ne

Version:

Lean: 4.34.0-rc2 (commit 6a10ac8c22beadecabdbb0919c2b50214762f91d)
Mathlib: 85e3a25e006c35636f0e53b0e9296caca2685bc0

Suggested improvements:

1. Add to Multipliable.inv docstring: "Requires [CommGroup α]. For ℂ/ℝ, use Multipliable.inv₀ with a nonzero-limit hypothesis."
2. Add to Multipliable.inv₀ docstring a cross-reference to tprod_one_add_ne_zero_of_summable.
3. Consider a convenience lemma for the common case: given Summable (fun i => ‖f i‖) and ‖f i‖ < 1, conclude Multipliable (fun i => (1 - f i)⁻¹).

Happy to submit a PR for the docstring updates if that's useful.

Locate the Multipliable.inv and Multipliable.inv₀ declarations and read their existing docstrings, then check the tprod_one_add_ne_zero_of_summable declaration for the intended cross-reference. Update the two docstrings with the stated requirements and reference, and verify the documentation changes compile; the optional convenience lemma is separate design work.