Product Rules (Generalized Distributive Laws) for Infinite Products

This file formalizes the product rules for expanding products of sums, both finite and infinite, following the treatment in the AlgebraicCombinatorics book.

Main definitions

• EssentiallyFinite: A family (k_i)_{i ∈ I} is essentially finite if all but finitely many i ∈ I satisfy k_i = 0. This is used to describe which terms appear when expanding infinite products of sums.

Main results

Finite Product Rules

• prod_sum_eq_sum_prod_finset: (Proposition prop.fps.prodrule-fin-fin) A finite product of finite sums equals a sum over the Cartesian product of the index sets.
• prod_tsum_eq_tsum_prod_finset: (Proposition prop.fps.prodrule-fin-inf) A finite product of infinite summable families equals a sum over the Cartesian product.

Infinite Product Rules

• tprod_tsum_eq_tsum_prod_essentiallyFinite_nat: (Proposition prop.fps.prodrule-inf-infN) An infinite product of sums (indexed by positive integers) equals a sum over essentially finite sequences.
• tprod_tsum_eq_tsum_prod_essentiallyFinite: (Proposition prop.fps.prodrule-inf-inf) General version with arbitrary index set I.

Applications

• euler_odd_parts_identity: (Proposition prop.gf.prod.euler-odd) Euler's identity: ∏_{i>0} (1 - x^{2i-1})⁻¹ = ∏_{k>0} (1 + x^k)
• euler_distinct_odd_partitions: (Theorem thm.gf.prod.euler-comb) The number of partitions of n into distinct parts equals the number of partitions into odd parts.

Substitution

• tprod_rescale_substitution: (Proposition prop.fps.subs.rule-infprod) Infinite products commute with rescaling (a special case of substitution).

Exp/Log

The source material includes Propositions prop.fps.Exp-Log-infsum and prop.fps.Exp-Log-infprod relating infinite sums/products via Exp and Log maps. The canonical definitions for FPS with constant term 0 or 1 (PowerSeries₀ and PowerSeries₁) are in FPS/ExpLog.lean.

References

• AlgebraicCombinatorics book, Section on Infinite Products (InfiniteProducts2.tex)

Essentially Finite Families

A family (k_i)_{i ∈ I} is essentially finite if all but finitely many i ∈ I satisfy k_i = 0. This notion is crucial for stating product rules for infinite products.

def EssentiallyFinite {I : Type u_2} {M : Type u_3} [Zero M] (f : I → M) : Prop

A family f : I → M is essentially finite if all but finitely many values are zero. This is equivalent to f having finite support.

(Definition def.fps.prodrule.ess-fin)

Canonical definition: This is the canonical, most general definition of EssentiallyFinite. It is definitionally equal to:

• AlgebraicCombinatorics.FPS.EssentiallyFinite in FPSDefinition.lean
• PowerSeries.EssentiallyFinite in Details/InfiniteProducts2.lean

All use {i | f i ≠ 0}.Finite which equals (Function.support f).Finite by definition. This version has the richest API in the EssentiallyFinite namespace.

Equations

• EssentiallyFinite f = (Function.support f).Finite

def EssentiallyFiniteSeq (k : ℕ+ → ℕ) : Prop

A sequence (k₁, k₂, k₃, ...) of natural numbers is essentially finite if all but finitely many terms are zero.

Equations

• EssentiallyFiniteSeq k = EssentiallyFinite k

def EssentiallyFiniteFamily (I : Type u_2) (M : Type u_3) [Zero M] : Type (max 0 u_2 u_3)

The set of essentially finite functions from I to M.

Equations

• EssentiallyFiniteFamily I M = { f : I → M // EssentiallyFinite f }

Basic Properties

theorem EssentiallyFinite.zero {I : Type u_2} {M : Type u_3} [Zero M] : EssentiallyFinite 0

The zero function is essentially finite.

theorem EssentiallyFinite.finite_support {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} (hf : EssentiallyFinite f) : (Function.support f).Finite

An essentially finite function has finite support.

theorem EssentiallyFinite.of_finite {I : Type u_2} {M : Type u_3} [Zero M] [Finite I] (f : I → M) : EssentiallyFinite f

A function with finite domain is essentially finite.

theorem EssentiallyFinite.of_fintype {I : Type u_2} {M : Type u_3} [Zero M] [Fintype I] (f : I → M) : EssentiallyFinite f

A function indexed by a Fintype is essentially finite.

theorem EssentiallyFinite.subfamily {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} (J : Set I) (hf : EssentiallyFinite f) : EssentiallyFinite fun (i : ↑J) => f ↑i

A subfamily of an essentially finite family is essentially finite.

theorem EssentiallyFinite.const_zero {I : Type u_2} {M : Type u_3} [Zero M] : EssentiallyFinite fun (x : I) => 0

The constant function with value zero is essentially finite.

Characterization via Filter.cofinite

theorem EssentiallyFinite.iff_eventually_cofinite {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} : EssentiallyFinite f ↔ ∀ᶠ (i : I) in Filter.cofinite, f i = 0

EssentiallyFinite f is equivalent to f i = 0 holding eventually in the cofinite filter. This is the key connection to the formulation used in the main theorems.

theorem EssentiallyFinite.iff_finite_setOf_ne_zero {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} : EssentiallyFinite f ↔ {i : I | f i ≠ 0}.Finite

Alternative characterization: the set of nonzero values is finite.

theorem EssentiallyFinite.iff_support_finite {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} : EssentiallyFinite f ↔ (Function.support f).Finite

Alternative characterization: the support is finite.

Operations on Essentially Finite Families

theorem EssentiallyFinite.neg {I : Type u_2} {M : Type u_4} [AddGroup M] {f : I → M} (hf : EssentiallyFinite f) : EssentiallyFinite (-f)

The negation of an essentially finite family is essentially finite.

theorem EssentiallyFinite.add {I : Type u_2} {M : Type u_4} [AddGroup M] {f g : I → M} (hf : EssentiallyFinite f) (hg : EssentiallyFinite g) : EssentiallyFinite (f + g)

The sum of two essentially finite families is essentially finite.

theorem EssentiallyFinite.sub {I : Type u_2} {M : Type u_4} [AddGroup M] {f g : I → M} (hf : EssentiallyFinite f) (hg : EssentiallyFinite g) : EssentiallyFinite (f - g)

The difference of two essentially finite families is essentially finite.

theorem EssentiallyFinite.mul_const {I : Type u_2} {R : Type u_4} [Ring R] [NoZeroDivisors R] {f : I → R} (hf : EssentiallyFinite f) (c : R) : EssentiallyFinite fun (i : I) => f i * c

Multiplication of an essentially finite family by a scalar is essentially finite.

theorem EssentiallyFinite.const_mul {I : Type u_2} {R : Type u_4} [Ring R] [NoZeroDivisors R] {f : I → R} (c : R) (hf : EssentiallyFinite f) : EssentiallyFinite fun (i : I) => c * f i

Multiplication of a scalar by an essentially finite family is essentially finite.

Finset and Finsupp Operations

noncomputable def EssentiallyFinite.toFinsupp {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} (hf : EssentiallyFinite f) : I →₀ M

Convert an essentially finite family to a Finsupp.

Equations

• hf.toFinsupp = Finsupp.ofSupportFinite f hf

theorem EssentiallyFinite.toFinsupp_apply {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} (hf : EssentiallyFinite f) (i : I) : hf.toFinsupp i = f i

noncomputable def EssentiallyFinite.supportFinset {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} (hf : EssentiallyFinite f) : Finset I

The support of an essentially finite family as a Finset.

Equations

• hf.supportFinset = Set.Finite.toFinset hf

theorem EssentiallyFinite.mem_supportFinset_iff {I : Type u_2} {M : Type u_3} [Zero M] {f : I → M} (hf : EssentiallyFinite f) (i : I) : i ∈ hf.supportFinset ↔ f i ≠ 0

Examples

Essentially Finite Subtype

The type of essentially finite functions, used in the main product rule theorems.

def EssentiallyFiniteFamily.toFun {I : Type u_2} {M : Type u_3} [Zero M] (f : EssentiallyFiniteFamily I M) : I → M

The underlying function of an essentially finite family.

Equations

• f.toFun = ↑f

instance EssentiallyFiniteFamily.instCoeFunForall {I : Type u_2} {M : Type u_3} [Zero M] : CoeFun (EssentiallyFiniteFamily I M) fun (x : EssentiallyFiniteFamily I M) => I → M

Equations

• EssentiallyFiniteFamily.instCoeFunForall = { coe := fun (f : EssentiallyFiniteFamily I M) => ↑f }

def EssentiallyFiniteFamily.zero {I : Type u_2} {M : Type u_3} [Zero M] : EssentiallyFiniteFamily I M

The zero essentially finite family.

Equations

• EssentiallyFiniteFamily.zero = ⟨0, ⋯⟩

instance EssentiallyFiniteFamily.instZero {I : Type u_2} {M : Type u_3} [Zero M] : Zero (EssentiallyFiniteFamily I M)

Equations

• EssentiallyFiniteFamily.instZero = { zero := EssentiallyFiniteFamily.zero }

@[simp]

theorem EssentiallyFiniteFamily.zero_apply {I : Type u_2} {M : Type u_3} [Zero M] (i : I) : ↑0 i = 0

theorem EssentiallyFiniteFamily.eventually_eq_zero {I : Type u_2} {M : Type u_3} [Zero M] (f : EssentiallyFiniteFamily I M) : ∀ᶠ (i : I) in Filter.cofinite, ↑f i = 0

An essentially finite family satisfies the cofinite condition.

theorem EssentiallyFiniteFamily.finite_support {I : Type u_2} {M : Type u_3} [Zero M] (f : EssentiallyFiniteFamily I M) : (Function.support ↑f).Finite

The support of an essentially finite family is finite.

Finite Product Rules

These are the basic distributive laws for products of sums.

theorem prod_sum_eq_sum_prod_finset {L : Type u_2} [CommSemiring L] {n : ℕ} {m : Fin n → ℕ} (p : (i : Fin n) → Fin (m i) → L) : ∏ i : Fin n, ∑ k : Fin (m i), p i k = ∑ f : (i : Fin n) → Fin (m i), ∏ i : Fin n, p i (f i)

Finite Product Rule for Finite Sums (Proposition prop.fps.prodrule-fin-fin)

A product of sums can be expanded into a sum over the Cartesian product: ∏_{i=1}^n (∑_{k=1}^{m_i} p_{i,k}) = ∑_{(k₁,...,k_n) ∈ [m₁]×...×[m_n]} ∏_{i=1}^n p_{i,k_i}

This is the generalized distributive law.

theorem prod_sum_eq_sum_prod_finset' {L : Type u_2} [CommSemiring L] {N : Type u_3} [Fintype N] [DecidableEq N] {S : N → Type u_4} [(i : N) → Fintype (S i)] (p : (i : N) → S i → L) : ∏ i : N, ∑ k : S i, p i k = ∑ f : (i : N) → S i, ∏ i : N, p i (f i)

Finite Product Rule for Finite Sums (general index set version)

Same as above but with an arbitrary finite index set N.

Finite Products of Infinite Sums

Product rules for finite products of infinite (but summable) families.

theorem coeff_finProd_eq_zero_of_factor_high_order {K : Type u_1} [CommRing K] {n : ℕ} {S : Fin n → Type u_2} (p : (i : Fin n) → S i → PowerSeries K) (f : (i : Fin n) → S i) (i : Fin n) (d : ℕ) (h : ∀ m ≤ d, (PowerSeries.coeff m) (p i (f i)) = 0) : (PowerSeries.coeff d) (∏ j : Fin n, p j (f j)) = 0

Helper lemma: The coefficient of a product is zero if one factor has all low coefficients zero. This is used in the proof of summability for product families.

theorem summable_finProd_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {n : ℕ} {S : Fin n → Type u_2} (p : (i : Fin n) → S i → PowerSeries K) (hp : ∀ (i : Fin n), Summable (p i)) : Summable fun (f : (i : Fin n) → S i) => ∏ i : Fin n, p i (f i)

Summability of finite product families (discrete case)

For discrete K, the family f ↦ ∏ i, p i (f i) is summable when each p i is summable. This is the key technical lemma for prod_tsum_eq_tsum_prod_finset.

Proof strategy: For each coefficient d, only finitely many f contribute:

• Define T i = union of supports of coeff m ∘ (p i) for m ≤ d
• Each T i is finite (by discrete summability)
• The set {f | ∀ i, f i ∈ T i} is finite (product of finite sets)
• If f i ∉ T i for some i, then coeff d (∏ j, p j (f j)) = 0

This proves that the support of f ↦ coeff d (∏ i, p i (f i)) is finite.

theorem summable_prod_of_summable_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {α : Type u_2} {β : Type u_3} (f : α → PowerSeries K) (g : β → PowerSeries K) (hf : Summable f) (hg : Summable g) : Summable fun (p : α × β) => f p.1 * g p.2

Product of two summable families in K⟦X⟧ is summable (discrete case).

This is used in the proof of prod_tsum_eq_tsum_prod_finset_discrete.

theorem prod_tsum_eq_tsum_prod_finset {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {n : ℕ} {S : Fin n → Type u_2} (p : (i : Fin n) → S i → PowerSeries K) (hp : ∀ (i : Fin n), Summable (p i)) : ∏ i : Fin n, ∑' (k : S i), p i k = ∑' (f : (i : Fin n) → S i), ∏ i : Fin n, p i (f i)

Finite Product Rule for Infinite Sums (Proposition prop.fps.prodrule-fin-inf)

For a finite product of summable families: ∏_{i=1}^n (∑_{k ∈ S_i} p_{i,k}) = ∑_{(k₁,...,k_n) ∈ S₁×...×S_n} ∏_{i=1}^n p_{i,k_i}

(Proposition prop.fps.prodrule-fin-infJ is the version with general finite index set)

Proof strategy: By induction on n.

• Base case (n=0): Both sides equal 1.
• Inductive step: Split the product into first n factors and the last factor, use IH on the first n, then apply the multiplication rule for sums.

Note: This theorem requires DiscreteTopology K. This covers the main use cases (integers, rationals, finite fields). For non-discrete K (like ℝ or ℂ), additional assumptions (such as absolute summability) would be needed.

theorem prod_tsum_eq_tsum_prod_finset' {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {N : Type u_2} [Fintype N] [DecidableEq N] {S : N → Type u_3} (p : (i : N) → S i → PowerSeries K) (hp : ∀ (i : N), Summable (p i)) : ∏ i : N, ∑' (k : S i), p i k = ∑' (f : (i : N) → S i), ∏ i : N, p i (f i)

Version with general finite index set.

Note: This theorem requires DiscreteTopology K to use prod_tsum_eq_tsum_prod_finset.

theorem prod_tsum_eq_tsum_prod_finset_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {n : ℕ} {S : Fin n → Type u_2} (p : (i : Fin n) → S i → PowerSeries K) (hp : ∀ (i : Fin n), Summable (p i)) : ∏ i : Fin n, ∑' (k : S i), p i k = ∑' (f : (i : Fin n) → S i), ∏ i : Fin n, p i (f i)

Finite Product Rule for Infinite Sums (discrete case, fully proved)

For a finite product of summable families over Fin n: ∏_{i=1}^n (∑_{k ∈ S_i} p_{i,k}) = ∑_{(k₁,...,k_n) ∈ S₁×...×S_n} ∏_{i=1}^n p_{i,k_i}

This is the discrete topology version of prod_tsum_eq_tsum_prod_finset, with a complete proof. The key insight is that in discrete topology, summability implies finite support for each coefficient, which allows us to prove summability of the product family directly.

Proof strategy: By induction on n.

• Base case (n=0): Both sides equal 1.
• Inductive step: Split the product into first n factors and the last factor, use IH on the first n, then apply the multiplication rule for sums.
• Summability of the product family is proved using summable_finProd_discrete and summable_prod_of_summable_discrete.

theorem prod_tsum_eq_tsum_prod_finset'_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {N : Type u_2} [Fintype N] [DecidableEq N] {S : N → Type u_3} (p : (i : N) → S i → PowerSeries K) (hp : ∀ (i : N), Summable (p i)) : ∏ i : N, ∑' (k : S i), p i k = ∑' (f : (i : N) → S i), ∏ i : N, p i (f i)

Finite Product Rule for Infinite Sums (discrete case, general finite index set)

This is prop.fps.prodrule-fin-infJ for discrete topology, fully proved.

For a finite product of summable families over any finite type N: ∏_{i ∈ N} (∑_{k ∈ S_i} p_{i,k}) = ∑_{f : N → S} ∏_{i ∈ N} p_{i,f(i)}

This version uses prod_tsum_eq_tsum_prod_finset_discrete and reindexes via Fintype.equivFin.

theorem prod_finset_tsum_eq_tsum_prod {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {I : Type u_2} [DecidableEq I] {S : I → Type u_3} (s : Finset I) (p : (i : I) → S i → PowerSeries K) (hp : ∀ i ∈ s, Summable (p i)) : ∏ i ∈ s, ∑' (k : S i), p i k = ∑' (f : (i : ↥s) → S ↑i), ∏ i : ↥s, p (↑i) (f i)

Finite product over a finset equals tsum over functions.

This is a variant of prod_tsum_eq_tsum_prod_finset'_discrete for products over a finset rather than a fintype. Useful for expanding ∏ i ∈ s, ∑' k, p i k.

Infinite Product Rules

The main results: product rules for infinite products of sums.

theorem multipliable_of_essentiallyFinite {K : Type u_1} [CommRing K] [TopologicalSpace K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_zero : ∀ (i : I), p i 0 = 1) (f : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 }) : Multipliable fun (i : I) => p i (↑f i)

For an essentially finite function f, the family (p i (f i))_i is multipliable when p i 0 = 1 for all i. This is because f i = 0 for all but finitely many i, so p i (f i) = p i 0 = 1 for all but finitely many i.

Technical Helper Lemmas

These lemmas are used in the proof of summability for the RHS of the infinite product rule.

theorem summable_comp_injective_of_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {α : Type u_2} {β : Type u_3} {f : α → K} (hf : Summable f) {g : β → α} (hg : Function.Injective g) : Summable (f ∘ g)

For discrete K, a subfamily via injective map is summable. This is used for proving that fibers of summable families are summable.

theorem T'n_finite_of_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) (n : ℕ) : {ik : (i : I) × { k : S i // k ≠ 0 } | ∃ m ≤ n, (PowerSeries.coeff m) (p ik.fst ↑ik.snd) ≠ 0}.Finite

For discrete K, T'_n = {(i,k) : k ≠ 0, ∃ m ≤ n, coeff m (p i k) ≠ 0} is finite. This follows from coefficient-wise summability.

theorem coeff_prod_eq_zero_of_factor_coeff_zero {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (s : Finset I) (f : I → PowerSeries K) (j : I) (hj : j ∈ s) (n : ℕ) (hf : ∀ m ≤ n, (PowerSeries.coeff m) (f j) = 0) (m : ℕ) : m ≤ n → (PowerSeries.coeff m) (∏ i ∈ s, f i) = 0

If a factor in a finite product has all coefficients up to n equal to zero, then the product also has coefficient n equal to zero.

theorem finite_funcs_with_graph_in_finite_set {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (T : Set ((i : I) × { k : S i // k ≠ 0 })) (hT : T.Finite) : {f : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 } | ∀ (i : I) (hi : ↑f i ≠ 0), ⟨i, ⟨↑f i, hi⟩⟩ ∈ T}.Finite

Essentially finite functions whose graph is contained in a finite set form a finite set. This is the key combinatorial lemma for proving summability of the RHS.

Helper Lemmas for the General Infinite Product Rule

These lemmas correspond to the claims in the detailed proof of Proposition prop.fps.prodrule-inf-inf.

theorem summable_fiber_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) (i : I) : Summable (p i)

Claim 1 from tex proof (discrete case): For each i ∈ I, the family (p_{i,k})_{k ∈ S_i} is summable.

This version is for discrete K, where the proof is straightforward using summable_comp_injective_of_discrete.

theorem summable_tsum_nonzero_fiber_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [T2Space K] [DiscreteTopology K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) : Summable fun (i : I) => ∑' (k : { k : S i // k ≠ 0 }), p i ↑k

For discrete K, the family (∑{k ∈ S_i, k ≠ 0} p{i,k})_{i ∈ I} is summable. This is a key lemma for proving multipliability of the tsum fiber family.

Summable Fiber Lemma (Complete Space Version)

This section proves that fibers of summable families are summable when the coefficient ring K is a complete uniform space. This is stronger than the discrete case but requires completeness.

theorem summable_fiber {K : Type u_1} [CommRing K] [UniformSpace K] [IsUniformAddGroup K] [IsTopologicalRing K] [CompleteSpace K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) (i : I) : Summable (p i)

Claim 1 from tex proof: For each i ∈ I, the family (p_{i,k})_{k ∈ S_i} is summable.

This follows from the assumption that (p_{i,k})_{(i,k) ∈ S̄} is summable, since each subfamily is summable.

Proof strategy: The family (p i k)_{k ∈ S_i} is summable because:

1. The subfamily (p i k)_{k ∈ S_i, k ≠ 0} is summable (as a subfamily of the summable family)
2. Adding the term p i 0 preserves summability

The key steps are:

• Use summable_iff_summable_coeff to reduce to coefficient-wise summability
• For each coefficient, use Summable.indicator_complete to show the fiber is summable
• Split the sum at k = 0 and combine

Note: This proof requires CompleteSpace K because subfamilies of summable families are only guaranteed to be summable in complete spaces. For the discrete topology case, use summable_fiber_discrete instead (which doesn't require completeness).

theorem multipliable_tsum_fiber_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_zero : ∀ (i : I), p i 0 = 1) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) : Multipliable fun (i : I) => ∑' (k : S i), p i k

Claim 2 from tex proof (discrete case): The family (∑{k ∈ S_i} p{i,k})_{i ∈ I} is multipliable.

For discrete K, this follows from coefficient-wise finiteness arguments. The key insight is that ∑k p{i,k} = 1 + ∑{k≠0} p{i,k}, and for discrete K, only finitely many finsets of indices contribute to each coefficient of the partial products.

theorem summable_prod_essentiallyFinite_discrete {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_zero : ∀ (i : I), p i 0 = 1) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) : Summable fun (f : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 }) => ∏' (i : I), p i (↑f i)

Claim 7 from tex proof (discrete case): The family (∏i p{i,k_i})_{(k_i) ∈ S^I_fin} is summable.

For discrete K, this follows from the finiteness of T'_n and the helper lemmas above.

theorem summable_prod_essentiallyFinite {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_zero : ∀ (i : I), p i 0 = 1) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) : Summable fun (f : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 }) => ∏' (i : I), p i (↑f i)

Claim 7 from tex proof: The family (∏i p{i,k_i})_{(k_i) ∈ S^I_fin} is summable.

This is the key summability result for the RHS. The proof shows that for each n, only finitely many essentially finite families (k_i) contribute to the n-th coefficient.

Proof strategy (following the tex source):

1. Use summable_iff_summable_coeff to reduce to coefficient-wise summability.

2. For each coefficient n, define T'_n = { (i,k) : k ≠ 0, ∃ m ≤ n, coeff m (p i k) ≠ 0 }. This set is finite because hp_summable implies coefficient-wise summability.

3. Define ValidFun_n = { f essentially finite | graph(f) ⊆ T'_n }. This set is finite because it injects into the powerset of T'_n.

4. Show that if f ∉ ValidFun_n, then coeff n (∏' i, p i (f.val i)) = 0. This uses the irrelevance lemma: if (i, f i) ∉ T'_n for some i with f i ≠ 0, then p i (f i) = 1 + (terms of order > n), so the n-th coefficient is unaffected.

5. Apply summable_of_finite_support to conclude.

Note: The proof requires discrete topology on K to show T'_n is finite via Summable.finite_support_of_discreteTopology. For general topological rings, the finiteness of T'_n from coefficient-wise summability would need additional structure beyond T2Space.

Helper Lemmas for Coefficient Computation

The following lemmas implement the key insight from the tex proof (Claims 9-10): factors with high order don't affect low-degree coefficients, allowing us to reduce infinite products to finite products when computing specific coefficients.

theorem coeff_prod_eq_of_extra_high_order' {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (g : I → PowerSeries K) (s t : Finset I) (hst : s ⊆ t) (n : ℕ) (h_high_order : ∀ i ∈ t \ s, ∀ m ≤ n, (PowerSeries.coeff m) (g i) = 0) : (PowerSeries.coeff n) (∏ i ∈ t, (1 + g i)) = (PowerSeries.coeff n) (∏ i ∈ s, (1 + g i))

For a finite product where extra factors have high order, the coeff n is unchanged. If s ⊆ t and for all i ∈ t \ s, g i has all coefficients up to n equal to 0, then coeff n (∏ i ∈ t, (1 + g i)) = coeff n (∏ i ∈ s, (1 + g i)).

This is a key helper for reducing infinite products to finite products when computing individual coefficients.

theorem coeff_tprod_one_add_eq_coeff_prod_of_high_order' {K : Type u_1} [CommRing K] [TopologicalSpace K] [DiscreteTopology K] {I : Type u_2} (g : I → PowerSeries K) (I_n : Set I) (hI_n : I_n.Finite) (hmult : Multipliable fun (x : I) => 1 + g x) (n : ℕ) (h_high_order : ∀ i ∉ I_n, ∀ m ≤ n, (PowerSeries.coeff m) (g i) = 0) : (PowerSeries.coeff n) (∏' (i : I), (1 + g i)) = (PowerSeries.coeff n) (∏ i ∈ hI_n.toFinset, (1 + g i))

For infinite products, if g i has high order for i ∉ I_n, then coeff n of the tprod equals coeff n of the finite product over I_n.

This is the key lemma for reducing infinite products to finite products when computing individual coefficients. It implements Claim 10 from the tex proof.

Extension and Restriction Maps for Bijection

These helper lemmas establish the bijection between functions on a finite subset I_n and essentially finite functions on the full index set I. This bijection is key to proving the infinite product rule.

def extendToI {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] {I_n : Set I} (hI_n_finite : I_n.Finite) (f : (i : ↥hI_n_finite.toFinset) → S ↑i) (i : I) : S i

Extension map: extend a function on a finite subset I_n to all of I by setting 0 outside. This is used to establish the bijection in the infinite product rule.

Equations

• extendToI hI_n_finite f i = if h : i ∈ hI_n_finite.toFinset then f ⟨i, h⟩ else 0

theorem extendToI_essentiallyFinite {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] {I_n : Set I} (hI_n_finite : I_n.Finite) (f : (i : ↥hI_n_finite.toFinset) → S ↑i) : ∀ᶠ (i : I) in Filter.cofinite, extendToI hI_n_finite f i = 0

The extension of a function on a finite set is essentially finite.

def extendToI_subtype {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] {I_n : Set I} (hI_n_finite : I_n.Finite) (f : (i : ↥hI_n_finite.toFinset) → S ↑i) : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 }

Package the extension as a subtype of essentially finite functions.

Equations

• extendToI_subtype hI_n_finite f = ⟨extendToI hI_n_finite f, ⋯⟩

def restrictToI_n {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] {I_n : Set I} (hI_n_finite : I_n.Finite) (f : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 }) (i : ↥hI_n_finite.toFinset) : S ↑i

Restriction map: restrict an essentially finite function on I to a finite subset I_n.

Equations

• restrictToI_n hI_n_finite f ⟨i, property⟩ = ↑f i

theorem restrictToI_n_extendToI_subtype {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] {I_n : Set I} (hI_n_finite : I_n.Finite) (f : (i : ↥hI_n_finite.toFinset) → S ↑i) : restrictToI_n hI_n_finite (extendToI_subtype hI_n_finite f) = f

Extension followed by restriction is the identity.

theorem extendToI_subtype_restrictToI_n {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] {I_n : Set I} (hI_n_finite : I_n.Finite) (f : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 }) (hf_supp : ∀ (i : I), ↑f i ≠ 0 → i ∈ I_n) : extendToI_subtype hI_n_finite (restrictToI_n hI_n_finite f) = f

For f with support in I_n, restriction followed by extension is the identity.

theorem prod_eq_tprod_extendToI {K : Type u_1} [CommRing K] [TopologicalSpace K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] {I_n : Set I} (hI_n_finite : I_n.Finite) (p : (i : I) → S i → PowerSeries K) (hp_zero : ∀ (i : I), p i 0 = 1) (f : (i : ↥hI_n_finite.toFinset) → S ↑i) : ∏ i : ↥hI_n_finite.toFinset, p (↑i) (f i) = ∏' (i : I), p i (extendToI hI_n_finite f i)

The finite product on I_n equals the tprod on I (after extension). This is key for showing the bijection preserves products.

theorem tprod_tsum_eq_tsum_prod_essentiallyFinite {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {I : Type u_2} {S : I → Type u_3} [(i : I) → Zero (S i)] [(i : I) → DecidableEq (S i)] (p : (i : I) → S i → PowerSeries K) (hp_zero : ∀ (i : I), p i 0 = 1) (hp_summable : Summable fun (ik : (i : I) × { k : S i // k ≠ 0 }) => p ik.fst ↑ik.snd) : ∏' (i : I), ∑' (k : S i), p i k = ∑' (f : { f : (i : I) → S i // ∀ᶠ (i : I) in Filter.cofinite, f i = 0 }), ∏' (i : I), p i (↑f i)

General Infinite Product Rule (Proposition prop.fps.prodrule-inf-inf)

For any index set I, let (S_i)_{i ∈ I} be sets that all contain 0. For p_{i,k} ∈ K⟦X⟧ with p_{i,0} = 1, if the family (p_{i,k})_{(i,k) ∈ S̄} is summable, then:

∏_{i ∈ I} (∑_{k ∈ S_i} p_{i,k}) = ∑_{essentially finite (k_i)_{i ∈ I}} ∏_{i ∈ I} p_{i,k_i}

The key insight is that only essentially finite families contribute to the sum on the RHS, ensuring that each product ∏_{i ∈ I} p_{i,k_i} is well-defined (since all but finitely many factors are p_{i,0} = 1).

Proof status: This theorem requires substantial infrastructure:

• prod_tsum_eq_tsum_prod_finset'_discrete: finite product of infinite sums (fully proved)
• coeff_mul_tprod_one_add_eq_coeff: irrelevance of high-order terms (proved)

The proof strategy (from the tex source) involves:

1. For each coefficient n, define finite approximating sets
2. Show both sides reduce to finite sums/products on these sets
3. Apply the finite distributive law
4. Use the irrelevance lemma to show high-order terms don't contribute

def SBar (S : ℕ+ → Type u_2) [(i : ℕ+) → Zero (S i)] : Type u_2

The set S̄ from Proposition prop.fps.prodrule-inf-infN: pairs (i, k) where i ∈ {1, 2, 3, ...}, k ∈ S_i, and k ≠ 0.

Equations

• SBar S = ((i : ℕ+) × { k : S i // k ≠ 0 })

theorem tprod_tsum_eq_tsum_prod_essentiallyFinite_nat {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [DiscreteTopology K] {S : ℕ+ → Type u_2} [(i : ℕ+) → Zero (S i)] [(i : ℕ+) → DecidableEq (S i)] (p : (i : ℕ+) → S i → PowerSeries K) (hp_zero : ∀ (i : ℕ+), p i 0 = 1) (hp_summable : Summable fun (ik : SBar S) => p ik.fst ↑ik.snd) : ∏' (i : ℕ+), ∑' (k : S i), p i k = ∑' (f : { f : (i : ℕ+) → S i // ∀ᶠ (i : ℕ+) in Filter.cofinite, f i = 0 }), ∏' (i : ℕ+), p i (↑f i)

Infinite Product Rule (Proposition prop.fps.prodrule-inf-infN)

Let S₁, S₂, S₃, ... be sets that all contain 0. For p_{i,k} ∈ K⟦X⟧ with p_{i,0} = 1, if the family (p_{i,k})_{(i,k) ∈ S̄} is summable, then:

∏_{i=1}^∞ (∑_{k ∈ S_i} p_{i,k}) = ∑_{essentially finite (k₁,k₂,...)} ∏_{i=1}^∞ p_{i,k_i}

The key insight is that only essentially finite sequences contribute to the sum on the RHS, ensuring that each product ∏_{i=1}^∞ p_{i,k_i} is well-defined (since all but finitely many factors are p_{i,0} = 1).

This is a special case of tprod_tsum_eq_tsum_prod_essentiallyFinite with I = ℕ+.

Lemma on Irrelevance of High-Order Terms

This lemma is used in the proof of the infinite product rule.

theorem coeff_mul_tprod_one_add_eq_coeff {K : Type u_1} [CommRing K] [TopologicalSpace K] [T2Space K] {J : Type u_2} (a : PowerSeries K) (f : J → PowerSeries K) (_hf_summable : Summable f) (n : ℕ) (hf_order : ∀ (i : J), ∀ m ≤ n, (PowerSeries.coeff m) (f i) = 0) (m : ℕ) : m ≤ n → (PowerSeries.coeff m) (a * ∏' (i : J), (1 + f i)) = (PowerSeries.coeff m) a

Irrelevance of High-Order Terms (Lemma lem.fps.prod.irlv.inf)

If a ∈ K⟦X⟧ and (f_i)_{i ∈ J} is a summable family with each f_i having [x^m](f_i) = 0 for m ∈ {0, 1, ..., n}, then [x^m](a · ∏_{i ∈ J}(1 + f_i)) = [x^m](a) for m ∈ {0, 1, ..., n}.

Intuitively, if all f_i have high order, then multiplying by ∏(1 + f_i) doesn't affect the first n+1 coefficients.

Euler's Identity for Odd Parts

A beautiful application of the product rules.

def oddPNatEquivPNat : { n : ℕ+ // Odd ↑n } ≃ ℕ+

Equivalence between positive odd natural numbers and positive natural numbers. Maps n ↦ (n+1)/2 with inverse i ↦ 2i-1.

Equations

• One or more equations did not get rendered due to their size.

theorem oddPNatEquivPNat_symm_coe (i : ℕ+) : ↑↑(oddPNatEquivPNat.symm i) = 2 * ↑i - 1

The coercion of oddPNatEquivPNat.symm i is 2 * i - 1.

theorem euler_odd_parts_identity {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [NoZeroDivisors K] : ∏' (i : ℕ+), Ring.inverse (1 - PowerSeries.X ^ (2 * ↑i - 1)) = ∏' (k : ℕ+), (1 + PowerSeries.X ^ ↑k)

Euler's Identity (Proposition prop.gf.prod.euler-odd)

∏_{i>0} (1 - x^{2i-1})⁻¹ = ∏_{k>0} (1 + x^k)

This identity relates the generating function for partitions into odd parts to the generating function for partitions into distinct parts.

The proof uses the fact that:

• The RHS is the generating function for partitions into distinct parts
• The LHS is the generating function for partitions into odd parts
• By Glaisher's theorem, these partition counts are equal

The algebraic proof (from the TeX source) shows:

1. (1 + x^k)(1 - x^k) = 1 - x^{2k}
2. ∏_{k>0}(1 + x^k) = ∏_{k>0}(1 - x^{2k}) / ∏_{k>0}(1 - x^k)
3. The even factors cancel, leaving 1 / ∏_{k odd}(1 - x^k)

theorem euler_odd_parts_identity' {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [NoZeroDivisors K] : ∏' (i : { n : ℕ+ // Odd ↑n }), Ring.inverse (1 - PowerSeries.X ^ ↑↑i) = ∏' (k : ℕ+), (1 + PowerSeries.X ^ ↑k)

Alternative form of Euler's identity using the set of odd positive integers.

This follows from euler_odd_parts_identity by reindexing the product using the equivalence oddPNatEquivPNat between { n : ℕ+ // Odd n } and ℕ+.

Combinatorial Interpretation: Partitions

The combinatorial consequence of Euler's identity.

def numDistinctPartitions (n : ℕ) : ℕ

Number of ways to write n as a sum of distinct positive integers.

Equations

• numDistinctPartitions n = (Nat.Partition.distincts n).card

def numOddPartitions (n : ℕ) : ℕ

Number of ways to write n as a sum of odd positive integers.

Equations

• numOddPartitions n = (Nat.Partition.odds n).card

theorem euler_distinct_odd_partitions (n : ℕ) : numDistinctPartitions n = numOddPartitions n

Euler's Partition Theorem (Theorem thm.gf.prod.euler-comb)

The number of partitions of n into distinct positive integers equals the number of partitions of n into odd positive integers.

For example, for n = 6:

• Distinct partitions: 6, 1+5, 2+4, 1+2+3 (4 partitions)
• Odd partitions: 1+5, 3+3, 3+1+1+1, 1+1+1+1+1+1 (4 partitions)

Infinite Products and Substitution

The substitution rule extends to infinite products.

theorem continuous_rescale {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] (a : K) : Continuous ⇑(PowerSeries.rescale a)

The rescale ring homomorphism is continuous in the pi topology on power series.

theorem tprod_rescale_substitution {K : Type u_1} [CommRing K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] {I : Type u_2} (f : I → PowerSeries K) (a : K) (hf : Multipliable f) : (PowerSeries.rescale a) (∏' (i : I), f i) = ∏' (i : I), (PowerSeries.rescale a) (f i)

Substitution Rule for Infinite Products (Proposition prop.fps.subs.rule-infprod)

If (f_i)_{i ∈ I} is a multipliable family and a ∈ K, then rescaling commutes with infinite products: rescale a (∏_{i ∈ I} f_i) = ∏_{i ∈ I} (rescale a (f_i)).

In the context of substitution, this says that (∏ f_i)(ax) = ∏ f_i(ax).

Exponentials, Logarithms and Infinite Products

The Exp and Log maps convert between infinite sums and products. These results require K to be a ℚ-algebra for the formal exp and log to be defined.

Note on formalization status:

The source material (Propositions prop.fps.Exp-Log-infsum and prop.fps.Exp-Log-infprod) states:

• Exp(∑_{i ∈ I} f_i) = ∏_{i ∈ I} Exp(f_i) for summable families in K⟦X⟧_0
• Log(∏_{i ∈ I} f_i) = ∑_{i ∈ I} Log(f_i) for multipliable families in K⟦X⟧_1

These require:

1. A general composition/substitution operation for power series (to define Exp(f) for f with zero constant term)
2. A formal logarithm Log : K⟦X⟧_1 → K⟦X⟧_0 (not yet in Mathlib)

The finite versions use PowerSeries.exp_mul_exp_eq_exp_add: exp(aX) * exp(bX) = exp((a+b)X). Once the infrastructure is available, the infinite versions should follow by taking limits.

Exp/Log Placeholder Section

The source material includes Propositions prop.fps.Exp-Log-infsum and prop.fps.Exp-Log-infprod relating infinite sums/products via Exp and Log maps.

Canonical definitions for FPS with constant term 0 or 1:

• PowerSeries.PowerSeries₀ (FPS with constant term 0) — see FPS/ExpLog.lean
• PowerSeries.PowerSeries₁ (FPS with constant term 1) — see FPS/ExpLog.lean

These definitions have extensive API including:

• PowerSeries₀.addSubgroup — additive subgroup structure
• PowerSeries₁.subgroup — multiplicative subgroup structure (for fields)
• Membership lemmas (mem_PowerSeries₀_iff, mem_PowerSeries₁_iff)
• Closure properties (add_mem, mul_mem, inv_mem, etc.)
• Composition lemmas (subst_mem, exp_subst_mem_PowerSeries₁, etc.)
• The Exp and Log maps between these sets

Once the Exp/Log infrastructure from ExpLog.lean is integrated, the infinite versions (prop.fps.Exp-Log-infsum and prop.fps.Exp-Log-infprod) can be formalized by taking limits.

The Binary Product Rule (eq.fps.prod.binary.prod-inf)

The special case that motivated the general theory.

theorem binary_product_rule {K : Type u_1} [CommRing K] [TopologicalSpace K] (a : ℕ → PowerSeries K) (ha : Summable a) [DiscreteTopology K] : ∏' (i : ℕ), (1 + a i) = ∑' (s : Finset ℕ), ∏ i ∈ s, a i

Binary Product Rule (Equation eq.fps.prod.binary.prod-inf)

For a summable sequence (a_n)_{n ∈ ℕ}: ∏_{i ∈ ℕ} (1 + a_i) = ∑_{i₁ < i₂ < ... < i_k} a_{i₁} a_{i₂} ... a_{i_k}

The RHS is a sum over all finite strictly increasing sequences of indices.

Note: This theorem requires K to have discrete topology. This covers the main use cases (integers, rationals, finite fields). For non-discrete K (like ℝ or ℂ), additional assumptions (such as completeness) may be needed.

theorem binary_product_rule' {K : Type u_1} [CommRing K] [TopologicalSpace K] (a : ℕ → PowerSeries K) (ha : Summable a) [DiscreteTopology K] : ∏' (i : ℕ), (1 + a i) = ∑' (J : { J : Set ℕ // J.Finite }), ∏ᶠ (i : ℕ) (_ : i ∈ ↑J), a i

Alternative formulation: the product equals a sum over finite subsets.