Mathlib.Topology.Algebra.InfiniteSum.Group

HasProd.inv theorem

(h : HasProd f a) : HasProd (fun b ↦ (f b)⁻¹) a⁻¹

Full source

@[to_additive]
theorem HasProd.inv (h : HasProd f a) : HasProd (fun b ↦ (f b)⁻¹) a⁻¹ := by
  simpa only using h.map (MonoidHom.id α)⁻¹ continuous_inv

Inversion Preserves Product Convergence: $\prod_b (f(b))^{-1} = (\prod_b f(b))^{-1}$

Informal description

Let $\alpha$ be a topological group and $f \colon \beta \to \alpha$ be a function such that the product of $f$ converges to $a \in \alpha$. Then the product of the pointwise inverses $(f(b))^{-1}$ converges to the inverse $a^{-1}$.

Multipliable.inv theorem

(hf : Multipliable f) : Multipliable fun b ↦ (f b)⁻¹

Full source

@[to_additive]
theorem Multipliable.inv (hf : Multipliable f) : Multipliable fun b ↦ (f b)⁻¹ :=
  hf.hasProd.inv.multipliable

Multipliability under pointwise inversion: $f$ multipliable $\Rightarrow$ $f^{-1}$ multipliable

Informal description

If a function $f \colon \beta \to \alpha$ is multipliable in a topological group $\alpha$, then the function $\lambda b, (f b)^{-1}$ (pointwise inversion of $f$) is also multipliable.

Multipliable.of_inv theorem

(hf : Multipliable fun b ↦ (f b)⁻¹) : Multipliable f

Full source

@[to_additive]
theorem Multipliable.of_inv (hf : Multipliable fun b ↦ (f b)⁻¹) : Multipliable f := by
  simpa only [inv_inv] using hf.inv

Multipliability from Inversion: $f^{-1}$ multipliable $\Rightarrow$ $f$ multipliable

Informal description

If the pointwise inverse function $b \mapsto (f(b))^{-1}$ is multipliable in a topological group $\alpha$, then the original function $f \colon \beta \to \alpha$ is also multipliable.

multipliable_inv_iff theorem

: (Multipliable fun b ↦ (f b)⁻¹) ↔ Multipliable f

Full source

@[to_additive]
theorem multipliable_inv_iff : (Multipliable fun b ↦ (f b)⁻¹) ↔ Multipliable f :=
  ⟨Multipliable.of_inv, Multipliable.inv⟩

Multipliability of Pointwise Inverse: $f^{-1}$ multipliable $\leftrightarrow$ $f$ multipliable

Informal description

For a function $f \colon \beta \to \alpha$ where $\alpha$ is a topological group, the function $b \mapsto (f(b))^{-1}$ is multipliable if and only if $f$ is multipliable.

HasProd.div theorem

(hf : HasProd f a₁) (hg : HasProd g a₂) : HasProd (fun b ↦ f b / g b) (a₁ / a₂)

Full source

@[to_additive]
theorem HasProd.div (hf : HasProd f a₁) (hg : HasProd g a₂) :
    HasProd (fun b ↦ f b / g b) (a₁ / a₂) := by
  simp only [div_eq_mul_inv]
  exact hf.mul hg.inv

Convergence of Pointwise Division: $\prod_b (f(b)/g(b)) = (\prod_b f(b)) / (\prod_b g(b))$

Informal description

Let $\alpha$ be a topological group and $f, g \colon \beta \to \alpha$ be functions such that the product of $f$ converges to $a_1 \in \alpha$ and the product of $g$ converges to $a_2 \in \alpha$. Then the pointwise division function $b \mapsto f(b)/g(b)$ has product $a_1/a_2$.

Multipliable.div theorem

(hf : Multipliable f) (hg : Multipliable g) : Multipliable fun b ↦ f b / g b

Full source

@[to_additive]
theorem Multipliable.div (hf : Multipliable f) (hg : Multipliable g) :
    Multipliable fun b ↦ f b / g b :=
  (hf.hasProd.div hg.hasProd).multipliable

Multipliability of Pointwise Division

Informal description

Let $\alpha$ be a topological group and $f, g \colon \beta \to \alpha$ be functions. If $f$ and $g$ are multipliable, then the pointwise division function $b \mapsto f(b)/g(b)$ is also multipliable.

Multipliable.trans_div theorem

(hg : Multipliable g) (hfg : Multipliable fun b ↦ f b / g b) : Multipliable f

Full source

@[to_additive]
theorem Multipliable.trans_div (hg : Multipliable g) (hfg : Multipliable fun b ↦ f b / g b) :
    Multipliable f := by
  simpa only [div_mul_cancel] using hfg.mul hg

Multipliability Transfer via Division: $g$ and $f/g$ multipliable implies $f$ multipliable

Informal description

Let $\alpha$ be a topological group and $f, g \colon \beta \to \alpha$ be functions. If $g$ is multipliable and the function $b \mapsto f(b)/g(b)$ is multipliable, then $f$ is multipliable.

multipliable_iff_of_multipliable_div theorem

(hfg : Multipliable fun b ↦ f b / g b) : Multipliable f ↔ Multipliable g

Full source

@[to_additive]
theorem multipliable_iff_of_multipliable_div (hfg : Multipliable fun b ↦ f b / g b) :
    MultipliableMultipliable f ↔ Multipliable g :=
  ⟨fun hf ↦ hf.trans_div <| by simpa only [inv_div] using hfg.inv, fun hg ↦ hg.trans_div hfg⟩

Multipliability Equivalence via Division: $f/g$ multipliable implies ($f$ multipliable $\leftrightarrow$ $g$ multipliable)

Informal description

Let $\alpha$ be a topological group and $f, g \colon \beta \to \alpha$ be functions. If the function $b \mapsto f(b)/g(b)$ is multipliable, then $f$ is multipliable if and only if $g$ is multipliable.

HasProd.update theorem

(hf : HasProd f a₁) (b : β) [DecidableEq β] (a : α) : HasProd (update f b a) (a / f b * a₁)

Full source

@[to_additive]
theorem HasProd.update (hf : HasProd f a₁) (b : β) [DecidableEq β] (a : α) :
    HasProd (update f b a) (a / f b * a₁) := by
  convert (hasProd_ite_eq b (a / f b)).mul hf with b'
  by_cases h : b' = b
  · rw [h, update_self]
    simp [eq_self_iff_true, if_true, sub_add_cancel]
  · simp only [h, update_of_ne, if_false, Ne, one_mul, not_false_iff]

Product of Updated Function: $\text{update } f \, b \, a$ has product $a/f(b) \cdot a_1$

Informal description

Let $f \colon \beta \to \alpha$ be a function with product $a_1$ in a topological group $\alpha$, and let $b \in \beta$ with decidable equality. For any $a \in \alpha$, the updated function $\text{update } f \, b \, a$ (which equals $a$ at $b$ and $f$ elsewhere) has product $a/f(b) \cdot a_1$.

Multipliable.update theorem

(hf : Multipliable f) (b : β) [DecidableEq β] (a : α) : Multipliable (update f b a)

Full source

@[to_additive]
theorem Multipliable.update (hf : Multipliable f) (b : β) [DecidableEq β] (a : α) :
    Multipliable (update f b a) :=
  (hf.hasProd.update b a).multipliable

Multipliability of Updated Function in Topological Groups

Informal description

Let $\alpha$ be a topological group and $f \colon \beta \to \alpha$ be a multipliable function. For any $b \in \beta$ (with decidable equality) and any $a \in \alpha$, the updated function $\text{update } f \, b \, a$ (which equals $a$ at $b$ and $f$ elsewhere) is also multipliable.

HasProd.hasProd_compl_iff theorem

 {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) : HasProd (f ∘ (↑) : ↑sᶜ → α) a₂ ↔ HasProd f (a₁ * a₂)

Full source

@[to_additive]
theorem HasProd.hasProd_compl_iff {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) :
    HasProdHasProd (f ∘ (↑) : ↑sᶜ → α) a₂ ↔ HasProd f (a₁ * a₂) := by
  refine ⟨fun h ↦ hf.mul_compl h, fun h ↦ ?_⟩
  rw [hasProd_subtype_iff_mulIndicator] at hf ⊢
  rw [Set.mulIndicator_compl]
  simpa only [div_eq_mul_inv, mul_inv_cancel_comm] using h.div hf

Product Decomposition over Complementary Subsets: $a_1 \cdot a_2$ for $s$ and $s^\complement$

Informal description

Let $f : \beta \to \alpha$ be a function and $s \subseteq \beta$ a subset. If the restriction of $f$ to $s$ has product $a_1$, then the restriction of $f$ to the complement $s^\complement$ has product $a_2$ if and only if the product of $f$ over all of $\beta$ exists and equals $a_1 \cdot a_2$.

HasProd.hasProd_iff_compl theorem

 {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) : HasProd f a₂ ↔ HasProd (f ∘ (↑) : ↑sᶜ → α) (a₂ / a₁)

Full source

@[to_additive]
theorem HasProd.hasProd_iff_compl {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) :
    HasProdHasProd f a₂ ↔ HasProd (f ∘ (↑) : ↑sᶜ → α) (a₂ / a₁) :=
  Iff.symm <| hf.hasProd_compl_iff.trans <| by rw [mul_div_cancel]

Product Decomposition Criterion via Complement: $a_2$ vs $a_2 / a_1$

Informal description

Let $f : \beta \to \alpha$ be a function and $s \subseteq \beta$ a subset. If the restriction of $f$ to $s$ has product $a_1$, then the product of $f$ over all of $\beta$ exists and equals $a_2$ if and only if the restriction of $f$ to the complement $s^\complement$ has product $a_2 / a_1$.

Multipliable.multipliable_compl_iff theorem

 {s : Set β} (hf : Multipliable (f ∘ (↑) : s → α)) : Multipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f

Full source

@[to_additive]
theorem Multipliable.multipliable_compl_iff {s : Set β} (hf : Multipliable (f ∘ (↑) : s → α)) :
    MultipliableMultipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f where
  mp := fun ⟨_, ha⟩ ↦ (hf.hasProd.hasProd_compl_iff.1 ha).multipliable
  mpr := fun ⟨_, ha⟩ ↦ (hf.hasProd.hasProd_iff_compl.1 ha).multipliable

Multipliability Criterion via Complement: $f|_{s^\complement}$ vs $f$

Informal description

Let $f \colon \beta \to \alpha$ be a function and $s \subseteq \beta$ a subset. If the restriction $f|_s$ is multipliable, then the restriction $f|_{s^\complement}$ to the complement is multipliable if and only if $f$ itself is multipliable.

Finset.hasProd_compl_iff theorem

(s : Finset β) : HasProd (fun x : { x // x ∉ s } ↦ f x) a ↔ HasProd f (a * ∏ i ∈ s, f i)

Full source

@[to_additive]
protected theorem Finset.hasProd_compl_iff (s : Finset β) :
    HasProdHasProd (fun x : { x // x ∉ s } ↦ f x) a ↔ HasProd f (a * ∏ i ∈ s, f i) :=
  (s.hasProd f).hasProd_compl_iff.trans <| by rw [mul_comm]

Product convergence on complement set: $a$ vs $a \cdot \prod_{i \in s} f(i)$

Informal description

For any finite set $s \subseteq \beta$ and function $f \colon \beta \to \alpha$, the product of $f$ restricted to the complement of $s$ converges to $a$ if and only if the product of $f$ over all of $\beta$ converges to $a \cdot \prod_{i \in s} f(i)$.

Finset.hasProd_iff_compl theorem

(s : Finset β) : HasProd f a ↔ HasProd (fun x : { x // x ∉ s } ↦ f x) (a / ∏ i ∈ s, f i)

Full source

@[to_additive]
protected theorem Finset.hasProd_iff_compl (s : Finset β) :
    HasProdHasProd f a ↔ HasProd (fun x : { x // x ∉ s } ↦ f x) (a / ∏ i ∈ s, f i) :=
  (s.hasProd f).hasProd_iff_compl

Product Decomposition Criterion for Finite Complements: $a$ vs $a / \prod_{i \in s} f(i)$

Informal description

Let $f \colon \beta \to \alpha$ be a function and $s \subseteq \beta$ a finite subset. The product of $f$ over all of $\beta$ exists and equals $a$ if and only if the product of $f$ restricted to the complement of $s$ exists and equals $a / \prod_{i \in s} f(i)$.

Finset.multipliable_compl_iff theorem

(s : Finset β) : (Multipliable fun x : { x // x ∉ s } ↦ f x) ↔ Multipliable f

Full source

@[to_additive]
protected theorem Finset.multipliable_compl_iff (s : Finset β) :
    (Multipliable fun x : { x // x ∉ s } ↦ f x) ↔ Multipliable f :=
  (s.multipliable f).multipliable_compl_iff

Multipliability Criterion for Finite Complements: $f|_{s^\complement}$ vs $f$

Informal description

For any finite subset $s \subseteq \beta$ and function $f \colon \beta \to \alpha$, the restriction of $f$ to the complement of $s$ is multipliable if and only if $f$ itself is multipliable.

Set.Finite.multipliable_compl_iff theorem

{s : Set β} (hs : s.Finite) : Multipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f

Full source

@[to_additive]
theorem Set.Finite.multipliable_compl_iff {s : Set β} (hs : s.Finite) :
    MultipliableMultipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f :=
  (hs.multipliable f).multipliable_compl_iff

Multipliability of $f$ vs. $f|_{s^\complement}$ for finite $s$

Informal description

Let $f \colon \beta \to \alpha$ be a function into a topological monoid $\alpha$, and let $s \subseteq \beta$ be a finite subset. Then the restriction of $f$ to the complement $s^\complement$ is multipliable if and only if $f$ itself is multipliable.

hasProd_ite_div_hasProd theorem

[DecidableEq β] (hf : HasProd f a) (b : β) : HasProd (fun n ↦ ite (n = b) 1 (f n)) (a / f b)

Full source

@[to_additive]
theorem hasProd_ite_div_hasProd [DecidableEq β] (hf : HasProd f a) (b : β) :
    HasProd (fun n ↦ ite (n = b) 1 (f n)) (a / f b) := by
  convert hf.update b 1 using 1
  · ext n
    rw [Function.update_apply]
  · rw [div_mul_eq_mul_div, one_mul]

Product of Modified Function: $g(n) = \mathbb{1}_{n=b} + f(n)\mathbb{1}_{n \neq b}$ has product $a/f(b)$

Informal description

Let $\alpha$ be a topological group, $\beta$ a type with decidable equality, and $f \colon \beta \to \alpha$ a function with product $a$. For any $b \in \beta$, the function defined by \[ g(n) = \begin{cases} 1 & \text{if } n = b, \\ f(n) & \text{otherwise} \end{cases} \] has product $a / f(b)$.

Multipliable.congr_cofinite theorem

(hf : Multipliable f) (hfg : f =ᶠ[cofinite] g) : Multipliable g

Full source

/-- A more general version of `Multipliable.congr`, allowing the functions to
disagree on a finite set.

Note that this requires the target to be a group, and hence fails for products valued
in a ring. See `Multipliable.congr_cofinite₀` for a version applying in this case,
with an additional non-vanishing hypothesis.
-/
@[to_additive "A more general version of `Summable.congr`, allowing the functions to
disagree on a finite set."]
theorem Multipliable.congr_cofinite (hf : Multipliable f) (hfg : f =ᶠ[cofinite] g) :
    Multipliable g :=
  hfg.multipliable_compl_iff.mp <| (hfg.multipliable_compl_iff.mpr hf).congr (by simp)

Multipliability Preserved Under Cofinite Equality in Topological Groups

Informal description

Let $f, g \colon \beta \to \alpha$ be functions into a topological group $\alpha$. If $f$ is multipliable and $f$ and $g$ agree on the complement of a finite set (i.e., $f = g$ cofinitely), then $g$ is also multipliable.

multipliable_congr_cofinite theorem

(hfg : f =ᶠ[cofinite] g) : Multipliable f ↔ Multipliable g

Full source

/-- A more general version of `multipliable_congr`, allowing the functions to
disagree on a finite set. -/
@[to_additive "A more general version of `summable_congr`, allowing the functions to
disagree on a finite set."]
theorem multipliable_congr_cofinite (hfg : f =ᶠ[cofinite] g) :
    MultipliableMultipliable f ↔ Multipliable g :=
  ⟨fun h ↦ h.congr_cofinite hfg, fun h ↦ h.congr_cofinite (hfg.mono fun _ h' ↦ h'.symm)⟩

Multipliability Equivalence Under Cofinite Equality in Topological Groups

Informal description

Let $f, g \colon \beta \to \alpha$ be functions into a topological group $\alpha$. Then $f$ is multipliable if and only if $g$ is multipliable, provided that $f$ and $g$ agree on the complement of a finite set (i.e., $f = g$ cofinitely).

Multipliable.congr_atTop theorem

{f₁ g₁ : ℕ → α} (hf : Multipliable f₁) (hfg : f₁ =ᶠ[atTop] g₁) : Multipliable g₁

Full source

@[to_additive]
theorem Multipliable.congr_atTop {f₁ g₁ : ℕ → α} (hf : Multipliable f₁) (hfg : f₁ =ᶠ[atTop] g₁) :
    Multipliable g₁ := hf.congr_cofinite (Nat.cofinite_eq_atTop ▸ hfg)

Multipliability Preserved Under Eventual Equality in Topological Groups

Informal description

Let $\alpha$ be a topological group and let $f_1, g_1 \colon \mathbb{N} \to \alpha$ be functions. If $f_1$ is multipliable and $f_1$ and $g_1$ eventually agree (i.e., $f_1(n) = g_1(n)$ for all sufficiently large $n$), then $g_1$ is also multipliable.

multipliable_congr_atTop theorem

{f₁ g₁ : ℕ → α} (hfg : f₁ =ᶠ[atTop] g₁) : Multipliable f₁ ↔ Multipliable g₁

Full source

@[to_additive]
theorem multipliable_congr_atTop {f₁ g₁ : ℕ → α} (hfg : f₁ =ᶠ[atTop] g₁) :
    MultipliableMultipliable f₁ ↔ Multipliable g₁ := multipliable_congr_cofinite (Nat.cofinite_eq_atTop ▸ hfg)

Multipliability Equivalence Under Eventual Equality in Topological Groups

Informal description

Let $\alpha$ be a topological group and let $f_1, g_1 \colon \mathbb{N} \to \alpha$ be functions. Then $f_1$ is multipliable if and only if $g_1$ is multipliable, provided that $f_1$ and $g_1$ eventually agree (i.e., $f_1(n) = g_1(n)$ for all sufficiently large $n$).

tprod_inv theorem

: ∏' b, (f b)⁻¹ = (∏' b, f b)⁻¹

Full source

@[to_additive]
theorem tprod_inv : ∏' b, (f b)⁻¹ = (∏' b, f b)⁻¹ := by
  by_cases hf : Multipliable f
  · exact hf.hasProd.inv.tprod_eq
  · simp [tprod_eq_one_of_not_multipliable hf,
      tprod_eq_one_of_not_multipliable (mt Multipliable.of_inv hf)]

Inversion of Unconditional Product: $\prod'_{b} (f(b))^{-1} = (\prod'_{b} f(b))^{-1}$

Informal description

Let $\alpha$ be a topological group and $f \colon \beta \to \alpha$ be a function. The unconditional product of the pointwise inverses $\prod'_{b} (f(b))^{-1}$ is equal to the inverse of the unconditional product $(\prod'_{b} f(b))^{-1}$.

Multipliable.tprod_div theorem

(hf : Multipliable f) (hg : Multipliable g) : ∏' b, (f b / g b) = (∏' b, f b) / ∏' b, g b

Full source

@[to_additive]
protected theorem Multipliable.tprod_div (hf : Multipliable f) (hg : Multipliable g) :
    ∏' b, (f b / g b) = (∏' b, f b) / ∏' b, g b :=
  (hf.hasProd.div hg.hasProd).tprod_eq

Unconditional Product of Pointwise Division: $\prod' (f/g) = (\prod' f) / (\prod' g)$

Informal description

Let $\alpha$ be a topological group and $f, g \colon \beta \to \alpha$ be multipliable functions. Then the unconditional product of their pointwise division satisfies \[ \prod'_{b} \left( \frac{f(b)}{g(b)} \right) = \left( \prod'_{b} f(b) \right) \Big/ \left( \prod'_{b} g(b) \right). \]

Multipliable.prod_mul_tprod_compl theorem

{s : Finset β} (hf : Multipliable f) : (∏ x ∈ s, f x) * ∏' x : ↑(s : Set β)ᶜ, f x = ∏' x, f x

Full source

@[to_additive]
protected theorem Multipliable.prod_mul_tprod_compl {s : Finset β} (hf : Multipliable f) :
    (∏ x ∈ s, f x) * ∏' x : ↑(s : Set β)ᶜ, f x = ∏' x, f x :=
  ((s.hasProd f).mul_compl (s.multipliable_compl_iff.2 hf).hasProd).tprod_eq.symm

Product Decomposition Formula: Finite Part and Complement

Informal description

Let $\alpha$ be a topological group and $f \colon \beta \to \alpha$ be a multipliable function. For any finite subset $s \subseteq \beta$, the product of $f$ over $s$ multiplied by the unconditional product of $f$ over the complement of $s$ equals the unconditional product of $f$ over all of $\beta$. That is, \[ \left( \prod_{x \in s} f(x) \right) \cdot \left( \prod'_{x \in s^\complement} f(x) \right) = \prod'_{x} f(x). \]

Multipliable.tprod_eq_mul_tprod_ite theorem

[DecidableEq β] (hf : Multipliable f) (b : β) : ∏' n, f n = f b * ∏' n, ite (n = b) 1 (f n)

Full source

/-- Let `f : β → α` be a multipliable function and let `b ∈ β` be an index.
Lemma `tprod_eq_mul_tprod_ite` writes `∏ n, f n` as `f b` times the product of the
remaining terms. -/
@[to_additive "Let `f : β → α` be a summable function and let `b ∈ β` be an index.
Lemma `tsum_eq_add_tsum_ite` writes `Σ' n, f n` as `f b` plus the sum of the
remaining terms."]
protected theorem Multipliable.tprod_eq_mul_tprod_ite [DecidableEq β] (hf : Multipliable f)
    (b : β) : ∏' n, f n = f b * ∏' n, ite (n = b) 1 (f n) := by
  rw [(hasProd_ite_div_hasProd hf.hasProd b).tprod_eq]
  exact (mul_div_cancel _ _).symm

Product Decomposition: $\prod' f = f(b) \cdot \prod' (1_{n=b} + f(n)1_{n \neq b})$

Informal description

Let $\alpha$ be a topological group, $\beta$ a type with decidable equality, and $f \colon \beta \to \alpha$ a multipliable function. For any index $b \in \beta$, the unconditional product $\prod'_{n} f(n)$ can be expressed as: \[ \prod'_{n} f(n) = f(b) \cdot \left( \prod'_{n} \begin{cases} 1 & \text{if } n = b, \\ f(n) & \text{otherwise} \end{cases} \right). \]

multipliable_iff_cauchySeq_finset theorem

[CompleteSpace α] {f : β → α} : Multipliable f ↔ CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b

Full source

/-- The **Cauchy criterion** for infinite products, also known as the **Cauchy convergence test** -/
@[to_additive "The **Cauchy criterion** for infinite sums, also known as the
**Cauchy convergence test**"]
theorem multipliable_iff_cauchySeq_finset [CompleteSpace α] {f : β → α} :
    MultipliableMultipliable f ↔ CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b := by
  classical exact cauchy_map_iff_exists_tendsto.symm

Cauchy Criterion for Multipliability in Complete Topological Groups

Informal description

Let $\alpha$ be a complete topological group and $f : \beta \to \alpha$ a function. Then $f$ is multipliable (i.e., the infinite product $\prod_{b \in \beta} f(b)$ converges) if and only if the sequence of partial products $\left( \prod_{b \in s} f(b) \right)_{s \in \text{Finset}(\beta)}$ is a Cauchy sequence, where the index $s$ ranges over all finite subsets of $\beta$.

cauchySeq_finset_iff_prod_vanishing theorem

 : (CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e

Full source

@[to_additive]
theorem cauchySeq_finset_iff_prod_vanishing :
    (CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b) ↔
      ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e := by
  classical
  simp only [CauchySeq, cauchy_map_iff, and_iff_right atTop_neBot, prod_atTop_atTop_eq,
    uniformity_eq_comap_nhds_one α, tendsto_comap_iff, Function.comp_def, atTop_neBot, true_and]
  rw [tendsto_atTop']
  constructor
  · intro h e he
    obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he
    use s₁ ∪ s₂
    intro t ht
    specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩
    simpa only [Finset.prod_union ht.symm, mul_div_cancel_left] using h
  · rintro h e he
    rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩
    rcases h d hd with ⟨s, h⟩
    use (s, s)
    rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
    have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
      rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]
    simp only [this]
    exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

Cauchy Criterion for Infinite Products in Topological Groups

Informal description

For a function $f : \beta \to \alpha$ in a complete topological group $\alpha$, the sequence of partial products $\prod_{b \in s} f(b)$ (indexed by finite subsets $s \subseteq \beta$) is Cauchy if and only if for every neighborhood $e$ of the identity $1 \in \alpha$, there exists a finite subset $s \subseteq \beta$ such that for any finite subset $t \subseteq \beta$ disjoint from $s$, the product $\prod_{b \in t} f(b)$ belongs to $e$.

cauchySeq_finset_iff_tprod_vanishing theorem

 :
  (CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b) ↔
    ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e

Full source

@[to_additive]
theorem cauchySeq_finset_iff_tprod_vanishing :
    (CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b) ↔
      ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e := by
  simp_rw [cauchySeq_finset_iff_prod_vanishing, Set.disjoint_left, disjoint_left]
  refine ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
  · obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he
    obtain ⟨s, hs⟩ := vanish o ho
    refine ⟨s, fun t hts ↦ oe ?_⟩
    by_cases ht : Multipliable fun a : t ↦ f a
    · classical
      refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)
      rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]
      apply hs
      simp_rw [Finset.mem_map]
      rintro _ ⟨b, -, rfl⟩
      exact hts b.prop
    · exact tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho
  · obtain ⟨s, hs⟩ := vanish _ he
    exact ⟨s, fun t hts ↦ (t.tprod_subtype f).symm ▸ hs _ hts⟩

Cauchy Criterion for Infinite Products via Unconditional Products in Topological Groups

Informal description

Let $\alpha$ be a topological group and $f : \beta \to \alpha$ a function. The sequence of partial products $\left( \prod_{b \in s} f(b) \right)_{s \in \text{Finset}(\beta)}$ is a Cauchy sequence if and only if for every neighborhood $e$ of the identity element $1 \in \alpha$, there exists a finite subset $s \subseteq \beta$ such that for any subset $t \subseteq \beta$ disjoint from $s$, the unconditional product $\prod'_{b \in t} f(b)$ belongs to $e$.

multipliable_iff_vanishing theorem

: Multipliable f ↔ ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e

Full source

@[to_additive]
theorem multipliable_iff_vanishing :
    MultipliableMultipliable f ↔
    ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e := by
  rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_prod_vanishing]

Vanishing Criterion for Multipliability in Topological Groups

Informal description

Let $\alpha$ be a topological group and $f : \beta \to \alpha$ a function. Then $f$ is multipliable (i.e., the infinite product $\prod_{b \in \beta} f(b)$ converges) if and only if for every neighborhood $e$ of the identity element $1 \in \alpha$, there exists a finite subset $s \subseteq \beta$ such that for any finite subset $t \subseteq \beta$ disjoint from $s$, the product $\prod_{b \in t} f(b)$ belongs to $e$.

multipliable_iff_tprod_vanishing theorem

 : Multipliable f ↔ ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e

Full source

@[to_additive]
theorem multipliable_iff_tprod_vanishing : MultipliableMultipliable f ↔
    ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e := by
  rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing]

Multipliability Criterion via Unconditional Product Vanishing in Topological Groups

Informal description

Let $\alpha$ be a topological group and $f : \beta \to \alpha$ a function. Then $f$ is multipliable (i.e., the infinite product $\prod_{b \in \beta} f(b)$ converges) if and only if for every neighborhood $e$ of the identity element $1 \in \alpha$, there exists a finite subset $s \subseteq \beta$ such that for any subset $t \subseteq \beta$ disjoint from $s$, the unconditional product $\prod'_{b \in t} f(b)$ belongs to $e$.

Multipliable.multipliable_of_eq_one_or_self theorem

(hf : Multipliable f) (h : ∀ b, g b = 1 ∨ g b = f b) : Multipliable g

Full source

@[to_additive]
theorem Multipliable.multipliable_of_eq_one_or_self (hf : Multipliable f)
    (h : ∀ b, g b = 1 ∨ g b = f b) : Multipliable g := by
  classical
  exact multipliable_iff_vanishing.2 fun e he ↦
    let ⟨s, hs⟩ := multipliable_iff_vanishing.1 hf e he
    ⟨s, fun t ht ↦
      have eq : ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t, g b :=
        calc
          ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t with g b = f b, g b :=
            Finset.prod_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm
          _ = ∏ b ∈ t, g b := by
           {refine Finset.prod_subset (Finset.filter_subset _ _) ?_
            intro b hbt hb
            simp only [Finset.mem_filter, and_iff_right hbt] at hb
            exact (h b).resolve_right hb}
      eq ▸ hs _ <| Finset.disjoint_of_subset_left (Finset.filter_subset _ _) ht⟩

Multipliability of Functions Equal to One or Original Function

Informal description

Let $\alpha$ be a topological group and $f, g : \beta \to \alpha$ be functions. If $f$ is multipliable and for every $b \in \beta$, $g(b)$ is either equal to $1$ or equal to $f(b)$, then $g$ is also multipliable.

Multipliable.mulIndicator theorem

(hf : Multipliable f) (s : Set β) : Multipliable (s.mulIndicator f)

Full source

@[to_additive]
protected theorem Multipliable.mulIndicator (hf : Multipliable f) (s : Set β) :
    Multipliable (s.mulIndicator f) :=
  hf.multipliable_of_eq_one_or_self <| Set.mulIndicator_eq_one_or_self _ _

Multipliability of Multiplicative Indicator Function

Informal description

Let $\alpha$ be a topological group and $f : \beta \to \alpha$ be a multipliable function. For any subset $s \subseteq \beta$, the multiplicative indicator function $\text{mulIndicator}_s f$ is also multipliable. Here, $\text{mulIndicator}_s f$ is defined as: \[ \text{mulIndicator}_s f (b) = \begin{cases} f(b) & \text{if } b \in s, \\ 1 & \text{otherwise.} \end{cases} \]

Multipliable.comp_injective theorem

{i : γ → β} (hf : Multipliable f) (hi : Injective i) : Multipliable (f ∘ i)

Full source

@[to_additive]
theorem Multipliable.comp_injective {i : γ → β} (hf : Multipliable f) (hi : Injective i) :
    Multipliable (f ∘ i) := by
  simpa only [Set.mulIndicator_range_comp] using
    (hi.multipliable_iff (fun x hx ↦ Set.mulIndicator_of_not_mem hx _)).2
    (hf.mulIndicator (Set.range i))

Multipliability under injective composition

Informal description

Let $\alpha$ be a topological group and $f : \beta \to \alpha$ be a multipliable function. If $i : \gamma \to \beta$ is an injective function, then the composition $f \circ i : \gamma \to \alpha$ is also multipliable.

Multipliable.subtype theorem

(hf : Multipliable f) (s : Set β) : Multipliable (f ∘ (↑) : s → α)

Full source

@[to_additive]
theorem Multipliable.subtype (hf : Multipliable f) (s : Set β) : Multipliable (f ∘ (↑) : s → α) :=
  hf.comp_injective Subtype.coe_injective

Multipliability of Restricted Function on Subset

Informal description

Let $\alpha$ be a topological group and $f : \beta \to \alpha$ be a multipliable function. For any subset $s \subseteq \beta$, the restriction of $f$ to $s$ (i.e., the composition $f \circ \iota$ where $\iota : s \hookrightarrow \beta$ is the inclusion map) is also multipliable.

multipliable_subtype_and_compl theorem

{s : Set β} : ((Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ f x) ↔ Multipliable f

Full source

@[to_additive]
theorem multipliable_subtype_and_compl {s : Set β} :
    ((Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ f x) ↔ Multipliable f :=
  ⟨and_imp.2 Multipliable.mul_compl, fun h ↦ ⟨h.subtype s, h.subtype sᶜ⟩⟩

Multipliability of a Function on a Set and its Complement is Equivalent to Global Multipliability

Informal description

For a function $f \colon \beta \to \alpha$ and a subset $s \subseteq \beta$, the function $f$ is multipliable if and only if both its restriction to $s$ and its restriction to the complement $s^\complement$ are multipliable. In other words, $f$ is multipliable if and only if both $f|_s$ and $f|_{s^\complement}$ are multipliable.

Multipliable.tprod_subtype_mul_tprod_subtype_compl theorem

 [T2Space α] {f : β → α} (hf : Multipliable f) (s : Set β) : (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x

Full source

@[to_additive]
protected theorem Multipliable.tprod_subtype_mul_tprod_subtype_compl [T2Space α] {f : β → α}
    (hf : Multipliable f) (s : Set β) : (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x :=
  ((hf.subtype s).hasProd.mul_compl (hf.subtype { x | x ∉ s }).hasProd).unique hf.hasProd

Product Decomposition over Subset and Complement: $\prod'_{s} f \cdot \prod'_{s^\complement} f = \prod' f$

Informal description

Let $\alpha$ be a Hausdorff topological group and $f : \beta \to \alpha$ a multipliable function. For any subset $s \subseteq \beta$, the product of $f$ over all elements in $\beta$ equals the product of $f$ over $s$ multiplied by the product of $f$ over the complement of $s$. In symbols: \[ \left(\prod'_{x \in s} f(x)\right) \cdot \left(\prod'_{x \in s^\complement} f(x)\right) = \prod'_{x \in \beta} f(x). \]

Multipliable.prod_mul_tprod_subtype_compl theorem

 [T2Space α] {f : β → α} (hf : Multipliable f) (s : Finset β) : (∏ x ∈ s, f x) * ∏' x : { x // x ∉ s }, f x = ∏' x, f x

Full source

@[to_additive]
protected theorem Multipliable.prod_mul_tprod_subtype_compl [T2Space α] {f : β → α}
    (hf : Multipliable f) (s : Finset β) :
    (∏ x ∈ s, f x) * ∏' x : { x // x ∉ s }, f x = ∏' x, f x := by
  rw [← hf.tprod_subtype_mul_tprod_subtype_compl s]
  simp only [Finset.tprod_subtype', mul_right_inj]
  rfl

Finite Product and Unconditional Product Decomposition: $\prod_s f \cdot \prod'_{s^\complement} f = \prod' f$

Informal description

Let $\alpha$ be a Hausdorff topological group and $f \colon \beta \to \alpha$ a multipliable function. For any finite subset $s \subseteq \beta$, the product of $f$ over all elements in $\beta$ equals the finite product of $f$ over $s$ multiplied by the unconditional product of $f$ over the complement of $s$. In symbols: \[ \left(\prod_{x \in s} f(x)\right) \cdot \left(\prod'_{x \notin s} f(x)\right) = \prod'_{x \in \beta} f(x). \]

Multipliable.vanishing theorem

 (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 (1 : G)) : ∃ s : Finset α, ∀ t, Disjoint t s → (∏ k ∈ t, f k) ∈ e

Full source

@[to_additive]
theorem Multipliable.vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 (1 : G)) :
    ∃ s : Finset α, ∀ t, Disjoint t s → (∏ k ∈ t, f k) ∈ e := by
  classical
  letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he

Vanishing Condition for Multipliable Functions in Topological Groups

Informal description

Let $G$ be a topological group and $f : \alpha \to G$ a multipliable function. For every neighborhood $e$ of the identity element $1 \in G$, there exists a finite subset $s \subseteq \alpha$ such that for any finite subset $t \subseteq \alpha$ disjoint from $s$, the product $\prod_{k \in t} f(k)$ belongs to $e$.

Multipliable.tprod_vanishing theorem

 (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 1) : ∃ s : Finset α, ∀ t : Set α, Disjoint t s → (∏' b : t, f b) ∈ e

Full source

@[to_additive]
theorem Multipliable.tprod_vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 1) :
    ∃ s : Finset α, ∀ t : Set α, Disjoint t s → (∏' b : t, f b) ∈ e := by
  classical
  letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he

Vanishing Condition for Unconditional Products of Multipliable Functions in Topological Groups

Informal description

Let $G$ be a topological group and $f : \alpha \to G$ a multipliable function. For every neighborhood $e$ of the identity element $1 \in G$, there exists a finite subset $s \subseteq \alpha$ such that for any subset $t \subseteq \alpha$ disjoint from $s$, the unconditional product $\prod'_{b \in t} f(b)$ belongs to $e$.

tendsto_tprod_compl_atTop_one theorem

(f : α → G) : Tendsto (fun s : Finset α ↦ ∏' a : { x // x ∉ s }, f a) atTop (𝓝 1)

Full source

/-- The product over the complement of a finset tends to `1` when the finset grows to cover the
whole space. This does not need a multipliability assumption, as otherwise all such products are
one. -/
@[to_additive "The sum over the complement of a finset tends to `0` when the finset grows to cover
the whole space. This does not need a summability assumption, as otherwise all such sums are zero."]
theorem tendsto_tprod_compl_atTop_one (f : α → G) :
    Tendsto (fun s : Finset α ↦ ∏' a : { x // x ∉ s }, f a) atTop (𝓝 1) := by
  classical
  by_cases H : Multipliable f
  · intro e he
    obtain ⟨s, hs⟩ := H.tprod_vanishing he
    rw [Filter.mem_map, mem_atTop_sets]
    exact ⟨s, fun t hts ↦ hs _ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
  · refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
    rwa [Finset.multipliable_compl_iff]

Convergence of Unconditional Product Over Complements to Identity in Topological Groups

Informal description

Let $G$ be a topological group and $f : \alpha \to G$ a function. The unconditional product of $f$ over the complement of any finite subset $s \subseteq \alpha$ tends to the identity element $1 \in G$ as $s$ grows to include all of $\alpha$. In other words, the net of products $\prod'_{a \notin s} f(a)$ converges to $1$ in the neighborhood filter of $1$ as $s$ becomes cofinite in $\alpha$.

Multipliable.tendsto_cofinite_one theorem

(hf : Multipliable f) : Tendsto f cofinite (𝓝 1)

Full source

/-- Product divergence test: if `f` is unconditionally multipliable, then `f x` tends to one along
`cofinite`. -/
@[to_additive "Series divergence test: if `f` is unconditionally summable, then `f x` tends to zero
along `cofinite`."]
theorem Multipliable.tendsto_cofinite_one (hf : Multipliable f) : Tendsto f cofinite (𝓝 1) := by
  intro e he
  rw [Filter.mem_map]
  rcases hf.vanishing he with ⟨s, hs⟩
  refine s.eventually_cofinite_nmem.mono fun x hx ↦ ?_
  · simpa using hs {x} (disjoint_singleton_left.2 hx)

Convergence to Identity Along Cofinite Filter for Multipliable Functions

Informal description

Let $G$ be a topological group and $f : \alpha \to G$ a multipliable function. Then $f(x)$ tends to the identity element $1 \in G$ along the cofinite filter on $\alpha$.

Multipliable.finite_mulSupport_of_discreteTopology theorem

 {α : Type*} [CommGroup α] [TopologicalSpace α] [DiscreteTopology α] {β : Type*} (f : β → α) (h : Multipliable f) :
  Set.Finite f.mulSupport

Full source

@[to_additive]
theorem Multipliable.finite_mulSupport_of_discreteTopology
    {α : Type*} [CommGroup α] [TopologicalSpace α] [DiscreteTopology α]
    {β : Type*} (f : β → α) (h : Multipliable f) : Set.Finite f.mulSupport :=
  haveI : IsTopologicalGroup α := ⟨⟩
  h.tendsto_cofinite_one (discreteTopology_iff_singleton_mem_nhds.mp ‹_› 1)

Finite Multiplicative Support of Multipliable Functions in Discrete Topological Groups

Informal description

Let $\alpha$ be a commutative group with a discrete topology, and let $f : \beta \to \alpha$ be a multipliable function. Then the multiplicative support of $f$, defined as $\{x \in \beta \mid f(x) \neq 1\}$, is finite.

Multipliable.countable_mulSupport theorem

[FirstCountableTopology G] [T1Space G] (hf : Multipliable f) : f.mulSupport.Countable

Full source

@[to_additive]
theorem Multipliable.countable_mulSupport [FirstCountableTopology G] [T1Space G]
    (hf : Multipliable f) : f.mulSupport.Countable := by
  simpa only [ker_nhds] using hf.tendsto_cofinite_one.countable_compl_preimage_ker

Countability of Multiplicative Support for Multipliable Functions in First-Countable T₁ Groups

Informal description

Let $G$ be a first-countable T₁ topological group and $f : \beta \to G$ a multipliable function. Then the multiplicative support of $f$, defined as $\{x \in \beta \mid f(x) \neq 1\}$, is countable.

multipliable_const_iff theorem

[Infinite β] [T2Space G] (a : G) : Multipliable (fun _ : β ↦ a) ↔ a = 1

Full source

@[to_additive]
theorem multipliable_const_iff [Infinite β] [T2Space G] (a : G) :
    MultipliableMultipliable (fun _ : β ↦ a) ↔ a = 1 := by
  refine ⟨fun h ↦ ?_, ?_⟩
  · by_contra ha
    have : {a}{a}ᶜ{a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)
    have : Finite β := by
      simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this
    exact not_finite β
  · rintro rfl
    exact multipliable_one

Multipliability of Constant Function in Hausdorff Groups: $f(b) = a$ is multipliable iff $a = 1$

Informal description

Let $G$ be a Hausdorff topological group and $\beta$ an infinite type. For any element $a \in G$, the constant function $f : \beta \to G$ defined by $f(b) = a$ for all $b \in \beta$ is multipliable if and only if $a = 1$.

tprod_const theorem

[T2Space G] (a : G) : ∏' _ : β, a = a ^ (Nat.card β)

Full source

@[to_additive (attr := simp)]
theorem tprod_const [T2Space G] (a : G) : ∏' _ : β, a = a ^ (Nat.card β) := by
  rcases finite_or_infinite β with hβ|hβ
  · letI : Fintype β := Fintype.ofFinite β
    rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]
    simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card]
  · simp only [Nat.card_eq_zero_of_infinite, pow_zero]
    rcases eq_or_ne a 1 with rfl|ha
    · simp
    · apply tprod_eq_one_of_not_multipliable
      simpa [multipliable_const_iff] using ha

Unconditional Product of Constant Function in Hausdorff Groups: $\prod'_{b} a = a^{\mathrm{card}(\beta)}$

Informal description

Let $G$ be a Hausdorff topological group and $\beta$ a type. For any element $a \in G$, the unconditional product of the constant function $f(b) = a$ over $\beta$ equals $a$ raised to the power of the cardinality of $\beta$ (where infinite cardinality is treated as zero), i.e., \[ \prod'_{b \in \beta} a = a^{\mathrm{Nat.card}(\beta)}. \]

HasProd.congr_cofinite₀ theorem

 {c : K} (hc : HasProd f c) {s : Finset α} (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) :
  HasProd g (c * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i))

Full source

lemma HasProd.congr_cofinite₀ {c : K} (hc : HasProd f c) {s : Finset α}
    (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) :
    HasProd g (c * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)) := by
  classical
  refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_
  filter_upwards [eventually_ge_atTop s] with t ht
  calc (∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
  _ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
  _ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i := by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs
  _ = ∏ i ∈ t, g i := by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

Product Convergence under Cofinite Modification in Groups with Zero

Informal description

Let $K$ be a topological group with zero, and let $f, g : \alpha \to K$ be functions. Suppose $f$ has product $c \in K$, and let $s$ be a finite subset of $\alpha$ such that $f(a) \neq 0$ for all $a \in s$. If $f(a) = g(a)$ for all $a \notin s$, then $g$ has product $c \cdot \left(\prod_{i \in s} g(i) / \prod_{i \in s} f(i)\right)$.

Multipliable.tsum_congr_cofinite₀ theorem

 [T2Space K] (hc : Multipliable f) {s : Finset α} (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) :
  ∏' i, g i = ((∏' i, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i))

Full source

protected lemma Multipliable.tsum_congr_cofinite₀ [T2Space K] (hc : Multipliable f) {s : Finset α}
    (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) :
    ∏' i, g i = ((∏' i, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)) :=
  (hc.hasProd.congr_cofinite₀ hs hs').tprod_eq

Unconditional Product under Cofinite Modification in Groups with Zero

Informal description

Let $K$ be a Hausdorff topological group with zero, and let $f, g : \alpha \to K$ be functions. Suppose $f$ is multipliable, and let $s$ be a finite subset of $\alpha$ such that $f(a) \neq 0$ for all $a \in s$. If $f(a) = g(a)$ for all $a \notin s$, then the unconditional product of $g$ satisfies \[ \prod'_{i} g(i) = \left(\prod'_{i} f(i)\right) \cdot \left(\frac{\prod_{i \in s} g(i)}{\prod_{i \in s} f(i)}\right). \]

Multipliable.congr_cofinite₀ theorem

(hf : Multipliable f) (hf' : ∀ a, f a ≠ 0) (hfg : ∀ᶠ a in cofinite, f a = g a) : Multipliable g

Full source

/--
See also `Multipliable.congr_cofinite`, which does not have a non-vanishing condition, but instead
requires the target to be a group under multiplication (and hence fails for infinite products in a
ring).
-/
lemma Multipliable.congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠ 0)
    (hfg : ∀ᶠ a in cofinite, f a = g a) :
    Multipliable g := by
  classical
  obtain ⟨c, hc⟩ := hf
  obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
  exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable

Multipliability under Cofinite Modification in Groups with Zero

Informal description

Let $K$ be a topological group with zero, and let $f, g : \alpha \to K$ be functions. If $f$ is multipliable, $f(a) \neq 0$ for all $a \in \alpha$, and $f(a) = g(a)$ for all but finitely many $a \in \alpha$, then $g$ is also multipliable.