Mathlib.Topology.Algebra.InfiniteSum.NatInt

HasProd.tendsto_prod_nat theorem

{f : ℕ → M} (h : HasProd f m) : Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Full source

/-- If `f : ℕ → M` has product `m`, then the partial products `∏ i ∈ range n, f i` converge
to `m`. -/
@[to_additive "If `f : ℕ → M` has sum `m`, then the partial sums `∑ i ∈ range n, f i` converge
to `m`."]
theorem HasProd.tendsto_prod_nat {f : ℕ → M} (h : HasProd f m) :
    Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 m) :=
  h.comp tendsto_finset_range

Convergence of Partial Products to the Infinite Product

Informal description

Let $M$ be a commutative monoid with a topological space structure, and let $f \colon \mathbb{N} \to M$ be a function. If the product of $f$ converges to $m \in M$ (i.e., $\text{HasProd}\, f\, m$ holds), then the sequence of partial products $\prod_{i=0}^{n-1} f(i)$ converges to $m$ in the topology of $M$ as $n \to \infty$.

Multipliable.tendsto_prod_tprod_nat theorem

{f : ℕ → M} (h : Multipliable f) : Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 (∏' i, f i))

Full source

/-- If `f : ℕ → M` is multipliable, then the partial products `∏ i ∈ range n, f i` converge
to `∏' i, f i`. -/
@[to_additive "If `f : ℕ → M` is summable, then the partial sums `∑ i ∈ range n, f i` converge
to `∑' i, f i`."]
theorem Multipliable.tendsto_prod_tprod_nat {f : ℕ → M} (h : Multipliable f) :
    Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 (∏' i, f i)) :=
  h.hasProd.tendsto_prod_nat

Convergence of partial products to the unconditional product on $\mathbb{N}$

Informal description

Let $M$ be a commutative topological monoid and $f \colon \mathbb{N} \to M$ be a multipliable function. Then the sequence of partial products $\prod_{i=0}^{n-1} f(i)$ converges to the unconditional product $\prod'_{i=0}^\infty f(i)$ in the topology of $M$ as $n \to \infty$.

HasProd.prod_range_mul theorem

{f : ℕ → M} {k : ℕ} (h : HasProd (fun n ↦ f (n + k)) m) : HasProd f ((∏ i ∈ range k, f i) * m)

Full source

@[to_additive]
theorem prod_range_mul {f : ℕ → M} {k : ℕ} (h : HasProd (fun n ↦ f (n + k)) m) :
    HasProd f ((∏ i ∈ range k, f i) * m) := by
  refine ((range k).hasProd f).mul_compl ?_
  rwa [← (notMemRangeEquiv k).symm.hasProd_iff]

Product Decomposition: Initial Segment and Shifted Tail Multiply to Total Product

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. If the product of the shifted function $n \mapsto f(n + k)$ converges to $m$, then the product of $f$ converges to the product of the first $k$ terms multiplied by $m$, i.e., $\left(\prod_{i=0}^{k-1} f(i)\right) \cdot m$.

HasProd.zero_mul theorem

{f : ℕ → M} (h : HasProd (fun n ↦ f (n + 1)) m) : HasProd f (f 0 * m)

Full source

@[to_additive]
theorem zero_mul {f : ℕ → M} (h : HasProd (fun n ↦ f (n + 1)) m) :
    HasProd f (f 0 * m) := by
  simpa only [prod_range_one] using h.prod_range_mul

Product Decomposition: Initial Term Multiplied by Shifted Product Equals Total Product

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. If the product of the shifted function $n \mapsto f(n + 1)$ converges to $m$, then the product of $f$ converges to $f(0) \cdot m$.

HasProd.even_mul_odd theorem

{f : ℕ → M} (he : HasProd (fun k ↦ f (2 * k)) m) (ho : HasProd (fun k ↦ f (2 * k + 1)) m') : HasProd f (m * m')

Full source

@[to_additive]
theorem even_mul_odd {f : ℕ → M} (he : HasProd (fun k ↦ f (2 * k)) m)
    (ho : HasProd (fun k ↦ f (2 * k + 1)) m') : HasProd f (m * m') := by
  have := mul_right_injective₀ (two_ne_zero' ℕ)
  replace ho := ((add_left_injective 1).comp this).hasProd_range_iff.2 ho
  refine (this.hasProd_range_iff.2 he).mul_isCompl ?_ ho
  simpa [Function.comp_def] using Nat.isCompl_even_odd

Product Decomposition: Even and Odd Terms Multiply to Total Product

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. If the product of $f$ over the even indices converges to $m$ and the product over the odd indices converges to $m'$, then the total product of $f$ over all natural numbers converges to $m \cdot m'$.

Multipliable.hasProd_iff_tendsto_nat theorem

 [T2Space M] {f : ℕ → M} (hf : Multipliable f) : HasProd f m ↔ Tendsto (fun n : ℕ ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Full source

@[to_additive]
theorem hasProd_iff_tendsto_nat [T2Space M] {f : ℕ → M} (hf : Multipliable f) :
    HasProdHasProd f m ↔ Tendsto (fun n : ℕ ↦ ∏ i ∈ range n, f i) atTop (𝓝 m) := by
  refine ⟨fun h ↦ h.tendsto_prod_nat, fun h ↦ ?_⟩
  rw [tendsto_nhds_unique h hf.hasProd.tendsto_prod_nat]
  exact hf.hasProd

Convergence of Infinite Product via Partial Products in Hausdorff Spaces

Informal description

Let $M$ be a Hausdorff topological space and $f \colon \mathbb{N} \to M$ be a multipliable function. Then the product of $f$ converges to $m \in M$ if and only if the sequence of partial products $\prod_{i=0}^{n-1} f(i)$ converges to $m$ as $n \to \infty$.

Multipliable.comp_nat_add theorem

{f : ℕ → M} {k : ℕ} (h : Multipliable fun n ↦ f (n + k)) : Multipliable f

Full source

@[to_additive]
theorem comp_nat_add {f : ℕ → M} {k : ℕ} (h : Multipliable fun n ↦ f (n + k)) : Multipliable f :=
  h.hasProd.prod_range_mul.multipliable

Multipliability of Shifted Function Implies Multipliability of Original Function

Informal description

Let $M$ be a commutative topological monoid and $f \colon \mathbb{N} \to M$ be a function. If the shifted function $n \mapsto f(n + k)$ is multipliable for some $k \in \mathbb{N}$, then $f$ itself is multipliable.

Multipliable.even_mul_odd theorem

{f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k)) (ho : Multipliable fun k ↦ f (2 * k + 1)) : Multipliable f

Full source

@[to_additive]
theorem even_mul_odd {f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k))
    (ho : Multipliable fun k ↦ f (2 * k + 1)) : Multipliable f :=
  (he.hasProd.even_mul_odd ho.hasProd).multipliable

Multipliability of a Function via Even and Odd Terms

Informal description

Let $M$ be a commutative topological monoid and $f \colon \mathbb{N} \to M$ be a function. If the restriction of $f$ to even indices (i.e., $k \mapsto f(2k)$) is multipliable and the restriction to odd indices (i.e., $k \mapsto f(2k+1)$) is multipliable, then $f$ itself is multipliable.

tprod_iSup_decode₂ theorem

 [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (s : β → α) : ∏' i : ℕ, m (⨆ b ∈ decode₂ β i, s b) = ∏' b : β, m (s b)

Full source

/-- You can compute a product over an encodable type by multiplying over the natural numbers and
taking a supremum. -/
@[to_additive "You can compute a sum over an encodable type by summing over the natural numbers and
  taking a supremum. This is useful for outer measures."]
theorem tprod_iSup_decode₂ [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (s : β → α) :
    ∏' i : ℕ, m (⨆ b ∈ decode₂ β i, s b) = ∏' b : β, m (s b) := by
  rw [← tprod_extend_one (@encode_injective β _)]
  refine tprod_congr fun n ↦ ?_
  rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn
  · simp [encode_injective.extend_apply]
  · rw [extend_apply' _ _ _ hn]
    rw [← decode₂_ne_none_iff, ne_eq, not_not] at hn
    simp [hn, m0]

Unconditional Product of Suprema via Decoding Equals Direct Product

Informal description

Let $\alpha$ be a complete lattice and $M$ a commutative topological monoid. Given a function $m : \alpha \to M$ with $m(\bot) = 1$ and a family of elements $s : \beta \to \alpha$, the unconditional product over $\mathbb{N}$ of $m$ applied to the supremum of $s$ over the decodings of each natural number equals the unconditional product of $m \circ s$ over $\beta$. That is, \[ \prod'_{i \in \mathbb{N}} m\left(\bigsqcup_{b \in \text{decode}_\beta(i)} s(b)\right) = \prod'_{b \in \beta} m(s(b)). \]

tprod_iUnion_decode₂ theorem

(m : Set α → M) (m0 : m ∅ = 1) (s : β → Set α) : ∏' i, m (⋃ b ∈ decode₂ β i, s b) = ∏' b, m (s b)

Full source

/-- `tprod_iSup_decode₂` specialized to the complete lattice of sets. -/
@[to_additive "`tsum_iSup_decode₂` specialized to the complete lattice of sets."]
theorem tprod_iUnion_decode₂ (m : Set α → M) (m0 : m ∅ = 1) (s : β → Set α) :
    ∏' i, m (⋃ b ∈ decode₂ β i, s b) = ∏' b, m (s b) :=
  tprod_iSup_decode₂ m m0 s

Unconditional Product of Set Unions via Decoding Equals Direct Product

Informal description

Let $M$ be a commutative topological monoid and $\alpha$ be a type. Given a function $m \colon \mathcal{P}(\alpha) \to M$ satisfying $m(\emptyset) = 1$ and a family of sets $s \colon \beta \to \mathcal{P}(\alpha)$, the unconditional product over $\mathbb{N}$ of $m$ applied to the union of $s(b)$ over all $b$ decoded from each natural number equals the unconditional product of $m \circ s$ over $\beta$. That is, \[ \prod'_{i \in \mathbb{N}} m\left(\bigcup_{b \in \text{decode}_\beta(i)} s(b)\right) = \prod'_{b \in \beta} m(s(b)). \]

rel_iSup_tprod theorem

 [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
  (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : β → α) : R (m (⨆ b : β, s b)) (∏' b : β, m (s b))

Full source

/-- If a function is countably sub-multiplicative then it is sub-multiplicative on countable
types -/
@[to_additive "If a function is countably sub-additive then it is sub-additive on countable types"]
theorem rel_iSup_tprod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
    (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : β → α) :
    R (m (⨆ b : β, s b)) (∏' b : β, m (s b)) := by
  cases nonempty_encodable β
  rw [← iSup_decode₂, ← tprod_iSup_decode₂ _ m0 s]
  exact m_iSup _

Relation Between Supremum and Unconditional Product for Countable Families

Informal description

Let $\alpha$ be a complete lattice and $M$ a commutative topological monoid. Given a function $m \colon \alpha \to M$ with $m(\bot) = 1$ and a relation $R \colon M \to M \to \text{Prop}$ such that for any sequence $s \colon \mathbb{N} \to \alpha$, the relation $R(m(\bigsqcup_i s_i), \prod'_{i} m(s_i))$ holds, then for any family $s \colon \beta \to \alpha$, the relation $R(m(\bigsqcup_{b \in \beta} s_b), \prod'_{b \in \beta} m(s_b))$ also holds.

rel_iSup_prod theorem

 [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
  (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : γ → α) (t : Finset γ) :
  R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))

Full source

/-- If a function is countably sub-multiplicative then it is sub-multiplicative on finite sets -/
@[to_additive "If a function is countably sub-additive then it is sub-additive on finite sets"]
theorem rel_iSup_prod [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
    (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s : γ → α) (t : Finset γ) :
    R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d)) := by
  rw [iSup_subtype', ← Finset.tprod_subtype]
  exact rel_iSup_tprod m m0 R m_iSup _

Relation Between Finite Supremum and Finite Product in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice and $M$ a commutative topological monoid. Given a function $m \colon \alpha \to M$ with $m(\bot) = 1$ and a relation $R \colon M \to M \to \text{Prop}$ such that for any sequence $s \colon \mathbb{N} \to \alpha$, the relation $R(m(\bigsqcup_i s_i), \prod'_{i} m(s_i))$ holds, then for any finite set $t$ and any family $s \colon \gamma \to \alpha$, the relation $R(m(\bigsqcup_{d \in t} s_d), \prod_{d \in t} m(s_d))$ holds.

rel_sup_mul theorem

 [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
  (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s₁ s₂ : α) : R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)

Full source

/-- If a function is countably sub-multiplicative then it is binary sub-multiplicative -/
@[to_additive "If a function is countably sub-additive then it is binary sub-additive"]
theorem rel_sup_mul [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
    (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s₁ s₂ : α) :
    R (m (s₁ ⊔ s₂)) (m s₁ * m s₂) := by
  convert rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂
  · simp only [iSup_bool_eq, cond]
  · rw [tprod_fintype, Fintype.prod_bool, cond, cond]

Binary Sub-multiplicativity from Countable Sub-multiplicativity

Informal description

Let $\alpha$ be a complete lattice and $M$ a commutative topological monoid. Given a function $m \colon \alpha \to M$ with $m(\bot) = 1$ and a relation $R \colon M \to M \to \text{Prop}$ such that for any sequence $s \colon \mathbb{N} \to \alpha$, the relation $R(m(\bigsqcup_i s_i), \prod'_{i} m(s_i))$ holds, then for any two elements $s_1, s_2 \in \alpha$, the relation $R(m(s_1 \sqcup s_2), m(s_1) \cdot m(s_2))$ holds.

Multipliable.prod_mul_tprod_nat_mul' theorem

 {f : ℕ → M} {k : ℕ} (h : Multipliable (fun n ↦ f (n + k))) : ((∏ i ∈ range k, f i) * ∏' i, f (i + k)) = ∏' i, f i

Full source

@[to_additive]
protected theorem Multipliable.prod_mul_tprod_nat_mul'
    {f : ℕ → M} {k : ℕ} (h : Multipliable (fun n ↦ f (n + k))) :
    ((∏ i ∈ range k, f i) * ∏' i, f (i + k)) = ∏' i, f i :=
  h.hasProd.prod_range_mul.tprod_eq.symm

Product Decomposition: $\prod_{i

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. If the shifted function $n \mapsto f(n + k)$ is multipliable, then the product of the first $k$ terms multiplied by the unconditional product of the shifted function equals the unconditional product of $f$, i.e., \[ \left( \prod_{i=0}^{k-1} f(i) \right) \cdot \left( \prod'_{i} f(i + k) \right) = \prod'_{i} f(i). \]

tprod_eq_zero_mul' theorem

{f : ℕ → M} (hf : Multipliable (fun n ↦ f (n + 1))) : ∏' b, f b = f 0 * ∏' b, f (b + 1)

Full source

@[to_additive]
theorem tprod_eq_zero_mul'
    {f : ℕ → M} (hf : Multipliable (fun n ↦ f (n + 1))) :
    ∏' b, f b = f 0 * ∏' b, f (b + 1) := by
  simpa only [prod_range_one] using hf.prod_mul_tprod_nat_mul'.symm

Product Decomposition: $\prod' f(b) = f(0) \cdot \prod' f(b+1)$

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. If the shifted function $n \mapsto f(n + 1)$ is multipliable, then the unconditional product of $f$ satisfies: \[ \prod'_{b} f(b) = f(0) \cdot \prod'_{b} f(b + 1). \]

tprod_even_mul_odd theorem

 {f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k)) (ho : Multipliable fun k ↦ f (2 * k + 1)) :
  (∏' k, f (2 * k)) * ∏' k, f (2 * k + 1) = ∏' k, f k

Full source

@[to_additive]
theorem tprod_even_mul_odd {f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k))
    (ho : Multipliable fun k ↦ f (2 * k + 1)) :
    (∏' k, f (2 * k)) * ∏' k, f (2 * k + 1) = ∏' k, f k :=
  (he.hasProd.even_mul_odd ho.hasProd).tprod_eq.symm

Product Decomposition: $\prod' f(k) = \prod' f(2k) \cdot \prod' f(2k+1)$

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. If the function $k \mapsto f(2k)$ is multipliable and the function $k \mapsto f(2k+1)$ is multipliable, then the product of the unconditional products satisfies: \[ \left( \prod'_{k} f(2k) \right) \cdot \left( \prod'_{k} f(2k+1) \right) = \prod'_{k} f(k). \]

hasProd_nat_add_iff theorem

{f : ℕ → G} (k : ℕ) : HasProd (fun n ↦ f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i)

Full source

@[to_additive]
theorem hasProd_nat_add_iff {f : ℕ → G} (k : ℕ) :
    HasProdHasProd (fun n ↦ f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i) := by
  refine Iff.trans ?_ (range k).hasProd_compl_iff
  rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]

Shifted Product Convergence Criterion: $\prod_{n} f(n+k) = g \leftrightarrow \prod_{n} f(n) = g \cdot \prod_{i

Informal description

Let $G$ be a commutative topological group and $f \colon \mathbb{N} \to G$ be a function. For any natural number $k$ and element $g \in G$, the product of the shifted function $n \mapsto f(n + k)$ converges to $g$ if and only if the product of $f$ converges to $g \cdot \prod_{i < k} f(i)$.

multipliable_nat_add_iff theorem

{f : ℕ → G} (k : ℕ) : (Multipliable fun n ↦ f (n + k)) ↔ Multipliable f

Full source

@[to_additive]
theorem multipliable_nat_add_iff {f : ℕ → G} (k : ℕ) :
    (Multipliable fun n ↦ f (n + k)) ↔ Multipliable f :=
  Iff.symm <|
    (Equiv.mulRight (∏ i ∈ range k, f i)).surjective.multipliable_iff_of_hasProd_iff
      (hasProd_nat_add_iff k).symm

Multipliability of Shifted Function: $\prod' f(n+k)$ converges iff $\prod' f(n)$ converges

Informal description

Let $G$ be a commutative topological group and $f \colon \mathbb{N} \to G$ be a function. For any natural number $k$, the function $n \mapsto f(n + k)$ is multipliable if and only if $f$ is multipliable.

hasProd_nat_add_iff' theorem

{f : ℕ → G} (k : ℕ) : HasProd (fun n ↦ f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g

Full source

@[to_additive]
theorem hasProd_nat_add_iff' {f : ℕ → G} (k : ℕ) :
    HasProdHasProd (fun n ↦ f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g := by
  simp [hasProd_nat_add_iff]

Shifted Product Convergence Criterion: $\prod_{n} f(n+k) = g / \prod_{i

Informal description

Let $G$ be a commutative topological group and $f : \mathbb{N} \to G$ a sequence. For any $k \in \mathbb{N}$ and $g \in G$, the product of the shifted sequence $n \mapsto f(n + k)$ converges to $g / \prod_{i < k} f(i)$ if and only if the product of $f$ converges to $g$.

Multipliable.prod_mul_tprod_nat_add theorem

 [T2Space G] {f : ℕ → G} (k : ℕ) (h : Multipliable f) : ((∏ i ∈ range k, f i) * ∏' i, f (i + k)) = ∏' i, f i

Full source

@[to_additive]
protected theorem Multipliable.prod_mul_tprod_nat_add [T2Space G] {f : ℕ → G} (k : ℕ)
    (h : Multipliable f) : ((∏ i ∈ range k, f i) * ∏' i, f (i + k)) = ∏' i, f i :=
  Multipliable.prod_mul_tprod_nat_mul' <| (multipliable_nat_add_iff k).2 h

Product Decomposition for Multipliable Sequences: $\prod_{i

Informal description

Let $G$ be a Hausdorff commutative topological group and $f \colon \mathbb{N} \to G$ be a multipliable function. For any natural number $k$, the product of the first $k$ terms multiplied by the unconditional product of the shifted function equals the unconditional product of $f$, i.e., \[ \left( \prod_{i=0}^{k-1} f(i) \right) \cdot \left( \prod'_{i} f(i + k) \right) = \prod'_{i} f(i). \]

Multipliable.tprod_eq_zero_mul theorem

[T2Space G] {f : ℕ → G} (hf : Multipliable f) : ∏' b, f b = f 0 * ∏' b, f (b + 1)

Full source

@[to_additive]
protected theorem Multipliable.tprod_eq_zero_mul [T2Space G] {f : ℕ → G} (hf : Multipliable f) :
    ∏' b, f b = f 0 * ∏' b, f (b + 1) :=
  tprod_eq_zero_mul' <| (multipliable_nat_add_iff 1).2 hf

Product Decomposition for Multipliable Functions: $\prod' f(b) = f(0) \cdot \prod' f(b+1)$

Informal description

Let $G$ be a Hausdorff commutative topological group and $f \colon \mathbb{N} \to G$ be a multipliable function. Then the unconditional product of $f$ satisfies: \[ \prod'_{b} f(b) = f(0) \cdot \prod'_{b} f(b + 1). \]

tendsto_prod_nat_add theorem

[T2Space G] (f : ℕ → G) : Tendsto (fun i ↦ ∏' k, f (k + i)) atTop (𝓝 1)

Full source

/-- For `f : ℕ → G`, the product `∏' k, f (k + i)` tends to one. This does not require a
multipliability assumption on `f`, as otherwise all such products are one. -/
@[to_additive "For `f : ℕ → G`, the sum `∑' k, f (k + i)` tends to zero. This does not require a
summability assumption on `f`, as otherwise all such sums are zero."]
theorem tendsto_prod_nat_add [T2Space G] (f : ℕ → G) :
    Tendsto (fun i ↦ ∏' k, f (k + i)) atTop (𝓝 1) := by
  by_cases hf : Multipliable f
  · have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by
      ext1 i
      rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
    have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds
    simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat
  · refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm
    rwa [multipliable_nat_add_iff n]

Limit of Shifted Products: $\prod' f(k+i) \to 1$ as $i \to \infty$

Informal description

Let $G$ be a Hausdorff commutative topological group and $f \colon \mathbb{N} \to G$ be a function. The unconditional product $\prod'_{k} f(k + i)$ tends to $1$ in the neighborhood filter of $G$ as $i \to \infty$.

cauchySeq_finset_iff_nat_tprod_vanishing theorem

 {f : ℕ → G} :
  (CauchySeq fun s : Finset ℕ ↦ ∏ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 (1 : G), ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e

Full source

@[to_additive]
theorem cauchySeq_finset_iff_nat_tprod_vanishing {f : ℕ → G} :
    (CauchySeq fun s : Finset ℕ ↦ ∏ n ∈ s, f n) ↔
      ∀ e ∈ 𝓝 (1 : G), ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e := by
  refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
  · obtain ⟨s, hs⟩ := vanish e he
    refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
    split_ifs at ht with h
    · exact fun m hmt hms ↦ (s.le_max' _ hms).not_lt (Nat.succ_le_iff.mp <| ht hmt)
    · exact fun _ _ hs ↦ h ⟨_, hs⟩
  · obtain ⟨N, hN⟩ := vanish e he
    exact ⟨range N, fun t ht ↦ hN _ fun n hnt ↦
      le_of_not_lt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩

Cauchy Criterion for Infinite Products over Natural Numbers via Vanishing Neighborhoods

Informal description

Let $G$ be a commutative topological group and $f \colon \mathbb{N} \to G$ a function. The sequence of partial products $\left( \prod_{n \in s} f(n) \right)_{s \in \text{Finset}(\mathbb{N})}$ is a Cauchy sequence if and only if for every neighborhood $e$ of the identity element $1 \in G$, there exists a natural number $N$ such that for any subset $t \subseteq \{n \mid N \leq n\}$, the unconditional product $\prod'_{n \in t} f(n)$ belongs to $e$.

multipliable_iff_nat_tprod_vanishing theorem

{f : ℕ → G} : Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e

Full source

@[to_additive]
theorem multipliable_iff_nat_tprod_vanishing {f : ℕ → G} : MultipliableMultipliable f ↔
    ∀ e ∈ 𝓝 1, ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e := by
  rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tprod_vanishing]

Multipliability Criterion via Vanishing Neighborhoods in $\mathbb{N}$

Informal description

Let $G$ be a commutative topological group and $f \colon \mathbb{N} \to G$ a function. The function $f$ is multipliable (i.e., the infinite product $\prod_{n \in \mathbb{N}} f(n)$ converges unconditionally) if and only if for every neighborhood $e$ of the identity element $1 \in G$, there exists a natural number $N$ such that for any subset $t \subseteq \{n \mid N \leq n\}$, the unconditional product $\prod'_{n \in t} f(n)$ belongs to $e$.

Multipliable.nat_tprod_vanishing theorem

 {f : ℕ → G} (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 1) : ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e

Full source

@[to_additive]
theorem Multipliable.nat_tprod_vanishing {f : ℕ → G} (hf : Multipliable f) ⦃e : Set G⦄
    (he : e ∈ 𝓝 1) : ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e :=
  letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  cauchySeq_finset_iff_nat_tprod_vanishing.1 hf.hasProd.cauchySeq e he

Vanishing Neighborhood Criterion for Multipliable Functions on $\mathbb{N}$

Informal description

Let $G$ be a commutative topological group and $f \colon \mathbb{N} \to G$ be a multipliable function. Then for every neighborhood $e$ of the identity element $1 \in G$, there exists a natural number $N$ such that for any subset $t \subseteq \{n \mid N \leq n\}$, the unconditional product $\prod'_{n \in t} f(n)$ belongs to $e$.

Multipliable.tendsto_atTop_one theorem

{f : ℕ → G} (hf : Multipliable f) : Tendsto f atTop (𝓝 1)

Full source

@[to_additive]
theorem Multipliable.tendsto_atTop_one {f : ℕ → G} (hf : Multipliable f) :
    Tendsto f atTop (𝓝 1) := by
  rw [← Nat.cofinite_eq_atTop]
  exact hf.tendsto_cofinite_one

Multipliable Functions on $\mathbb{N}$ Tend to Identity at Infinity

Informal description

Let $G$ be a topological group and $f : \mathbb{N} \to G$ be a multipliable function. Then $f(n)$ converges to the identity element $1 \in G$ as $n \to \infty$.

HasProd.nat_mul_neg_add_one theorem

{f : ℤ → M} (hf : HasProd f m) : HasProd (fun n : ℕ ↦ f n * f (-(n + 1))) m

Full source

@[to_additive HasSum.nat_add_neg_add_one]
lemma HasProd.nat_mul_neg_add_one {f : ℤ → M} (hf : HasProd f m) :
    HasProd (fun n : ℕ ↦ f n * f (-(n + 1))) m := by
  change HasProd (fun n : ℕ ↦ f n * f (Int.negSucc n)) m
  have : Injective Int.negSucc := @Int.negSucc.inj
  refine hf.hasProd_of_prod_eq fun u ↦ ?_
  refine ⟨u.preimage _ Nat.cast_injective.injOn ∪ u.preimage _ this.injOn,
      fun v' hv' ↦ ⟨v'.image Nat.cast ∪ v'.image Int.negSucc, fun x hx ↦ ?_, ?_⟩⟩
  · simp only [mem_union, mem_image]
    cases x
    · exact Or.inl ⟨_, hv' (by simpa using Or.inl hx), rfl⟩
    · exact Or.inr ⟨_, hv' (by simpa using Or.inr hx), rfl⟩
  · rw [prod_union, prod_image Nat.cast_injective.injOn, prod_image this.injOn,
      prod_mul_distrib]
    simp only [disjoint_iff_ne, mem_image, ne_eq, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂, not_false_eq_true, implies_true, forall_const, reduceCtorEq]

Product convergence of paired integer terms via natural numbers

Informal description

Let $f : \mathbb{Z} \to M$ be a function such that the product of $f$ over all integers converges to $m$. Then the product of the function $g(n) = f(n) \cdot f(-(n+1))$ over all natural numbers $n \in \mathbb{N}$ also converges to $m$.

Multipliable.nat_mul_neg_add_one theorem

{f : ℤ → M} (hf : Multipliable f) : Multipliable (fun n : ℕ ↦ f n * f (-(n + 1)))

Full source

@[to_additive Summable.nat_add_neg_add_one]
lemma Multipliable.nat_mul_neg_add_one {f : ℤ → M} (hf : Multipliable f) :
    Multipliable (fun n : ℕ ↦ f n * f (-(n + 1))) :=
  hf.hasProd.nat_mul_neg_add_one.multipliable

Multipliability of Paired Integer Terms over Natural Numbers

Informal description

Let $f : \mathbb{Z} \to M$ be a multipliable function in a commutative topological monoid $M$. Then the function $g(n) = f(n) \cdot f(-(n+1))$ is multipliable over the natural numbers $\mathbb{N}$.

tprod_nat_mul_neg_add_one theorem

[T2Space M] {f : ℤ → M} (hf : Multipliable f) : ∏' (n : ℕ), (f n * f (-(n + 1))) = ∏' (n : ℤ), f n

Full source

@[to_additive tsum_nat_add_neg_add_one]
lemma tprod_nat_mul_neg_add_one [T2Space M] {f : ℤ → M} (hf : Multipliable f) :
    ∏' (n : ℕ), (f n * f (-(n + 1))) = ∏' (n : ℤ), f n :=
  hf.hasProd.nat_mul_neg_add_one.tprod_eq

Product Equality for Paired Integer Terms over Natural Numbers

Informal description

Let $M$ be a Hausdorff commutative topological monoid and $f : \mathbb{Z} \to M$ be a multipliable function. Then the unconditional product of $f(n) \cdot f(-(n+1))$ over all natural numbers $n \in \mathbb{N}$ equals the unconditional product of $f$ over all integers $n \in \mathbb{Z}$, i.e., \[ \prod_{n \in \mathbb{N}}' (f(n) \cdot f(-(n+1))) = \prod_{n \in \mathbb{Z}}' f(n). \]

HasProd.of_nat_of_neg_add_one theorem

 {f : ℤ → M} (hf₁ : HasProd (fun n : ℕ ↦ f n) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') : HasProd f (m * m')

Full source

@[to_additive HasSum.of_nat_of_neg_add_one]
lemma HasProd.of_nat_of_neg_add_one {f : ℤ → M}
    (hf₁ : HasProd (fun n : ℕ ↦ f n) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') :
    HasProd f (m * m') := by
  have hi₂ : Injective Int.negSucc := @Int.negSucc.inj
  have : IsCompl (Set.range ((↑) : ℕ → ℤ)) (Set.range Int.negSucc) := by
    constructor
    · rw [disjoint_iff_inf_le]
      rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩
    · rw [codisjoint_iff_le_sup]
      rintro (i | j) <;> simp
  exact (Nat.cast_injective.hasProd_range_iff.mpr hf₁).mul_isCompl
    this (hi₂.hasProd_range_iff.mpr hf₂)

Product Convergence over Integers via Natural and Shifted Negative Integers: $m \cdot m'$

Informal description

Let $f : \mathbb{Z} \to M$ be a function in a commutative topological monoid $M$. If the product of $f$ over the natural numbers $\mathbb{N}$ converges to $m$ and the product of $f$ over the negative integers shifted by one (i.e., $n \mapsto f(-(n+1))$) converges to $m'$, then the product of $f$ over all integers $\mathbb{Z}$ converges to $m \cdot m'$.

Multipliable.of_nat_of_neg_add_one theorem

 {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : Multipliable f

Full source

@[to_additive Summable.of_nat_of_neg_add_one]
lemma Multipliable.of_nat_of_neg_add_one {f : ℤ → M}
    (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) :
    Multipliable f :=
  (hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).multipliable

Multipliability of Integer Function via Natural and Shifted Negative Parts

Informal description

Let $M$ be a commutative topological monoid and $f : \mathbb{Z} \to M$ be a function. If the restrictions of $f$ to the natural numbers $\mathbb{N}$ and to the negative integers shifted by one (i.e., $n \mapsto f(-(n+1))$) are both multipliable, then $f$ is multipliable over all integers $\mathbb{Z}$.

tprod_of_nat_of_neg_add_one theorem

 [T2Space M] {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) :
  ∏' n : ℤ, f n = (∏' n : ℕ, f n) * ∏' n : ℕ, f (-(n + 1))

Full source

@[to_additive tsum_of_nat_of_neg_add_one]
lemma tprod_of_nat_of_neg_add_one [T2Space M] {f : ℤ → M}
    (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) :
    ∏' n : ℤ, f n = (∏' n : ℕ, f n) * ∏' n : ℕ, f (-(n + 1)) :=
  (hf₁.hasProd.of_nat_of_neg_add_one hf₂.hasProd).tprod_eq

Unconditional Product over Integers as Product of Positive and Negative Parts

Informal description

Let $M$ be a Hausdorff topological space and a commutative monoid. For a function $f : \mathbb{Z} \to M$, if the products $\prod'_{n \in \mathbb{N}} f(n)$ and $\prod'_{n \in \mathbb{N}} f(-(n+1))$ both exist (i.e., the corresponding functions are multipliable), then the unconditional product over all integers satisfies \[ \prod'_{n \in \mathbb{Z}} f(n) = \left(\prod'_{n \in \mathbb{N}} f(n)\right) \cdot \left(\prod'_{n \in \mathbb{N}} f(-(n+1))\right). \]

HasProd.int_rec theorem

{f g : ℕ → M} (hf : HasProd f m) (hg : HasProd g m') : HasProd (Int.rec f g) (m * m')

Full source

/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have products `a`, `b` respectively, then
the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has
product `a + b`. -/
@[to_additive "If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have sums `a`, `b` respectively, then
the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has
sum `a + b`."]
lemma HasProd.int_rec {f g : ℕ → M} (hf : HasProd f m) (hg : HasProd g m') :
    HasProd (Int.rec f g) (m * m') :=
  HasProd.of_nat_of_neg_add_one hf hg

Product of Integer-Recursed Sequences: $m \cdot m'$

Informal description

Let $M$ be a commutative topological monoid, and let $f, g : \mathbb{N} \to M$ be sequences such that the product of $f$ converges to $m$ and the product of $g$ converges to $m'$. Then the $\mathbb{Z}$-indexed sequence defined by $h(n) = f(n)$ for $n \geq 0$ and $h(n) = g(-n - 1)$ for $n < 0$ has product $m \cdot m'$.

Multipliable.int_rec theorem

{f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) : Multipliable (Int.rec f g)

Full source

/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable then so is the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position). -/
@[to_additive "If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable then so is the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position)."]
lemma Multipliable.int_rec {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) :
    Multipliable (Int.rec f g) :=
  .of_nat_of_neg_add_one hf hg

Multipliability of Integer-Recursed Sequence from Multipliable Natural Sequences

Informal description

Let $M$ be a commutative topological monoid, and let $f, g : \mathbb{N} \to M$ be sequences. If $f$ and $g$ are both multipliable, then the $\mathbb{Z}$-indexed sequence defined by $h(n) = f(n)$ for $n \geq 0$ and $h(n) = g(-n - 1)$ for $n < 0$ is also multipliable.

tprod_int_rec theorem

 [T2Space M] {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) :
  ∏' n : ℤ, Int.rec f g n = (∏' n : ℕ, f n) * ∏' n : ℕ, g n

Full source

/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable, then the product of the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is
`(∏' n, f n) * ∏' n, g n`. -/
@[to_additive "If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable, then the sum of the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is
`∑' n, f n + ∑' n, g n`."]
lemma tprod_int_rec [T2Space M] {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) :
    ∏' n : ℤ, Int.rec f g n = (∏' n : ℕ, f n) * ∏' n : ℕ, g n :=
  (hf.hasProd.int_rec hg.hasProd).tprod_eq

Product of $\mathbb{Z}$-Indexed Sequence via $\mathbb{N}$-Indexed Sequences: $\prod'_{\mathbb{Z}} h = (\prod'_{\mathbb{N}} f) \cdot (\prod'_{\mathbb{N}} g)$

Informal description

Let $M$ be a Hausdorff topological commutative monoid, and let $f, g : \mathbb{N} \to M$ be sequences such that $f$ and $g$ are multipliable. Then the unconditional product of the $\mathbb{Z}$-indexed sequence defined by $h(n) = f(n)$ for $n \geq 0$ and $h(n) = g(-n - 1)$ for $n < 0$ is equal to the product of the unconditional products of $f$ and $g$, i.e., \[ \prod'_{n \in \mathbb{Z}} h(n) = \left(\prod'_{n \in \mathbb{N}} f(n)\right) \cdot \left(\prod'_{n \in \mathbb{N}} g(n)\right). \]

HasProd.nat_mul_neg theorem

{f : ℤ → M} (hf : HasProd f m) : HasProd (fun n : ℕ ↦ f n * f (-n)) (m * f 0)

Full source

@[to_additive]
theorem HasProd.nat_mul_neg {f : ℤ → M} (hf : HasProd f m) :
    HasProd (fun n : ℕ ↦ f n * f (-n)) (m * f 0) := by
  -- Note this is much easier to prove if you assume more about the target space, but we have to
  -- work hard to prove it under the very minimal assumptions here.
  apply (hf.mul (hasProd_ite_eq (0 : ℤ) (f 0))).hasProd_of_prod_eq fun u ↦ ?_
  refine ⟨u.image Int.natAbs, fun v' hv' ↦ ?_⟩
  let u1 := v'.image fun x : ℕ ↦ (x : ℤ)
  let u2 := v'.image fun x : ℕ ↦ -(x : ℤ)
  have A : u ⊆ u1 ∪ u2 := by
    intro x hx
    simp only [u1, u2, mem_union, mem_image, exists_prop]
    rcases le_total 0 x with (h'x | h'x)
    · refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [Int.natCast_natAbs, abs_eq_self, h'x]
    · refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [abs_of_nonpos h'x, Int.natCast_natAbs, neg_neg]
  exact ⟨_, A, calc
    (∏ x ∈ u1 ∪ u2, (f x * if x = 0 then f 0 else 1)) =
        (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x := by
      rw [prod_mul_distrib]
      congr 1
      refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm
      · intro x hx
        suffices x ≠ 0 by simp only [this, if_false]
        rintro rfl
        simp only [mem_sdiff, mem_union, mem_image, Nat.cast_eq_zero, exists_eq_right, neg_eq_zero,
          or_self, mem_inter, and_self, and_not_self, u1, u2] at hx
      · intro x hx
        simp only [u1, u2, mem_inter, mem_image, exists_prop] at hx
        suffices x = 0 by simp only [this, eq_self_iff_true, if_true]
        omega
    _ = (∏ x ∈ u1, f x) * ∏ x ∈ u2, f x := prod_union_inter
    _ = (∏ b ∈ v', f b) * ∏ b ∈ v', f (-b) := by
      simp only [u1, u2, Nat.cast_inj, imp_self, implies_true, forall_const, prod_image, neg_inj]
    _ = ∏ b ∈ v', (f b * f (-b)) := prod_mul_distrib.symm⟩

Product of Symmetric Terms: $\prod_{n\in\mathbb{N}} f(n)f(-n) = (\prod_{n\in\mathbb{Z}} f(n)) \cdot f(0)$

Informal description

Let $M$ be a commutative topological monoid and $f : \mathbb{Z} \to M$ be a function. If the product of $f$ over $\mathbb{Z}$ converges to $m$, then the product of the function $n \mapsto f(n) \cdot f(-n)$ over $\mathbb{N}$ converges to $m \cdot f(0)$.

Multipliable.nat_mul_neg theorem

{f : ℤ → M} (hf : Multipliable f) : Multipliable fun n : ℕ ↦ f n * f (-n)

Full source

@[to_additive]
theorem Multipliable.nat_mul_neg {f : ℤ → M} (hf : Multipliable f) :
    Multipliable fun n : ℕ ↦ f n * f (-n) :=
  hf.hasProd.nat_mul_neg.multipliable

Multipliability of Symmetric Product Terms: $n \mapsto f(n)f(-n)$ over $\mathbb{N}$

Informal description

Let $M$ be a commutative topological monoid and $f \colon \mathbb{Z} \to M$ be a multipliable function. Then the function $n \mapsto f(n) \cdot f(-n)$ is multipliable over $\mathbb{N}$.

tprod_nat_mul_neg theorem

[T2Space M] {f : ℤ → M} (hf : Multipliable f) : ∏' n : ℕ, (f n * f (-n)) = (∏' n : ℤ, f n) * f 0

Full source

@[to_additive]
lemma tprod_nat_mul_neg [T2Space M] {f : ℤ → M} (hf : Multipliable f) :
    ∏' n : ℕ, (f n * f (-n)) = (∏' n : ℤ, f n) * f 0 :=
  hf.hasProd.nat_mul_neg.tprod_eq

Product Identity: $\prod'_{n \in \mathbb{N}} f(n)f(-n) = (\prod'_{n \in \mathbb{Z}} f(n)) \cdot f(0)$

Informal description

Let $M$ be a Hausdorff commutative topological monoid and $f : \mathbb{Z} \to M$ be a multipliable function. Then the unconditional product of $f(n) \cdot f(-n)$ over $n \in \mathbb{N}$ equals the product of the unconditional product of $f$ over $\mathbb{Z}$ multiplied by $f(0)$, i.e., $$\prod'_{n \in \mathbb{N}} (f(n) \cdot f(-n)) = \left(\prod'_{n \in \mathbb{Z}} f(n)\right) \cdot f(0).$$

HasProd.of_add_one_of_neg_add_one theorem

 {f : ℤ → M} (hf₁ : HasProd (fun n : ℕ ↦ f (n + 1)) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') :
  HasProd f (m * f 0 * m')

Full source

@[to_additive HasSum.of_add_one_of_neg_add_one]
theorem HasProd.of_add_one_of_neg_add_one {f : ℤ → M}
    (hf₁ : HasProd (fun n : ℕ ↦ f (n + 1)) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') :
    HasProd f (m * f 0 * m') :=
  HasProd.of_nat_of_neg_add_one (mul_comm _ m ▸ HasProd.zero_mul hf₁) hf₂

Product Decomposition over Integers via Shifted Positive and Negative Terms: $m \cdot f(0) \cdot m'$

Informal description

Let $M$ be a commutative topological monoid and $f \colon \mathbb{Z} \to M$ be a function. If the product of the shifted function $n \mapsto f(n + 1)$ over $\mathbb{N}$ converges to $m$, and the product of the shifted negative function $n \mapsto f(-(n + 1))$ over $\mathbb{N}$ converges to $m'$, then the product of $f$ over all integers $\mathbb{Z}$ converges to $m \cdot f(0) \cdot m'$.

Multipliable.of_add_one_of_neg_add_one theorem

 {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1)) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : Multipliable f

Full source

@[to_additive Summable.of_add_one_of_neg_add_one]
lemma Multipliable.of_add_one_of_neg_add_one {f : ℤ → M}
    (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1)) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) :
    Multipliable f :=
  (hf₁.hasProd.of_add_one_of_neg_add_one hf₂.hasProd).multipliable

Multipliability of a Function on $\mathbb{Z}$ via Shifted Positive and Negative Terms

Informal description

Let $M$ be a commutative topological monoid and $f \colon \mathbb{Z} \to M$ be a function. If the function $n \mapsto f(n + 1)$ is multipliable over $\mathbb{N}$ and the function $n \mapsto f(-(n + 1))$ is multipliable over $\mathbb{N}$, then $f$ is multipliable over $\mathbb{Z}$.

tprod_of_add_one_of_neg_add_one theorem

 [T2Space M] {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1)) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) :
  ∏' n : ℤ, f n = (∏' n : ℕ, f (n + 1)) * f 0 * ∏' n : ℕ, f (-(n + 1))

Full source

@[to_additive tsum_of_add_one_of_neg_add_one]
lemma tprod_of_add_one_of_neg_add_one [T2Space M] {f : ℤ → M}
    (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1)) (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) :
    ∏' n : ℤ, f n = (∏' n : ℕ, f (n + 1)) * f 0 * ∏' n : ℕ, f (-(n + 1)) :=
  (hf₁.hasProd.of_add_one_of_neg_add_one hf₂.hasProd).tprod_eq

Product Decomposition Formula for Integer-Indexed Functions: $\prod_{\mathbb{Z}} f = (\prod_{\mathbb{N}} f(n+1)) \cdot f(0) \cdot (\prod_{\mathbb{N}} f(-(n+1)))$

Informal description

Let $M$ be a Hausdorff commutative topological monoid and $f \colon \mathbb{Z} \to M$ a function. If the function $n \mapsto f(n+1)$ is multipliable over $\mathbb{N}$ and the function $n \mapsto f(-(n+1))$ is multipliable over $\mathbb{N}$, then the unconditional product over all integers satisfies: \[ \prod_{n \in \mathbb{Z}} f(n) = \left(\prod_{n \in \mathbb{N}} f(n+1)\right) \cdot f(0) \cdot \left(\prod_{n \in \mathbb{N}} f(-(n+1))\right) \]

HasProd.of_nat_of_neg theorem

 {f : ℤ → G} (hf₁ : HasProd (fun n : ℕ ↦ f n) g) (hf₂ : HasProd (fun n : ℕ ↦ f (-n)) g') : HasProd f (g * g' / f 0)

Full source

@[to_additive]
lemma HasProd.of_nat_of_neg {f : ℤ → G} (hf₁ : HasProd (fun n : ℕ ↦ f n) g)
    (hf₂ : HasProd (fun n : ℕ ↦ f (-n)) g') : HasProd f (g * g' / f 0) := by
  refine mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_
  rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂

Product Convergence over Integers via Natural and Negative Integers: $g \cdot g' / f(0)$

Informal description

Let $G$ be a commutative topological group and $f : \mathbb{Z} \to G$ a function. If the product of $f$ over the natural numbers $\mathbb{N}$ converges to $g$ and the product of $f$ over the negative integers $\mathbb{N}$ (i.e., $n \mapsto f(-n)$) converges to $g'$, then the product of $f$ over all integers $\mathbb{Z}$ converges to $g \cdot g' / f(0)$.

Multipliable.of_nat_of_neg theorem

 {f : ℤ → G} (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) : Multipliable f

Full source

@[to_additive]
lemma Multipliable.of_nat_of_neg {f : ℤ → G} (hf₁ : Multipliable fun n : ℕ ↦ f n)
    (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) : Multipliable f :=
  (hf₁.hasProd.of_nat_of_neg hf₂.hasProd).multipliable

Multipliability over Integers via Natural and Negative Integers

Informal description

Let $G$ be a commutative topological group and $f : \mathbb{Z} \to G$ a function. If the restriction of $f$ to the natural numbers $\mathbb{N}$ is multipliable and the restriction of $f$ to the negative integers (via $n \mapsto f(-n)$) is also multipliable, then $f$ is multipliable over all integers $\mathbb{Z}$.

Multipliable.tprod_of_nat_of_neg theorem

 [T2Space G] {f : ℤ → G} (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) :
  ∏' n : ℤ, f n = (∏' n : ℕ, f n) * (∏' n : ℕ, f (-n)) / f 0

Full source

@[to_additive]
protected lemma Multipliable.tprod_of_nat_of_neg [T2Space G] {f : ℤ → G}
    (hf₁ : Multipliable fun n : ℕ ↦ f n) (hf₂ : Multipliable fun n : ℕ ↦ f (-n)) :
    ∏' n : ℤ, f n = (∏' n : ℕ, f n) * (∏' n : ℕ, f (-n)) / f 0 :=
  (hf₁.hasProd.of_nat_of_neg hf₂.hasProd).tprod_eq

Unconditional Product over Integers via Natural and Negative Integers: $\prod'_{\mathbb{Z}} f = (\prod'_{\mathbb{N}} f) \cdot (\prod'_{\mathbb{N}} f \circ (-)) / f(0)$

Informal description

Let $G$ be a Hausdorff commutative topological group and $f : \mathbb{Z} \to G$ a function. If the function $f$ restricted to the natural numbers $\mathbb{N}$ is multipliable and the function $n \mapsto f(-n)$ is also multipliable, then the unconditional product over all integers satisfies \[ \prod'_{n \in \mathbb{Z}} f(n) = \left(\prod'_{n \in \mathbb{N}} f(n)\right) \cdot \left(\prod'_{n \in \mathbb{N}} f(-n)\right) / f(0). \]

multipliable_int_iff_multipliable_nat_and_neg_add_one theorem

{f : ℤ → G} : Multipliable f ↔ (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-(n + 1)))

Full source

/-- "iff" version of `Multipliable.of_nat_of_neg_add_one`. -/
@[to_additive "\"iff\" version of `Summable.of_nat_of_neg_add_one`."]
lemma multipliable_int_iff_multipliable_nat_and_neg_add_one {f : ℤ → G} : MultipliableMultipliable f ↔
    (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-(n + 1))) := by
  refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩ <;>
  apply p.comp_injective
  exacts [Nat.cast_injective, @Int.negSucc.inj]

Multipliability over Integers via Natural and Shifted Negative Parts: $\text{Multipliable}(f) \leftrightarrow \text{Multipliable}(f|_{\mathbb{N}}) \land \text{Multipliable}(n \mapsto f(-(n+1)))$

Informal description

Let $G$ be a commutative topological group and $f : \mathbb{Z} \to G$ a function. Then $f$ is multipliable if and only if both the restriction of $f$ to the natural numbers $\mathbb{N}$ is multipliable and the function $n \mapsto f(-(n + 1))$ is multipliable over $\mathbb{N}$.

multipliable_int_iff_multipliable_nat_and_neg theorem

{f : ℤ → G} : Multipliable f ↔ (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-n))

Full source

/-- "iff" version of `Multipliable.of_nat_of_neg`. -/
@[to_additive "\"iff\" version of `Summable.of_nat_of_neg`."]
lemma multipliable_int_iff_multipliable_nat_and_neg {f : ℤ → G} :
    MultipliableMultipliable f ↔ (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-n)) := by
  refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩ <;>
  apply p.comp_injective
  exacts [Nat.cast_injective, neg_injective.comp Nat.cast_injective]

Multipliability over Integers Equivalence: $\text{Multipliable}(f) \leftrightarrow \text{Multipliable}(f|_{\mathbb{N}}) \land \text{Multipliable}(n \mapsto f(-n))$

Informal description

Let $G$ be a commutative topological group and $f : \mathbb{Z} \to G$ a function. Then $f$ is multipliable if and only if both the restriction of $f$ to the natural numbers $\mathbb{N}$ is multipliable and the function $n \mapsto f(-n)$ is multipliable on $\mathbb{N}$.

pnat_multipliable_iff_multipliable_succ theorem

 {α : Type*} [TopologicalSpace α] [CommMonoid α] {f : ℕ → α} :
  Multipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1)

Full source

@[to_additive]
theorem pnat_multipliable_iff_multipliable_succ {α : Type*} [TopologicalSpace α] [CommMonoid α]
    {f : ℕ → α} : MultipliableMultipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1) :=
  Equiv.pnatEquivNat.symm.multipliable_iff.symm

Multipliability Equivalence for Positive Naturals and Shifted Function

Informal description

Let $\alpha$ be a topological space with a commutative monoid structure, and let $f : \mathbb{N} \to \alpha$ be a function. The function $f$ restricted to positive natural numbers is multipliable if and only if the shifted function $n \mapsto f(n + 1)$ is multipliable over all natural numbers. In other words, the following equivalence holds: \[ \text{Multipliable} (f \restriction \mathbb{N}^+) \leftrightarrow \text{Multipliable} (n \mapsto f(n + 1)). \]

tprod_pnat_eq_tprod_succ theorem

{α : Type*} [TopologicalSpace α] [CommMonoid α] (f : ℕ → α) : ∏' n : ℕ+, f n = ∏' n, f (n + 1)

Full source

@[to_additive]
theorem tprod_pnat_eq_tprod_succ {α : Type*} [TopologicalSpace α] [CommMonoid α] (f : ℕ → α) :
    ∏' n : ℕ+, f n = ∏' n, f (n + 1) := (Equiv.pnatEquivNat.symm.tprod_eq _).symm

Equality of Unconditional Products: $\prod'_{\mathbb{N}^+} f(n) = \prod'_{\mathbb{N}} f(n+1)$

Informal description

Let $\alpha$ be a topological space equipped with a commutative monoid structure, and let $f \colon \mathbb{N} \to \alpha$ be a function. The unconditional product of $f$ over the positive natural numbers $\mathbb{N}^+$ is equal to the unconditional product of the shifted function $n \mapsto f(n + 1)$ over all natural numbers $\mathbb{N}$. That is, \[ \prod'_{n \in \mathbb{N}^+} f(n) = \prod'_{n \in \mathbb{N}} f(n + 1). \]