Mathlib.Topology.Algebra.InfiniteSum.Basic

hasProd_one theorem

: HasProd (fun _ ↦ 1 : β → α) 1

Full source

/-- Constant one function has product `1` -/
@[to_additive "Constant zero function has sum `0`"]
theorem hasProd_one : HasProd (fun _ ↦ 1 : β → α) 1 := by simp [HasProd, tendsto_const_nhds]

Product of Constant One Function is One

Informal description

The constant function $f : \beta \to \alpha$ defined by $f(b) = 1$ for all $b \in \beta$ has product $1$ in the topological monoid $\alpha$. That is, $\prod_{b \in \beta} 1 = 1$.

hasProd_empty theorem

[IsEmpty β] : HasProd f 1

Full source

@[to_additive]
theorem hasProd_empty [IsEmpty β] : HasProd f 1 := by
  convert @hasProd_one α β _ _

Product over Empty Index Set is One

Informal description

For any function $f : \beta \to \alpha$ where $\beta$ is an empty type, the product $\prod_{b \in \beta} f(b)$ converges to $1$ in the topological monoid $\alpha$.

multipliable_one theorem

: Multipliable (fun _ ↦ 1 : β → α)

Full source

@[to_additive]
theorem multipliable_one : Multipliable (fun _ ↦ 1 : β → α) :=
  hasProd_one.multipliable

Multipliability of Constant One Function

Informal description

The constant function $f : \beta \to \alpha$ defined by $f(b) = 1$ for all $b \in \beta$ is multipliable in the topological monoid $\alpha$.

multipliable_empty theorem

[IsEmpty β] : Multipliable f

Full source

@[to_additive]
theorem multipliable_empty [IsEmpty β] : Multipliable f :=
  hasProd_empty.multipliable

Multipliability of Functions over Empty Index Sets

Informal description

For any function $f \colon \beta \to \alpha$ where $\beta$ is an empty type, $f$ is multipliable in the topological monoid $\alpha$.

multipliable_congr theorem

(hfg : ∀ b, f b = g b) : Multipliable f ↔ Multipliable g

Full source

/-- See `multipliable_congr_cofinite` for a version allowing the functions to
disagree on a finite set. -/
@[to_additive "See `summable_congr_cofinite` for a version allowing the functions to
disagree on a finite set."]
theorem multipliable_congr (hfg : ∀ b, f b = g b) : MultipliableMultipliable f ↔ Multipliable g :=
  iff_of_eq (congr_arg Multipliable <| funext hfg)

Multipliability is preserved under pointwise equality

Informal description

For functions $f, g : \beta \to \alpha$, if $f(b) = g(b)$ for all $b \in \beta$, then $f$ is multipliable if and only if $g$ is multipliable.

Multipliable.congr theorem

(hf : Multipliable f) (hfg : ∀ b, f b = g b) : Multipliable g

Full source

/-- See `Multipliable.congr_cofinite` for a version allowing the functions to
disagree on a finite set. -/
@[to_additive "See `Summable.congr_cofinite` for a version allowing the functions to
disagree on a finite set."]
theorem Multipliable.congr (hf : Multipliable f) (hfg : ∀ b, f b = g b) : Multipliable g :=
  (multipliable_congr hfg).mp hf

Multipliability Preserved Under Pointwise Equality

Informal description

If a function $f : \beta \to \alpha$ is multipliable and another function $g : \beta \to \alpha$ satisfies $f(b) = g(b)$ for all $b \in \beta$, then $g$ is also multipliable.

HasProd.congr_fun theorem

(hf : HasProd f a) (h : ∀ x : β, g x = f x) : HasProd g a

Full source

@[to_additive]
lemma HasProd.congr_fun (hf : HasProd f a) (h : ∀ x : β, g x = f x) : HasProd g a :=
  (funext h : g = f) ▸ hf

Product Convergence is Preserved by Pointwise Equality

Informal description

If a function $f : \beta \to \alpha$ has a product converging to $a$, and another function $g : \beta \to \alpha$ satisfies $g(x) = f(x)$ for all $x \in \beta$, then $g$ also has a product converging to $a$.

HasProd.hasProd_of_prod_eq theorem

 {g : γ → α} (h_eq : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b)
  (hf : HasProd g a) : HasProd f a

Full source

@[to_additive]
theorem HasProd.hasProd_of_prod_eq {g : γ → α}
    (h_eq : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' →
      ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b)
    (hf : HasProd g a) : HasProd f a :=
  le_trans (map_atTop_finset_prod_le_of_prod_eq h_eq) hf

Product Convergence Transfer via Finite Subset Correspondence

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions such that for every finite subset $u \subseteq \gamma$, there exists a finite subset $v \subseteq \beta$ with the property that for any finite superset $v' \supseteq v$, there exists a finite superset $u' \supseteq u$ satisfying $\prod_{x \in u'} g(x) = \prod_{b \in v'} f(b)$. If $g$ has a product converging to $a$, then $f$ also has a product converging to $a$.

hasProd_iff_hasProd theorem

 {g : γ → α} (h₁ : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b)
  (h₂ : ∀ v : Finset β, ∃ u : Finset γ, ∀ u', u ⊆ u' → ∃ v', v ⊆ v' ∧ ∏ b ∈ v', f b = ∏ x ∈ u', g x) :
  HasProd f a ↔ HasProd g a

Full source

@[to_additive]
theorem hasProd_iff_hasProd {g : γ → α}
    (h₁ : ∀ u : Finset γ, ∃ v : Finset β, ∀ v', v ⊆ v' →
      ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b)
    (h₂ : ∀ v : Finset β, ∃ u : Finset γ, ∀ u', u ⊆ u' →
      ∃ v', v ⊆ v' ∧ ∏ b ∈ v', f b = ∏ x ∈ u', g x) :
    HasProdHasProd f a ↔ HasProd g a :=
  ⟨HasProd.hasProd_of_prod_eq h₂, HasProd.hasProd_of_prod_eq h₁⟩

Equivalence of Product Convergence via Finite Subset Correspondence

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions such that: 1. For every finite subset $u \subseteq \gamma$, there exists a finite subset $v \subseteq \beta$ such that for any finite superset $v' \supseteq v$, there exists a finite superset $u' \supseteq u$ satisfying $\prod_{x \in u'} g(x) = \prod_{b \in v'} f(b)$. 2. For every finite subset $v \subseteq \beta$, there exists a finite subset $u \subseteq \gamma$ such that for any finite superset $u' \supseteq u$, there exists a finite superset $v' \supseteq v$ satisfying $\prod_{b \in v'} f(b) = \prod_{x \in u'} g(x)$. Then the product of $f$ converges to $a$ if and only if the product of $g$ converges to $a$.

Function.Injective.multipliable_iff theorem

{g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 1) : Multipliable (f ∘ g) ↔ Multipliable f

Full source

@[to_additive]
theorem Function.Injective.multipliable_iff {g : γ → β} (hg : Injective g)
    (hf : ∀ x ∉ Set.range g, f x = 1) : MultipliableMultipliable (f ∘ g) ↔ Multipliable f :=
  exists_congr fun _ ↦ hg.hasProd_iff hf

Injective Function Preserves Multipliability Condition

Informal description

Let $g : \gamma \to \beta$ be an injective function and $f : \beta \to \alpha$ a function such that $f(x) = 1$ for all $x \notin \text{range}(g)$. Then the composition $f \circ g$ is multipliable if and only if $f$ is multipliable.

hasProd_extend_one theorem

{g : β → γ} (hg : Injective g) : HasProd (extend g f 1) a ↔ HasProd f a

Full source

@[to_additive (attr := simp)] theorem hasProd_extend_one {g : β → γ} (hg : Injective g) :
    HasProdHasProd (extend g f 1) a ↔ HasProd f a := by
  rw [← hg.hasProd_iff, extend_comp hg]
  exact extend_apply' _ _

Product Convergence of Extended Function Equals Original Function's Convergence

Informal description

Let $g : \beta \to \gamma$ be an injective function. Then the extended function $\text{extend}\,g\,f\,1$ (which equals $f$ on the range of $g$ and $1$ elsewhere) has product converging to $a$ if and only if $f$ has product converging to $a$.

multipliable_extend_one theorem

{g : β → γ} (hg : Injective g) : Multipliable (extend g f 1) ↔ Multipliable f

Full source

@[to_additive (attr := simp)] theorem multipliable_extend_one {g : β → γ} (hg : Injective g) :
    MultipliableMultipliable (extend g f 1) ↔ Multipliable f :=
  exists_congr fun _ ↦ hasProd_extend_one hg

Multipliability of Extended Function via Injective Map

Informal description

Let $g : \beta \to \gamma$ be an injective function. The extended function $\text{extend}\,g\,f\,1$ (which equals $f$ on the range of $g$ and $1$ elsewhere) is multipliable if and only if $f$ is multipliable.

hasProd_subtype_iff_mulIndicator theorem

{s : Set β} : HasProd (f ∘ (↑) : s → α) a ↔ HasProd (s.mulIndicator f) a

Full source

@[to_additive]
theorem hasProd_subtype_iff_mulIndicator {s : Set β} :
    HasProdHasProd (f ∘ (↑) : s → α) a ↔ HasProd (s.mulIndicator f) a := by
  rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
    hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]

Product Convergence Equivalence for Restricted Function and Multiplicative Indicator

Informal description

For any set $s \subseteq \beta$ and function $f : \beta \to \alpha$, the product of the restriction $f|_s$ converges to $a$ if and only if the product of the multiplicative indicator function $\text{mulIndicator}_s f$ converges to $a$. Here, $\text{mulIndicator}_s f$ is defined as: \[ \text{mulIndicator}_s f (x) = \begin{cases} f(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \]

multipliable_subtype_iff_mulIndicator theorem

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

Full source

@[to_additive]
theorem multipliable_subtype_iff_mulIndicator {s : Set β} :
    MultipliableMultipliable (f ∘ (↑) : s → α) ↔ Multipliable (s.mulIndicator f) :=
  exists_congr fun _ ↦ hasProd_subtype_iff_mulIndicator

Multipliability Equivalence for Restricted Function and Multiplicative Indicator

Informal description

For any set $s \subseteq \beta$ and function $f : \beta \to \alpha$, the restriction $f|_s$ is multipliable if and only if the multiplicative indicator function $\text{mulIndicator}_s f$ is multipliable, where $\text{mulIndicator}_s f$ is defined as: \[ \text{mulIndicator}_s f (x) = \begin{cases} f(x) & \text{if } x \in s, \\ 1 & \text{otherwise.} \end{cases} \]

hasProd_subtype_mulSupport theorem

: HasProd (f ∘ (↑) : mulSupport f → α) a ↔ HasProd f a

Full source

@[to_additive (attr := simp)]
theorem hasProd_subtype_mulSupport : HasProdHasProd (f ∘ (↑) : mulSupport f → α) a ↔ HasProd f a :=
  hasProd_subtype_iff_of_mulSupport_subset <| Set.Subset.refl _

Product convergence equivalence for restriction to multiplicative support

Informal description

Let $f : \beta \to \alpha$ be a function with values in a topological monoid $\alpha$. Then the product of $f$ converges to $a$ if and only if the product of the restriction of $f$ to its multiplicative support $\{x \in \beta \mid f(x) \neq 1\}$ converges to $a$.

Finset.multipliable theorem

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

Full source

@[to_additive]
protected theorem Finset.multipliable (s : Finset β) (f : β → α) :
    Multipliable (f ∘ (↑) : (↑s : Set β) → α) :=
  (s.hasProd f).multipliable

Multipliability of Functions Restricted to Finite Sets

Informal description

For any finite subset $s \subseteq \beta$ and any function $f \colon \beta \to \alpha$ into a topological monoid $\alpha$, the restriction of $f$ to $s$ is multipliable. That is, the product $\prod_{b \in s} f(b)$ converges unconditionally in $\alpha$.

Set.Finite.multipliable theorem

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

Full source

@[to_additive]
protected theorem Set.Finite.multipliable {s : Set β} (hs : s.Finite) (f : β → α) :
    Multipliable (f ∘ (↑) : s → α) := by
  have := hs.toFinset.multipliable f
  rwa [hs.coe_toFinset] at this

Multipliability of Functions Restricted to Finite Sets

Informal description

For any finite set $s \subseteq \beta$ and any function $f \colon \beta \to \alpha$ into a topological monoid $\alpha$, the restriction of $f$ to $s$ is multipliable. That is, the product $\prod_{b \in s} f(b)$ converges unconditionally in $\alpha$.

multipliable_of_finite_mulSupport theorem

(h : (mulSupport f).Finite) : Multipliable f

Full source

@[to_additive]
theorem multipliable_of_finite_mulSupport (h : (mulSupport f).Finite) : Multipliable f := by
  apply multipliable_of_ne_finset_one (s := h.toFinset); simp

Multipliability of functions with finite multiplicative support

Informal description

Let $f : \beta \to \alpha$ be a function into a topological monoid $\alpha$. If the multiplicative support of $f$, defined as $\{b \in \beta \mid f(b) \neq 1\}$, is finite, then $f$ is multipliable.

Multipliable.of_finite theorem

[Finite β] {f : β → α} : Multipliable f

Full source

@[to_additive]
lemma Multipliable.of_finite [Finite β] {f : β → α} : Multipliable f :=
  multipliable_of_finite_mulSupport <| Set.finite_univ.subset (Set.subset_univ _)

Multipliability of Functions on Finite Types

Informal description

For any finite type $\beta$ and any function $f \colon \beta \to \alpha$ into a topological monoid $\alpha$, the function $f$ is multipliable. That is, the product $\prod_{b \in \beta} f(b)$ converges unconditionally in $\alpha$.

hasProd_single theorem

{f : β → α} (b : β) (hf : ∀ (b') (_ : b' ≠ b), f b' = 1) : HasProd f (f b)

Full source

@[to_additive]
theorem hasProd_single {f : β → α} (b : β) (hf : ∀ (b') (_ : b' ≠ b), f b' = 1) : HasProd f (f b) :=
  suffices HasProd f (∏ b' ∈ {b}, f b') by simpa using this
  hasProd_prod_of_ne_finset_one <| by simpa [hf]

Product of a Function with Singleton Support: $\prod f = f(b)$ when $f(b')=1$ for $b' \neq b$

Informal description

Let $f : \beta \to \alpha$ be a function such that $f(b') = 1$ for all $b' \neq b$. Then the product of $f$ converges unconditionally to $f(b)$.

hasProd_unique theorem

[Unique β] (f : β → α) : HasProd f (f default)

Full source

@[to_additive (attr := simp)] lemma hasProd_unique [Unique β] (f : β → α) : HasProd f (f default) :=
  hasProd_single default (fun _ hb ↦ False.elim <| hb <| Unique.uniq ..)

Product of a Function over a Unique Type: $\prod f = f(\text{default})$

Informal description

For any function $f : \beta \to \alpha$ where $\beta$ is a type with a unique element (denoted `default`), the product of $f$ converges unconditionally to $f(\text{default})$.

hasProd_singleton theorem

(m : β) (f : β → α) : HasProd (({ m } : Set β).restrict f) (f m)

Full source

@[to_additive (attr := simp)]
lemma hasProd_singleton (m : β) (f : β → α) : HasProd (({m} : Set β).restrict f) (f m) :=
  hasProd_unique (Set.restrict {m} f)

Product over Singleton Set: $\prod_{x \in \{m\}} f(x) = f(m)$

Informal description

For any element $m$ in a type $\beta$ and any function $f : \beta \to \alpha$, the restriction of $f$ to the singleton set $\{m\}$ has an unconditional product converging to $f(m)$. In other words, $\prod_{x \in \{m\}} f(x) = f(m)$.

hasProd_ite_eq theorem

(b : β) [DecidablePred (· = b)] (a : α) : HasProd (fun b' ↦ if b' = b then a else 1) a

Full source

@[to_additive]
theorem hasProd_ite_eq (b : β) [DecidablePred (· = b)] (a : α) :
    HasProd (fun b' ↦ if b' = b then a else 1) a := by
  convert @hasProd_single _ _ _ _ (fun b' ↦ if b' = b then a else 1) b (fun b' hb' ↦ if_neg hb')
  exact (if_pos rfl).symm

Product of Indicator Function at a Point: $\prod_{b'} (\text{if } b' = b \text{ then } a \text{ else } 1) = a$

Informal description

For any element $b$ in a type $\beta$ with a decidable equality predicate, and any element $a$ in a topological monoid $\alpha$, the function $f : \beta \to \alpha$ defined by $f(b') = a$ if $b' = b$ and $f(b') = 1$ otherwise has an unconditional product converging to $a$. In other words, $\prod_{b'} f(b') = a$ where $f$ is non-trivial only at $b' = b$.

Equiv.hasProd_iff theorem

(e : γ ≃ β) : HasProd (f ∘ e) a ↔ HasProd f a

Full source

@[to_additive]
theorem Equiv.hasProd_iff (e : γ ≃ β) : HasProdHasProd (f ∘ e) a ↔ HasProd f a :=
  e.injective.hasProd_iff <| by simp

Product Convergence Under Equivalence: $\text{HasProd}(f \circ e, a) \leftrightarrow \text{HasProd}(f, a)$

Informal description

Let $e : \gamma \simeq \beta$ be an equivalence (bijection with inverse) between types $\gamma$ and $\beta$, and let $f : \beta \to \alpha$ be a function. The product of $f \circ e$ converges to $a$ if and only if the product of $f$ converges to $a$.

Function.Injective.hasProd_range_iff theorem

{g : γ → β} (hg : Injective g) : HasProd (fun x : Set.range g ↦ f x) a ↔ HasProd (f ∘ g) a

Full source

@[to_additive]
theorem Function.Injective.hasProd_range_iff {g : γ → β} (hg : Injective g) :
    HasProdHasProd (fun x : Set.range g ↦ f x) a ↔ HasProd (f ∘ g) a :=
  (Equiv.ofInjective g hg).hasProd_iff.symm

Product Convergence over Range of Injective Function: $\text{HasProd}(f|_{\text{range}(g)}, a) \leftrightarrow \text{HasProd}(f \circ g, a)$

Informal description

Let $g : \gamma \to \beta$ be an injective function. The product of $f$ over the range of $g$ converges to $a$ if and only if the product of $f \circ g$ converges to $a$.

Equiv.multipliable_iff theorem

(e : γ ≃ β) : Multipliable (f ∘ e) ↔ Multipliable f

Full source

@[to_additive]
theorem Equiv.multipliable_iff (e : γ ≃ β) : MultipliableMultipliable (f ∘ e) ↔ Multipliable f :=
  exists_congr fun _ ↦ e.hasProd_iff

Multipliability Under Equivalence: $\text{Multipliable}(f \circ e) \leftrightarrow \text{Multipliable}(f)$

Informal description

Let $e : \gamma \simeq \beta$ be an equivalence (bijection with inverse) between types $\gamma$ and $\beta$, and let $f : \beta \to \alpha$ be a function. The function $f \circ e$ is multipliable if and only if $f$ is multipliable.

Equiv.hasProd_iff_of_mulSupport theorem

 {g : γ → α} (e : mulSupport f ≃ mulSupport g) (he : ∀ x : mulSupport f, g (e x) = f x) : HasProd f a ↔ HasProd g a

Full source

@[to_additive]
theorem Equiv.hasProd_iff_of_mulSupport {g : γ → α} (e : mulSupportmulSupport f ≃ mulSupport g)
    (he : ∀ x : mulSupport f, g (e x) = f x) : HasProdHasProd f a ↔ HasProd g a := by
  have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he
  rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]

Product Convergence Equivalence Under Multiplicative Support Bijection: $\text{HasProd}(f, a) \leftrightarrow \text{HasProd}(g, a)$

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions with values in a topological monoid $\alpha$, and let $e : \text{mulSupport}\, f \simeq \text{mulSupport}\, g$ be an equivalence between their multiplicative supports. If for every $x$ in the multiplicative support of $f$, we have $g(e(x)) = f(x)$, then the product of $f$ converges to $a$ if and only if the product of $g$ converges to $a$.

hasProd_iff_hasProd_of_ne_one_bij theorem

 {g : γ → α} (i : mulSupport g → β) (hi : Injective i) (hf : mulSupport f ⊆ Set.range i) (hfg : ∀ x, f (i x) = g x) :
  HasProd f a ↔ HasProd g a

Full source

@[to_additive]
theorem hasProd_iff_hasProd_of_ne_one_bij {g : γ → α} (i : mulSupport g → β)
    (hi : Injective i) (hf : mulSupportmulSupport f ⊆ Set.range i)
    (hfg : ∀ x, f (i x) = g x) : HasProdHasProd f a ↔ HasProd g a :=
  Iff.symm <|
    Equiv.hasProd_iff_of_mulSupport
      (Equiv.ofBijective (fun x ↦ ⟨i x, fun hx ↦ x.coe_prop <| hfg x ▸ hx⟩)
        ⟨fun _ _ h ↦ hi <| Subtype.ext_iff.1 h, fun y ↦
          (hf y.coe_prop).imp fun _ hx ↦ Subtype.ext hx⟩)
      hfg

Product Convergence Equivalence Under Bijection on Multiplicative Support: $\text{HasProd}(f, a) \leftrightarrow \text{HasProd}(g, a)$

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions with values in a topological monoid $\alpha$. Suppose there exists an injective function $i : \text{mulSupport}\, g \to \beta$ such that the multiplicative support of $f$ is contained in the range of $i$, and for all $x$ in the multiplicative support of $g$, we have $f(i(x)) = g(x)$. Then the product of $f$ converges to $a$ if and only if the product of $g$ converges to $a$.

Equiv.multipliable_iff_of_mulSupport theorem

 {g : γ → α} (e : mulSupport f ≃ mulSupport g) (he : ∀ x : mulSupport f, g (e x) = f x) :
  Multipliable f ↔ Multipliable g

Full source

@[to_additive]
theorem Equiv.multipliable_iff_of_mulSupport {g : γ → α} (e : mulSupportmulSupport f ≃ mulSupport g)
    (he : ∀ x : mulSupport f, g (e x) = f x) : MultipliableMultipliable f ↔ Multipliable g :=
  exists_congr fun _ ↦ e.hasProd_iff_of_mulSupport he

Multipliability Equivalence Under Multiplicative Support Bijection: $\text{Multipliable}(f) \leftrightarrow \text{Multipliable}(g)$

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions with values in a topological monoid $\alpha$, and let $e : \text{mulSupport}\, f \simeq \text{mulSupport}\, g$ be an equivalence between their multiplicative supports. If for every $x$ in the multiplicative support of $f$, we have $g(e(x)) = f(x)$, then the product of $f$ is multipliable if and only if the product of $g$ is multipliable.

HasProd.map theorem

 [CommMonoid γ] [TopologicalSpace γ] (hf : HasProd f a) {G} [FunLike G α γ] [MonoidHomClass G α γ] (g : G)
  (hg : Continuous g) : HasProd (g ∘ f) (g a)

Full source

@[to_additive]
protected theorem HasProd.map [CommMonoid γ] [TopologicalSpace γ] (hf : HasProd f a) {G}
    [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous g) :
    HasProd (g ∘ f) (g a) := by
  have : (g ∘ fun s : Finset β ↦ ∏ b ∈ s, f b) = fun s : Finset β ↦ ∏ b ∈ s, (g ∘ f) b :=
    funext <| map_prod g _
  unfold HasProd
  rw [← this]
  exact (hg.tendsto a).comp hf

Continuous Monoid Homomorphism Preserves Product Convergence

Informal description

Let $\alpha$ and $\gamma$ be commutative monoids with topological structures, and let $f \colon \beta \to \alpha$ be a function such that the product of $f$ converges to $a \in \alpha$. Let $G$ be a type of homomorphisms from $\alpha$ to $\gamma$ that preserve the monoid structure, and let $g \colon G$ be a continuous homomorphism. Then the product of $g \circ f$ converges to $g(a)$.

Topology.IsInducing.hasProd_iff theorem

 [CommMonoid γ] [TopologicalSpace γ] {G} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α)
  (a : α) : HasProd (g ∘ f) (g a) ↔ HasProd f a

Full source

@[to_additive]
protected theorem Topology.IsInducing.hasProd_iff [CommMonoid γ] [TopologicalSpace γ] {G}
    [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α) (a : α) :
    HasProdHasProd (g ∘ f) (g a) ↔ HasProd f a := by
  simp_rw [HasProd, comp_apply, ← map_prod]
  exact hg.tendsto_nhds_iff.symm

Inducing Homomorphism Preserves Product Convergence: $g \circ f$ converges to $g(a)$ iff $f$ converges to $a$

Informal description

Let $\alpha$ and $\gamma$ be commutative monoids with topological structures, and let $G$ be a type of homomorphisms from $\alpha$ to $\gamma$ that preserve the monoid structure. Given an inducing homomorphism $g \colon G$ and a function $f \colon \beta \to \alpha$, the product of $g \circ f$ converges to $g(a)$ if and only if the product of $f$ converges to $a$.

Multipliable.map theorem

 [CommMonoid γ] [TopologicalSpace γ] (hf : Multipliable f) {G} [FunLike G α γ] [MonoidHomClass G α γ] (g : G)
  (hg : Continuous g) : Multipliable (g ∘ f)

Full source

@[to_additive]
protected theorem Multipliable.map [CommMonoid γ] [TopologicalSpace γ] (hf : Multipliable f) {G}
    [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous g) : Multipliable (g ∘ f) :=
  (hf.hasProd.map g hg).multipliable

Continuous Monoid Homomorphism Preserves Multipliability

Informal description

Let $\alpha$ and $\gamma$ be commutative topological monoids, and let $f \colon \beta \to \alpha$ be a multipliable function. If $g \colon \alpha \to \gamma$ is a continuous monoid homomorphism, then the composition $g \circ f \colon \beta \to \gamma$ is also multipliable.

Multipliable.map_iff_of_leftInverse theorem

 [CommMonoid γ] [TopologicalSpace γ] {G G'} [FunLike G α γ] [MonoidHomClass G α γ] [FunLike G' γ α]
  [MonoidHomClass G' γ α] (g : G) (g' : G') (hg : Continuous g) (hg' : Continuous g')
  (hinv : Function.LeftInverse g' g) : Multipliable (g ∘ f) ↔ Multipliable f

Full source

@[to_additive]
protected theorem Multipliable.map_iff_of_leftInverse [CommMonoid γ] [TopologicalSpace γ] {G G'}
    [FunLike G α γ] [MonoidHomClass G α γ] [FunLike G' γ α] [MonoidHomClass G' γ α]
    (g : G) (g' : G') (hg : Continuous g) (hg' : Continuous g') (hinv : Function.LeftInverse g' g) :
    MultipliableMultipliable (g ∘ f) ↔ Multipliable f :=
  ⟨fun h ↦ by
    have := h.map _ hg'
    rwa [← Function.comp_assoc, hinv.id] at this, fun h ↦ h.map _ hg⟩

Multipliability under Continuous Monoid Homomorphism with Left Inverse: $g \circ f$ multipliable iff $f$ multipliable

Informal description

Let $\alpha$ and $\gamma$ be commutative topological monoids, and let $G$ and $G'$ be types of monoid homomorphisms from $\alpha$ to $\gamma$ and from $\gamma$ to $\alpha$, respectively. Given continuous homomorphisms $g \colon G$ and $g' \colon G'$ such that $g'$ is a left inverse of $g$, the composition $g \circ f \colon \beta \to \gamma$ is multipliable if and only if $f \colon \beta \to \alpha$ is multipliable.

Multipliable.map_tprod theorem

 [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] (hf : Multipliable f) {G} [FunLike G α γ] [MonoidHomClass G α γ]
  (g : G) (hg : Continuous g) : g (∏' i, f i) = ∏' i, g (f i)

Full source

@[to_additive]
theorem Multipliable.map_tprod [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] (hf : Multipliable f)
    {G} [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous g) :
    g (∏' i, f i) = ∏' i, g (f i) := (HasProd.tprod_eq (HasProd.map hf.hasProd g hg)).symm

Continuous Homomorphism Commutes with Unconditional Product: $g(\prod' f) = \prod' (g \circ f)$

Informal description

Let $\alpha$ and $\gamma$ be commutative topological monoids with $\gamma$ Hausdorff, and let $f \colon \beta \to \alpha$ be a multipliable function. If $g \colon \alpha \to \gamma$ is a continuous monoid homomorphism, then $g$ applied to the unconditional product $\prod'_{i} f(i)$ equals the unconditional product $\prod'_{i} g(f(i))$.

Topology.IsInducing.multipliable_iff_tprod_comp_mem_range theorem

 [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] {G} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g)
  (f : β → α) : Multipliable f ↔ Multipliable (g ∘ f) ∧ ∏' i, g (f i) ∈ Set.range g

Full source

@[to_additive]
lemma Topology.IsInducing.multipliable_iff_tprod_comp_mem_range [CommMonoid γ] [TopologicalSpace γ]
    [T2Space γ] {G} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α) :
    MultipliableMultipliable f ↔ Multipliable (g ∘ f) ∧ ∏' i, g (f i) ∈ Set.range g := by
  constructor
  · intro hf
    constructor
    · exact hf.map g hg.continuous
    · use ∏' i, f i
      exact hf.map_tprod g hg.continuous
  · rintro ⟨hgf, a, ha⟩
    use a
    have := hgf.hasProd
    simp_rw [comp_apply, ← ha] at this
    exact (hg.hasProd_iff f a).mp this

Multipliability Criterion via Inducing Homomorphism: $f$ multipliable iff $g \circ f$ multipliable with product in range of $g$

Informal description

Let $\alpha$ and $\gamma$ be commutative topological monoids with $\gamma$ Hausdorff, and let $G$ be a type of monoid homomorphisms from $\alpha$ to $\gamma$. Given an inducing homomorphism $g \colon G$ and a function $f \colon \beta \to \alpha$, the following are equivalent: 1. $f$ is multipliable. 2. The composition $g \circ f$ is multipliable and the unconditional product $\prod'_{i} g(f(i))$ lies in the range of $g$.

Multipliable.map_iff_of_equiv theorem

 [CommMonoid γ] [TopologicalSpace γ] {G} [EquivLike G α γ] [MulEquivClass G α γ] (g : G) (hg : Continuous g)
  (hg' : Continuous (EquivLike.inv g : γ → α)) : Multipliable (g ∘ f) ↔ Multipliable f

Full source

/-- "A special case of `Multipliable.map_iff_of_leftInverse` for convenience" -/
@[to_additive "A special case of `Summable.map_iff_of_leftInverse` for convenience"]
protected theorem Multipliable.map_iff_of_equiv [CommMonoid γ] [TopologicalSpace γ] {G}
    [EquivLike G α γ] [MulEquivClass G α γ] (g : G) (hg : Continuous g)
    (hg' : Continuous (EquivLike.inv g : γ → α)) : MultipliableMultipliable (g ∘ f) ↔ Multipliable f :=
  Multipliable.map_iff_of_leftInverse g (g : α ≃* γ).symm hg hg' (EquivLike.left_inv g)

Multipliability under Continuous Multiplicative Equivalence: $g \circ f$ multipliable iff $f$ multipliable

Informal description

Let $\alpha$ and $\gamma$ be commutative topological monoids, and let $G$ be a type of multiplicative equivalences between $\alpha$ and $\gamma$. Given a continuous multiplicative equivalence $g \colon G$ whose inverse is also continuous, the composition $g \circ f \colon \beta \to \gamma$ is multipliable if and only if $f \colon \beta \to \alpha$ is multipliable.

Function.Surjective.multipliable_iff_of_hasProd_iff theorem

 {α' : Type*} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) {f : β → α} {g : γ → α'}
  (he : ∀ {a}, HasProd f (e a) ↔ HasProd g a) : Multipliable f ↔ Multipliable g

Full source

@[to_additive]
theorem Function.Surjective.multipliable_iff_of_hasProd_iff {α' : Type*} [CommMonoid α']
    [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) {f : β → α} {g : γ → α'}
    (he : ∀ {a}, HasProdHasProd f (e a) ↔ HasProd g a) : MultipliableMultipliable f ↔ Multipliable g :=
  hes.exists.trans <| exists_congr <| @he

Multipliability under Surjective Mapping with Product Convergence Equivalence

Informal description

Let $\alpha'$ be a type with a commutative monoid structure and a topological space structure, and let $e : \alpha' \to \alpha$ be a surjective function. Given functions $f : \beta \to \alpha$ and $g : \gamma \to \alpha'$, suppose that for any $a \in \alpha'$, the product of $f$ converges to $e(a)$ if and only if the product of $g$ converges to $a$. Then $f$ is multipliable if and only if $g$ is multipliable.

HasProd.mul theorem

(hf : HasProd f a) (hg : HasProd g b) : HasProd (fun b ↦ f b * g b) (a * b)

Full source

@[to_additive]
theorem HasProd.mul (hf : HasProd f a) (hg : HasProd g b) :
    HasProd (fun b ↦ f b * g b) (a * b) := by
  dsimp only [HasProd] at hf hg ⊢
  simp_rw [prod_mul_distrib]
  exact hf.mul hg

Product of convergent products is $a \cdot b$

Informal description

If $f$ has product $a$ and $g$ has product $b$, then the pointwise product function $\lambda b, f(b) \cdot g(b)$ has product $a \cdot b$.

Multipliable.mul theorem

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

Full source

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

Multipliability of Pointwise Product of Multipliable Functions

Informal description

If two functions $f, g : \beta \to \alpha$ are multipliable in a commutative topological monoid $\alpha$, then their pointwise product $\lambda b, f(b) \cdot g(b)$ is also multipliable.

hasProd_prod theorem

 {f : γ → β → α} {a : γ → α} {s : Finset γ} :
  (∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i)

Full source

@[to_additive]
theorem hasProd_prod {f : γ → β → α} {a : γ → α} {s : Finset γ} :
    (∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) := by
  classical
  exact Finset.induction_on s (by simp only [hasProd_one, prod_empty, forall_true_iff]) <| by
    simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
      prod_insert, and_imp]
    exact fun x s _ IH hx h ↦ hx.mul (IH h)

Product of convergent products over a finite index set

Informal description

Let $f : \gamma \to \beta \to \alpha$ be a family of functions and $a : \gamma \to \alpha$ be a family of values. For any finite set $s \subseteq \gamma$, if for every $i \in s$ the function $f(i)$ has product $a(i)$, then the pointwise product function $\lambda b, \prod_{i \in s} f(i)(b)$ has product $\prod_{i \in s} a(i)$.

multipliable_prod theorem

 {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i)) : Multipliable fun b ↦ ∏ i ∈ s, f i b

Full source

@[to_additive]
theorem multipliable_prod {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i)) :
    Multipliable fun b ↦ ∏ i ∈ s, f i b :=
  (hasProd_prod fun i hi ↦ (hf i hi).hasProd).multipliable

Multipliability of Finite Pointwise Products

Informal description

Let $f : \gamma \to \beta \to \alpha$ be a family of functions and $s$ be a finite subset of $\gamma$. If for every $i \in s$, the function $f(i)$ is multipliable, then the pointwise product function $\lambda b, \prod_{i \in s} f(i)(b)$ is multipliable.

HasProd.mul_disjoint theorem

 {s t : Set β} (hs : Disjoint s t) (ha : HasProd (f ∘ (↑) : s → α) a) (hb : HasProd (f ∘ (↑) : t → α) b) :
  HasProd (f ∘ (↑) : (s ∪ t : Set β) → α) (a * b)

Full source

@[to_additive]
theorem HasProd.mul_disjoint {s t : Set β} (hs : Disjoint s t) (ha : HasProd (f ∘ (↑) : s → α) a)
    (hb : HasProd (f ∘ (↑) : t → α) b) : HasProd (f ∘ (↑) : (s ∪ t : Set β) → α) (a * b) := by
  rw [hasProd_subtype_iff_mulIndicator] at *
  rw [Set.mulIndicator_union_of_disjoint hs]
  exact ha.mul hb

Product of Disjoint Restrictions: $\text{HasProd}(f|_{s \cup t}) = \text{HasProd}(f|_s) \cdot \text{HasProd}(f|_t)$

Informal description

Let $s$ and $t$ be disjoint subsets of $\beta$, and let $f : \beta \to \alpha$ be a function. If the restriction of $f$ to $s$ has product $a$ and the restriction of $f$ to $t$ has product $b$, then the restriction of $f$ to $s \cup t$ has product $a \cdot b$.

hasProd_prod_disjoint theorem

 {ι} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : (s : Set ι).Pairwise (Disjoint on t))
  (hf : ∀ i ∈ s, HasProd (f ∘ (↑) : t i → α) (a i)) : HasProd (f ∘ (↑) : (⋃ i ∈ s, t i) → α) (∏ i ∈ s, a i)

Full source

@[to_additive]
theorem hasProd_prod_disjoint {ι} (s : Finset ι) {t : ι → Set β} {a : ι → α}
    (hs : (s : Set ι).Pairwise (DisjointDisjoint on t)) (hf : ∀ i ∈ s, HasProd (f ∘ (↑) : t i → α) (a i)) :
    HasProd (f ∘ (↑) : (⋃ i ∈ s, t i) → α) (∏ i ∈ s, a i) := by
  simp_rw [hasProd_subtype_iff_mulIndicator] at *
  rw [Finset.mulIndicator_biUnion _ _ hs]
  exact hasProd_prod hf

Product over a Union of Pairwise Disjoint Sets

Informal description

Let $\{t_i\}_{i \in \iota}$ be a family of pairwise disjoint subsets of $\beta$, and let $s$ be a finite subset of $\iota$. For each $i \in s$, suppose the restriction of $f$ to $t_i$ has product $a_i$. Then the restriction of $f$ to the union $\bigcup_{i \in s} t_i$ has product $\prod_{i \in s} a_i$.

HasProd.mul_isCompl theorem

 {s t : Set β} (hs : IsCompl s t) (ha : HasProd (f ∘ (↑) : s → α) a) (hb : HasProd (f ∘ (↑) : t → α) b) :
  HasProd f (a * b)

Full source

@[to_additive]
theorem HasProd.mul_isCompl {s t : Set β} (hs : IsCompl s t) (ha : HasProd (f ∘ (↑) : s → α) a)
    (hb : HasProd (f ∘ (↑) : t → α) b) : HasProd f (a * b) := by
  simpa [← hs.compl_eq] using
    (hasProd_subtype_iff_mulIndicator.1 ha).mul (hasProd_subtype_iff_mulIndicator.1 hb)

Product over Complementary Subsets: $a \cdot b$ for Complementary $s$ and $t$

Informal description

Let $s$ and $t$ be complementary subsets of $\beta$ (i.e., $s \sqcup t = \top$ and $s \sqcap t = \bot$ in the Boolean algebra of subsets). If the restriction of $f$ to $s$ has product $a$ and the restriction of $f$ to $t$ has product $b$, then the product of $f$ over all of $\beta$ exists and equals $a \cdot b$.

HasProd.mul_compl theorem

 {s : Set β} (ha : HasProd (f ∘ (↑) : s → α) a) (hb : HasProd (f ∘ (↑) : (sᶜ : Set β) → α) b) : HasProd f (a * b)

Full source

@[to_additive]
theorem HasProd.mul_compl {s : Set β} (ha : HasProd (f ∘ (↑) : s → α) a)
    (hb : HasProd (f ∘ (↑) : (sᶜ : Set β) → α) b) : HasProd f (a * b) :=
  ha.mul_isCompl isCompl_compl hb

Product Decomposition over Complementary Subsets: $a \cdot b$ 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$ and the restriction of $f$ to the complement $s^\complement$ has product $b$, then the product of $f$ over all of $\beta$ exists and equals $a \cdot b$.

Multipliable.mul_compl theorem

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

Full source

@[to_additive]
theorem Multipliable.mul_compl {s : Set β} (hs : Multipliable (f ∘ (↑) : s → α))
    (hsc : Multipliable (f ∘ (↑) : (sᶜ : Set β) → α)) : Multipliable f :=
  (hs.hasProd.mul_compl hsc.hasProd).multipliable

Multipliability of a Function on a Set and its Complement Implies Global Multipliability

Informal description

Let $f \colon \beta \to \alpha$ be a function and $s \subseteq \beta$ a subset. If the restriction of $f$ to $s$ is multipliable and the restriction of $f$ to the complement $s^\complement$ is multipliable, then $f$ is multipliable.

HasProd.compl_mul theorem

 {s : Set β} (ha : HasProd (f ∘ (↑) : (sᶜ : Set β) → α) a) (hb : HasProd (f ∘ (↑) : s → α) b) : HasProd f (a * b)

Full source

@[to_additive]
theorem HasProd.compl_mul {s : Set β} (ha : HasProd (f ∘ (↑) : (sᶜ : Set β) → α) a)
    (hb : HasProd (f ∘ (↑) : s → α) b) : HasProd f (a * b) :=
  ha.mul_isCompl isCompl_compl.symm hb

Product over a Set and its Complement: $a \cdot b$ for $s^\complement$ and $s$

Informal description

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

Multipliable.compl_add theorem

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

Full source

@[to_additive]
theorem Multipliable.compl_add {s : Set β} (hs : Multipliable (f ∘ (↑) : (sᶜ : Set β) → α))
    (hsc : Multipliable (f ∘ (↑) : s → α)) : Multipliable f :=
  (hs.hasProd.compl_mul hsc.hasProd).multipliable

Multipliability of a Function via Multipliability on a Set and its Complement

Informal description

Let $s$ be a subset of $\beta$ and $f : \beta \to \alpha$ be a function. If the restrictions of $f$ to both the complement $s^\complement$ and $s$ are multipliable, then $f$ is multipliable.

HasProd.update' theorem

 {α β : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α] [ContinuousMul α] [DecidableEq β] {f : β → α} {a a' : α}
  (hf : HasProd f a) (b : β) (x : α) (hf' : HasProd (update f b x) a') : a * x = a' * f b

Full source

/-- Version of `HasProd.update` for `CommMonoid` rather than `CommGroup`.
Rather than showing that `f.update` has a specific product in terms of `HasProd`,
it gives a relationship between the products of `f` and `f.update` given that both exist. -/
@[to_additive "Version of `HasSum.update` for `AddCommMonoid` rather than `AddCommGroup`.
Rather than showing that `f.update` has a specific sum in terms of `HasSum`,
it gives a relationship between the sums of `f` and `f.update` given that both exist."]
theorem HasProd.update' {α β : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α]
    [ContinuousMul α] [DecidableEq β] {f : β → α} {a a' : α} (hf : HasProd f a) (b : β) (x : α)
    (hf' : HasProd (update f b x) a') : a * x = a' * f b := by
  have : ∀ b', f b' * ite (b' = b) x 1 = update f b x b' * ite (b' = b) (f b) 1 := by
    intro b'
    split_ifs with hb'
    · simpa only [Function.update_apply, hb', eq_self_iff_true] using mul_comm (f b) x
    · simp only [Function.update_apply, hb', if_false]
  have h := hf.mul (hasProd_ite_eq b x)
  simp_rw [this] at h
  exact HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b)))

Product Relation for Updated Function: $a \cdot x = a' \cdot f(b)$

Informal description

Let $\alpha$ be a topological commutative monoid that is Hausdorff and has continuous multiplication, and let $\beta$ be a type with decidable equality. Given a function $f : \beta \to \alpha$ with product $a$, and an element $b \in \beta$, if the updated function $\text{update } f \, b \, x$ has product $a'$, then the following equality holds: \[ a \cdot x = a' \cdot f(b). \]

tprod_congr_set_coe theorem

(f : β → α) {s t : Set β} (h : s = t) : ∏' x : s, f x = ∏' x : t, f x

Full source

@[to_additive]
theorem tprod_congr_set_coe (f : β → α) {s t : Set β} (h : s = t) :
    ∏' x : s, f x = ∏' x : t, f x := by rw [h]

Unconditional Product Equality for Equal Subsets

Informal description

Let $f : \beta \to \alpha$ be a function and $s, t \subseteq \beta$ be subsets with $s = t$. Then the unconditional product of $f$ over the elements of $s$ equals the unconditional product of $f$ over the elements of $t$, i.e., \[ \prod'_{x \in s} f(x) = \prod'_{x \in t} f(x). \]

tprod_congr_subtype theorem

(f : β → α) {P Q : β → Prop} (h : ∀ x, P x ↔ Q x) : ∏' x : { x // P x }, f x = ∏' x : { x // Q x }, f x

Full source

@[to_additive]
theorem tprod_congr_subtype (f : β → α) {P Q : β → Prop} (h : ∀ x, P x ↔ Q x) :
    ∏' x : {x // P x}, f x = ∏' x : {x // Q x}, f x :=
  tprod_congr_set_coe f <| Set.ext h

Unconditional Product Equality for Equivalent Predicates

Informal description

Let $f : \beta \to \alpha$ be a function and $P, Q : \beta \to \text{Prop}$ be predicates such that for all $x \in \beta$, $P(x) \leftrightarrow Q(x)$. Then the unconditional product of $f$ over the subtype $\{x \mid P(x)\}$ is equal to the unconditional product of $f$ over the subtype $\{x \mid Q(x)\}$, i.e., \[ \prod'_{x \in \{x \mid P(x)\}} f(x) = \prod'_{x \in \{x \mid Q(x)\}} f(x). \]

tprod_eq_finprod theorem

(hf : (mulSupport f).Finite) : ∏' b, f b = ∏ᶠ b, f b

Full source

@[to_additive]
theorem tprod_eq_finprod (hf : (mulSupport f).Finite) :
    ∏' b, f b = ∏ᶠ b, f b := by simp [tprod_def, multipliable_of_finite_mulSupport hf, hf]

Unconditional product equals finite product for functions with finite support

Informal description

For a function $f : \beta \to \alpha$ with finite multiplicative support (i.e., the set $\{b \in \beta \mid f(b) \neq 1\}$ is finite), the unconditional product $\prod'_{b} f(b)$ is equal to the finite product $\prodᶠ_{b} f(b)$ over its support.

tprod_eq_prod' theorem

{s : Finset β} (hf : mulSupport f ⊆ s) : ∏' b, f b = ∏ b ∈ s, f b

Full source

@[to_additive]
theorem tprod_eq_prod' {s : Finset β} (hf : mulSupportmulSupport f ⊆ s) :
    ∏' b, f b = ∏ b ∈ s, f b := by
  rw [tprod_eq_finprod (s.finite_toSet.subset hf), finprod_eq_prod_of_mulSupport_subset _ hf]

Unconditional Product Equals Finite Product When Support is Contained in a Finite Set

Informal description

For a function $f : \beta \to \alpha$ and a finite set $s \subseteq \beta$ such that the multiplicative support of $f$ is contained in $s$, the unconditional product $\prod'_{b} f(b)$ is equal to the finite product $\prod_{b \in s} f(b)$.

tprod_eq_prod theorem

{s : Finset β} (hf : ∀ b ∉ s, f b = 1) : ∏' b, f b = ∏ b ∈ s, f b

Full source

@[to_additive]
theorem tprod_eq_prod {s : Finset β} (hf : ∀ b ∉ s, f b = 1) :
    ∏' b, f b = ∏ b ∈ s, f b :=
  tprod_eq_prod' <| mulSupport_subset_iff'.2 hf

Unconditional Product Equals Finite Product Outside Support

Informal description

For a function $f : \beta \to \alpha$ and a finite set $s \subseteq \beta$ such that $f(b) = 1$ for all $b \notin s$, the unconditional product $\prod'_{b} f(b)$ is equal to the finite product $\prod_{b \in s} f(b)$.

tprod_one theorem

: ∏' _ : β, (1 : α) = 1

Full source

@[to_additive (attr := simp)]
theorem tprod_one : ∏' _ : β, (1 : α) = 1 := by rw [tprod_eq_finprod] <;> simp

Unconditional Product of Constant One Function is One

Informal description

The unconditional product of the constant function $f(b) = 1$ over any index set $\beta$ in a commutative topological multiplicative monoid $\alpha$ is equal to $1$, i.e., $\prod'_{b \in \beta} 1 = 1$.

tprod_empty theorem

[IsEmpty β] : ∏' b, f b = 1

Full source

@[to_additive (attr := simp)]
theorem tprod_empty [IsEmpty β] : ∏' b, f b = 1 := by
  rw [tprod_eq_prod (s := (∅ : Finset β))] <;> simp

Unconditional Product over Empty Type is One

Informal description

For any function $f : \beta \to \alpha$ where $\beta$ is an empty type, the unconditional product $\prod'_{b \in \beta} f(b)$ equals $1$.

tprod_congr theorem

{f g : β → α} (hfg : ∀ b, f b = g b) : ∏' b, f b = ∏' b, g b

Full source

@[to_additive]
theorem tprod_congr {f g : β → α}
    (hfg : ∀ b, f b = g b) : ∏' b, f b = ∏' b, g b :=
  congr_arg tprod (funext hfg)

Unconditional Product Equality under Pointwise Function Equality

Informal description

For any two functions $f, g : \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, if $f(b) = g(b)$ for all $b \in \beta$, then the unconditional products $\prod'_{b} f(b)$ and $\prod'_{b} g(b)$ are equal.

tprod_fintype theorem

[Fintype β] (f : β → α) : ∏' b, f b = ∏ b, f b

Full source

@[to_additive]
theorem tprod_fintype [Fintype β] (f : β → α) : ∏' b, f b = ∏ b, f b := by
  apply tprod_eq_prod; simp

Unconditional Product Equals Finite Product for Finite Types

Informal description

For any finite type $\beta$ and any function $f \colon \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, the unconditional product $\prod'_{b \in \beta} f(b)$ is equal to the finite product $\prod_{b \in \beta} f(b)$.

prod_eq_tprod_mulIndicator theorem

(f : β → α) (s : Finset β) : ∏ x ∈ s, f x = ∏' x, Set.mulIndicator (↑s) f x

Full source

@[to_additive]
theorem prod_eq_tprod_mulIndicator (f : β → α) (s : Finset β) :
    ∏ x ∈ s, f x = ∏' x, Set.mulIndicator (↑s) f x := by
  rw [tprod_eq_prod' (Set.mulSupport_mulIndicator_subset),
      Finset.prod_mulIndicator_subset _ Finset.Subset.rfl]

Finite Product as Unconditional Product via Multiplicative Indicator

Informal description

For any function $f \colon \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$ and any finite set $s \subseteq \beta$, the finite product $\prod_{x \in s} f(x)$ is equal to the unconditional product $\prod'_{x} \text{mulIndicator}_s f(x)$, where $\text{mulIndicator}_s f$ is the multiplicative indicator function of $f$ on $s$.

tprod_bool theorem

(f : Bool → α) : ∏' i : Bool, f i = f false * f true

Full source

@[to_additive]
theorem tprod_bool (f : Bool → α) : ∏' i : Bool, f i = f false * f true := by
  rw [tprod_fintype, Fintype.prod_bool, mul_comm]

Unconditional Product over Boolean Values: $\prod'_{i \in \text{Bool}} f(i) = f(\text{false}) \cdot f(\text{true})$

Informal description

For any function $f \colon \text{Bool} \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, the unconditional product $\prod'_{i \in \text{Bool}} f(i)$ is equal to $f(\text{false}) \cdot f(\text{true})$.

tprod_eq_mulSingle theorem

{f : β → α} (b : β) (hf : ∀ b' ≠ b, f b' = 1) : ∏' b, f b = f b

Full source

@[to_additive]
theorem tprod_eq_mulSingle {f : β → α} (b : β) (hf : ∀ b' ≠ b, f b' = 1) :
    ∏' b, f b = f b := by
  rw [tprod_eq_prod (s := {b}), prod_singleton]
  exact fun b' hb' ↦ hf b' (by simpa using hb')

Unconditional Product of Function with Single Non-Identity Value Equals That Value

Informal description

For a function $f \colon \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, if there exists an element $b \in \beta$ such that $f(b') = 1$ for all $b' \neq b$, then the unconditional product $\prod'_{b} f(b)$ equals $f(b)$.

tprod_tprod_eq_mulSingle theorem

 (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ b' ≠ b, f b' c = 1) (hfc : ∀ b', ∀ c' ≠ c, f b' c' = 1) :
  ∏' (b') (c'), f b' c' = f b c

Full source

@[to_additive]
theorem tprod_tprod_eq_mulSingle (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ b' ≠ b, f b' c = 1)
    (hfc : ∀ b', ∀ c' ≠ c, f b' c' = 1) : ∏' (b') (c'), f b' c' = f b c :=
  calc
    ∏' (b') (c'), f b' c' = ∏' b', f b' c := tprod_congr fun b' ↦ tprod_eq_mulSingle _ (hfc b')
    _ = f b c := tprod_eq_mulSingle _ hfb

Double Unconditional Product of Function with Single Non-Identity Value Equals That Value

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid, and let $f \colon \beta \times \gamma \to \alpha$ be a function. Suppose there exist elements $b \in \beta$ and $c \in \gamma$ such that: 1. For all $b' \neq b$ in $\beta$, $f(b', c) = 1$. 2. For all $b' \in \beta$ and $c' \neq c$ in $\gamma$, $f(b', c') = 1$. Then the unconditional double product $\prod'_{(b', c')} f(b', c')$ equals $f(b, c)$.

tprod_ite_eq theorem

(b : β) [DecidablePred (· = b)] (a : α) : ∏' b', (if b' = b then a else 1) = a

Full source

@[to_additive (attr := simp)]
theorem tprod_ite_eq (b : β) [DecidablePred (· = b)] (a : α) :
    ∏' b', (if b' = b then a else 1) = a := by
  rw [tprod_eq_mulSingle b]
  · simp
  · intro b' hb'; simp [hb']

Unconditional Product of Indicator Function at a Point Equals Its Value

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid, $\beta$ a type, and $b \in \beta$. For any element $a \in \alpha$, the unconditional product $\prod'_{b' \in \beta} ( \text{if } b' = b \text{ then } a \text{ else } 1 )$ equals $a$.

Finset.tprod_subtype theorem

(s : Finset β) (f : β → α) : ∏' x : { x // x ∈ s }, f x = ∏ x ∈ s, f x

Full source

@[to_additive (attr := simp)]
theorem Finset.tprod_subtype (s : Finset β) (f : β → α) :
    ∏' x : { x // x ∈ s }, f x = ∏ x ∈ s, f x := by
  rw [← prod_attach]; exact tprod_fintype _

Unconditional Product Equals Finite Product over Subtype

Informal description

For any finite set $s$ of type $\beta$ and any function $f \colon \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, the unconditional product of $f$ over the subtype $\{x \mid x \in s\}$ is equal to the finite product of $f$ over $s$.

Finset.tprod_subtype' theorem

(s : Finset β) (f : β → α) : ∏' x : (s : Set β), f x = ∏ x ∈ s, f x

Full source

@[to_additive]
theorem Finset.tprod_subtype' (s : Finset β) (f : β → α) :
    ∏' x : (s : Set β), f x = ∏ x ∈ s, f x := by simp

Unconditional Product over Finite Set Equals Finite Product

Informal description

For any finite set $s$ of type $\beta$ and any function $f \colon \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, the unconditional product of $f$ over the set $s$ (viewed as a subset of $\beta$) is equal to the finite product of $f$ over $s$.

tprod_singleton theorem

(b : β) (f : β → α) : ∏' x : ({ b } : Set β), f x = f b

Full source

@[to_additive (attr := simp)]
theorem tprod_singleton (b : β) (f : β → α) : ∏' x : ({b} : Set β), f x = f b := by
  rw [← coe_singleton, Finset.tprod_subtype', prod_singleton]

Unconditional Product over Singleton Set Equals Function Value

Informal description

For any element $b$ of type $\beta$ and any function $f \colon \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, the unconditional product of $f$ over the singleton set $\{b\}$ is equal to $f(b)$, i.e., $$\prod'_{x \in \{b\}} f(x) = f(b).$$

Function.Injective.tprod_eq theorem

{g : γ → β} (hg : Injective g) {f : β → α} (hf : mulSupport f ⊆ Set.range g) : ∏' c, f (g c) = ∏' b, f b

Full source

@[to_additive]
theorem Function.Injective.tprod_eq {g : γ → β} (hg : Injective g) {f : β → α}
    (hf : mulSupportmulSupport f ⊆ Set.range g) : ∏' c, f (g c) = ∏' b, f b := by
  have : mulSupport f = g '' mulSupport (f ∘ g) := by
    rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
  rw [← Function.comp_def]
  by_cases hf_fin : (mulSupport f).Finite
  · have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
    lift g to γ ↪ β using hg
    simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge,
      comp_apply, ← Finset.prod_map]
    refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl
    simp [this]
  · have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
    simp_rw [tprod_def, if_neg hf_fin, if_neg hf_fin', Multipliable,
      funext fun a => propext <| hg.hasProd_iff (mulSupport_subset_iff'.1 hf) (a := a)]

Injective Function Preserves Unconditional Product When Support is in Range

Informal description

Let $g : \gamma \to \beta$ be an injective function and $f : \beta \to \alpha$ a function whose multiplicative support is contained in the range of $g$. Then the unconditional product of $f \circ g$ over $\gamma$ equals the unconditional product of $f$ over $\beta$, i.e., $$\prod'_{c \in \gamma} f(g(c)) = \prod'_{b \in \beta} f(b).$$

Equiv.tprod_eq theorem

(e : γ ≃ β) (f : β → α) : ∏' c, f (e c) = ∏' b, f b

Full source

@[to_additive]
theorem Equiv.tprod_eq (e : γ ≃ β) (f : β → α) : ∏' c, f (e c) = ∏' b, f b :=
  e.injective.tprod_eq <| by simp

Unconditional Product Invariance under Bijection: $\prod'_{c} f(e(c)) = \prod'_{b} f(b)$

Informal description

Let $e : \gamma \simeq \beta$ be a bijection between types $\gamma$ and $\beta$, and let $f : \beta \to \alpha$ be a function. Then the unconditional product of $f \circ e$ over $\gamma$ equals the unconditional product of $f$ over $\beta$, i.e., $$\prod'_{c \in \gamma} f(e(c)) = \prod'_{b \in \beta} f(b).$$

tprod_subtype_eq_of_mulSupport_subset theorem

{f : β → α} {s : Set β} (hs : mulSupport f ⊆ s) : ∏' x : s, f x = ∏' x, f x

Full source

@[to_additive]
theorem tprod_subtype_eq_of_mulSupport_subset {f : β → α} {s : Set β} (hs : mulSupportmulSupport f ⊆ s) :
    ∏' x : s, f x = ∏' x, f x :=
  Subtype.val_injective.tprod_eq <| by simpa

Unconditional Product Equality for Functions with Support in Subset

Informal description

Let $f : \beta \to \alpha$ be a function and $s \subseteq \beta$ a subset such that the multiplicative support of $f$ is contained in $s$. Then the unconditional product of $f$ restricted to $s$ equals the unconditional product of $f$ over the entire domain, i.e., $$\prod'_{x \in s} f(x) = \prod'_{x \in \beta} f(x).$$

tprod_subtype_mulSupport theorem

(f : β → α) : ∏' x : mulSupport f, f x = ∏' x, f x

Full source

@[to_additive]
theorem tprod_subtype_mulSupport (f : β → α) : ∏' x : mulSupport f, f x = ∏' x, f x :=
  tprod_subtype_eq_of_mulSupport_subset Set.Subset.rfl

Unconditional Product Equality over Multiplicative Support: $\prod'_{x \in \operatorname{mulSupport} f} f(x) = \prod'_{x} f(x)$

Informal description

For any function $f : \beta \to \alpha$, the unconditional product of $f$ over its multiplicative support equals the unconditional product of $f$ over the entire domain, i.e., $$\prod'_{x \in \operatorname{mulSupport} f} f(x) = \prod'_{x \in \beta} f(x).$$

tprod_subtype theorem

(s : Set β) (f : β → α) : ∏' x : s, f x = ∏' x, s.mulIndicator f x

Full source

@[to_additive]
theorem tprod_subtype (s : Set β) (f : β → α) : ∏' x : s, f x = ∏' x, s.mulIndicator f x := by
  rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr]
  simp

Unconditional Product of Function over Subtype Equals Product of Indicator Function

Informal description

Let $s$ be a subset of $\beta$ and $f : \beta \to \alpha$ a function. The unconditional product of $f$ over the subtype $s$ is equal to the unconditional product of the multiplicative indicator function of $f$ on $s$ over the entire domain, i.e., \[ \prod'_{x \in s} f(x) = \prod'_{x \in \beta} \text{mulIndicator}_s f (x). \] Here, $\text{mulIndicator}_s f (x) = f(x)$ if $x \in s$ and $1$ otherwise.

tprod_univ theorem

(f : β → α) : ∏' x : (Set.univ : Set β), f x = ∏' x, f x

Full source

@[to_additive (attr := simp)]
theorem tprod_univ (f : β → α) : ∏' x : (Set.univ : Set β), f x = ∏' x, f x :=
  tprod_subtype_eq_of_mulSupport_subset <| Set.subset_univ _

Unconditional Product over Universal Set Equals Full Product

Informal description

For any function $f \colon \beta \to \alpha$ mapping into a commutative topological multiplicative monoid $\alpha$, the unconditional product of $f$ over the universal set $\text{univ} \subseteq \beta$ equals the unconditional product of $f$ over the entire domain $\beta$, i.e., $$\prod'_{x \in \text{univ}} f(x) = \prod'_{x \in \beta} f(x).$$

tprod_image theorem

{g : γ → β} (f : β → α) {s : Set γ} (hg : Set.InjOn g s) : ∏' x : g '' s, f x = ∏' x : s, f (g x)

Full source

@[to_additive]
theorem tprod_image {g : γ → β} (f : β → α) {s : Set γ} (hg : Set.InjOn g s) :
    ∏' x : g '' s, f x = ∏' x : s, f (g x) :=
  ((Equiv.Set.imageOfInjOn _ _ hg).tprod_eq fun x ↦ f x).symm

Unconditional Product over Image of Injective Function: $\prod'_{x \in g(s)} f(x) = \prod'_{x \in s} f(g(x))$

Informal description

Let $g : \gamma \to \beta$ be a function and $f : \beta \to \alpha$ be a function into a commutative topological multiplicative monoid $\alpha$. For any subset $s \subseteq \gamma$, if $g$ is injective on $s$, then the unconditional product of $f$ over the image $g(s)$ equals the unconditional product of $f \circ g$ over $s$, i.e., \[ \prod'_{x \in g(s)} f(x) = \prod'_{x \in s} f(g(x)). \]

tprod_range theorem

{g : γ → β} (f : β → α) (hg : Injective g) : ∏' x : Set.range g, f x = ∏' x, f (g x)

Full source

@[to_additive]
theorem tprod_range {g : γ → β} (f : β → α) (hg : Injective g) :
    ∏' x : Set.range g, f x = ∏' x, f (g x) := by
  rw [← Set.image_univ, tprod_image f hg.injOn]
  simp_rw [← comp_apply (g := g), tprod_univ (f ∘ g)]

Unconditional Product over Range of Injective Function: $\prod'_{x \in \mathrm{range}\, g} f(x) = \prod'_{x} f(g(x))$

Informal description

Let $g \colon \gamma \to \beta$ be an injective function and $f \colon \beta \to \alpha$ be a function into a commutative topological multiplicative monoid $\alpha$. Then the unconditional product of $f$ over the range of $g$ equals the unconditional product of $f \circ g$ over the entire domain $\gamma$, i.e., \[ \prod'_{x \in \mathrm{range}\, g} f(x) = \prod'_{x \in \gamma} f(g(x)). \]

tprod_setElem_eq_tprod_setElem_diff theorem

{f : β → α} (s t : Set β) (hf₀ : ∀ b ∈ t, f b = 1) : ∏' a : s, f a = ∏' a : (s \ t : Set β), f a

Full source

/-- If `f b = 1` for all `b ∈ t`, then the product of `f a` with `a ∈ s` is the same as the
product of `f a` with `a ∈ s ∖ t`. -/
@[to_additive "If `f b = 0` for all `b ∈ t`, then the sum of `f a` with `a ∈ s` is the same as the
sum of `f a` with `a ∈ s ∖ t`."]
lemma tprod_setElem_eq_tprod_setElem_diff {f : β → α} (s t : Set β)
    (hf₀ : ∀ b ∈ t, f b = 1) :
    ∏' a : s, f a = ∏' a : (s \ t : Set β), f a :=
  .symm <| (Set.inclusion_injective (t := s) Set.diff_subset).tprod_eq (f := f ∘ (↑)) <|
    mulSupport_subset_iff'.2 fun b hb ↦ hf₀ b <| by simpa using hb

Unconditional Product Equality over Set Difference When Function Vanishes on Subset

Informal description

Let $f : \beta \to \alpha$ be a function into a commutative topological multiplicative monoid $\alpha$, and let $s, t$ be subsets of $\beta$. If $f(b) = 1$ for all $b \in t$, then the unconditional product of $f$ over $s$ is equal to the unconditional product of $f$ over the set difference $s \setminus t$, i.e., \[ \prod'_{a \in s} f(a) = \prod'_{a \in s \setminus t} f(a). \]

tprod_eq_tprod_diff_singleton theorem

{f : β → α} (s : Set β) {b : β} (hf₀ : f b = 1) : ∏' a : s, f a = ∏' a : (s \ { b } : Set β), f a

Full source

/-- If `f b = 1`, then the product of `f a` with `a ∈ s` is the same as the product of `f a` for
`a ∈ s ∖ {b}`. -/
@[to_additive "If `f b = 0`, then the sum of `f a` with `a ∈ s` is the same as the sum of `f a`
for `a ∈ s ∖ {b}`."]
lemma tprod_eq_tprod_diff_singleton {f : β → α} (s : Set β) {b : β} (hf₀ : f b = 1) :
    ∏' a : s, f a = ∏' a : (s \ {b} : Set β), f a :=
  tprod_setElem_eq_tprod_setElem_diff s {b} fun _ ha ↦ ha ▸ hf₀

Unconditional Product Equality over Set Difference with Singleton When Function Vanishes at Point

Informal description

Let $f : \beta \to \alpha$ be a function into a commutative topological multiplicative monoid $\alpha$, and let $s$ be a subset of $\beta$. If $f(b) = 1$ for some element $b \in \beta$, then the unconditional product of $f$ over $s$ is equal to the unconditional product of $f$ over the set difference $s \setminus \{b\}$, i.e., \[ \prod'_{a \in s} f(a) = \prod'_{a \in s \setminus \{b\}} f(a). \]

tprod_eq_tprod_of_ne_one_bij theorem

 {g : γ → α} (i : mulSupport g → β) (hi : Injective i) (hf : mulSupport f ⊆ Set.range i) (hfg : ∀ x, f (i x) = g x) :
  ∏' x, f x = ∏' y, g y

Full source

@[to_additive]
theorem tprod_eq_tprod_of_ne_one_bij {g : γ → α} (i : mulSupport g → β) (hi : Injective i)
    (hf : mulSupportmulSupport f ⊆ Set.range i) (hfg : ∀ x, f (i x) = g x) : ∏' x, f x = ∏' y, g y := by
  rw [← tprod_subtype_mulSupport g, ← hi.tprod_eq hf]
  simp only [hfg]

Equality of Unconditional Products via Bijection on Multiplicative Supports

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions into a commutative topological multiplicative monoid $\alpha$. Suppose there exists an injective function $i : \operatorname{mulSupport} g \to \beta$ such that: 1. The multiplicative support of $f$ is contained in the range of $i$, and 2. For all $x \in \operatorname{mulSupport} g$, we have $f(i(x)) = g(x)$. Then the unconditional products of $f$ and $g$ are equal, i.e., $$\prod'_{x \in \beta} f(x) = \prod'_{y \in \gamma} g(y).$$

Equiv.tprod_eq_tprod_of_mulSupport theorem

 {f : β → α} {g : γ → α} (e : mulSupport f ≃ mulSupport g) (he : ∀ x, g (e x) = f x) : ∏' x, f x = ∏' y, g y

Full source

@[to_additive]
theorem Equiv.tprod_eq_tprod_of_mulSupport {f : β → α} {g : γ → α}
    (e : mulSupportmulSupport f ≃ mulSupport g) (he : ∀ x, g (e x) = f x) :
    ∏' x, f x = ∏' y, g y :=
  .symm <| tprod_eq_tprod_of_ne_one_bij _ (Subtype.val_injective.comp e.injective) (by simp) he

Equality of Unconditional Products via Bijection on Multiplicative Supports

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions into a commutative topological multiplicative monoid $\alpha$. Suppose there exists an equivalence (bijection) $e$ between the multiplicative supports of $f$ and $g$ such that for all $x$ in the multiplicative support of $f$, we have $g(e(x)) = f(x)$. Then the unconditional products of $f$ and $g$ are equal, i.e., $$\prod'_{x \in \beta} f(x) = \prod'_{y \in \gamma} g(y).$$

tprod_dite_right theorem

 (P : Prop) [Decidable P] (x : β → ¬P → α) :
  ∏' b : β, (if h : P then (1 : α) else x b h) = if h : P then (1 : α) else ∏' b : β, x b h

Full source

@[to_additive]
theorem tprod_dite_right (P : Prop) [Decidable P] (x : β → ¬P → α) :
    ∏' b : β, (if h : P then (1 : α) else x b h) = if h : P then (1 : α) else ∏' b : β, x b h := by
  by_cases hP : P <;> simp [hP]

Unconditional Product of Conditional Function (Right Case)

Informal description

Let $P$ be a decidable proposition and let $x : \beta \to \neg P \to \alpha$ be a function. Then the unconditional product can be expressed as: \[ \prod'_{b \in \beta} \begin{cases} 1 & \text{if } P \\ x(b, h) & \text{if } \neg P \text{ (with } h : \neg P\text{)} \end{cases} = \begin{cases} 1 & \text{if } P \\ \prod'_{b \in \beta} x(b, h) & \text{if } \neg P \text{ (with } h : \neg P\text{)} \end{cases} \]

tprod_dite_left theorem

 (P : Prop) [Decidable P] (x : β → P → α) :
  ∏' b : β, (if h : P then x b h else 1) = if h : P then ∏' b : β, x b h else 1

Full source

@[to_additive]
theorem tprod_dite_left (P : Prop) [Decidable P] (x : β → P → α) :
    ∏' b : β, (if h : P then x b h else 1) = if h : P then ∏' b : β, x b h else 1 := by
  by_cases hP : P <;> simp [hP]

Unconditional Product of Conditional Function with Left Case

Informal description

Let $P$ be a decidable proposition and let $x : \beta \to P \to \alpha$ be a function. The unconditional product $\prod'_{b \in \beta} \text{if } h : P \text{ then } x(b)(h) \text{ else } 1$ is equal to $\text{if } h : P \text{ then } \prod'_{b \in \beta} x(b)(h) \text{ else } 1$.

tprod_extend_one theorem

{γ : Type*} {g : γ → β} (hg : Injective g) (f : γ → α) : ∏' y, extend g f 1 y = ∏' x, f x

Full source

@[to_additive (attr := simp)]
lemma tprod_extend_one {γ : Type*} {g : γ → β} (hg : Injective g) (f : γ → α) :
    ∏' y, extend g f 1 y = ∏' x, f x := by
  have : mulSupportmulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _
  simp_rw [← hg.tprod_eq this, hg.extend_apply]

Unconditional Product of Extended Function Along Injection Equals Original Product

Informal description

Let $g : \gamma \to \beta$ be an injective function and $f : \gamma \to \alpha$ a function. Then the unconditional product of the extension of $f$ along $g$ (with default value $1$) equals the unconditional product of $f$, i.e., \[ \prod'_{y \in \beta} \text{extend}\,g\,f\,1\,y = \prod'_{x \in \gamma} f(x). \]

Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd theorem

 {α' : Type*} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) (h1 : e 1 = 1)
  {f : β → α} {g : γ → α'} (h : ∀ {a}, HasProd f (e a) ↔ HasProd g a) : ∏' b, f b = e (∏' c, g c)

Full source

@[to_additive]
theorem Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd {α' : Type*} [CommMonoid α']
    [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) (h1 : e 1 = 1) {f : β → α}
    {g : γ → α'} (h : ∀ {a}, HasProdHasProd f (e a) ↔ HasProd g a) : ∏' b, f b = e (∏' c, g c) :=
  by_cases (fun x ↦ (h.mpr x.hasProd).tprod_eq) fun hg : ¬Multipliable g ↦ by
    have hf : ¬Multipliable f := mt (hes.multipliable_iff_of_hasProd_iff @h).1 hg
    simp [tprod_def, hf, hg, h1]

Unconditional Product Equality under Surjective Mapping with Product Convergence Equivalence

Informal description

Let $\alpha'$ be a commutative topological monoid and $e : \alpha' \to \alpha$ a surjective function preserving the multiplicative identity (i.e., $e(1) = 1$). Given functions $f : \beta \to \alpha$ and $g : \gamma \to \alpha'$, suppose that for any $a \in \alpha'$, the product of $f$ converges to $e(a)$ if and only if the product of $g$ converges to $a$. Then the unconditional product of $f$ equals the image under $e$ of the unconditional product of $g$, i.e., \[ \prod'_{b} f(b) = e\left(\prod'_{c} g(c)\right). \]

tprod_eq_tprod_of_hasProd_iff_hasProd theorem

{f : β → α} {g : γ → α} (h : ∀ {a}, HasProd f a ↔ HasProd g a) : ∏' b, f b = ∏' c, g c

Full source

@[to_additive]
theorem tprod_eq_tprod_of_hasProd_iff_hasProd {f : β → α} {g : γ → α}
    (h : ∀ {a}, HasProdHasProd f a ↔ HasProd g a) : ∏' b, f b = ∏' c, g c :=
  surjective_id.tprod_eq_tprod_of_hasProd_iff_hasProd rfl @h

Equality of Unconditional Products under Equivalent Convergence Conditions

Informal description

Let $f : \beta \to \alpha$ and $g : \gamma \to \alpha$ be functions in a commutative topological monoid $\alpha$. If for every $a \in \alpha$, the product of $f$ converges to $a$ if and only if the product of $g$ converges to $a$, then the unconditional products of $f$ and $g$ are equal, i.e., \[ \prod'_{b} f(b) = \prod'_{c} g(c). \]

Multipliable.tprod_mul 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_mul (hf : Multipliable f) (hg : Multipliable g) :
    ∏' b, (f b * g b) = (∏' b, f b) * ∏' b, g b :=
  (hf.hasProd.mul hg.hasProd).tprod_eq

Product of Unconditional Products: $\prod' (f \cdot g) = (\prod' f) \cdot (\prod' g)$

Informal description

For two multipliable functions $f, g : \beta \to \alpha$ in a commutative topological multiplicative monoid $\alpha$, the unconditional product of their pointwise product equals the product of their unconditional products, i.e., \[ \prod'_{b} (f(b) \cdot g(b)) = \left(\prod'_{b} f(b)\right) \cdot \left(\prod'_{b} g(b)\right). \]

Multipliable.tprod_finsetProd theorem

 {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i)) : ∏' b, ∏ i ∈ s, f i b = ∏ i ∈ s, ∏' b, f i b

Full source

@[to_additive]
protected theorem Multipliable.tprod_finsetProd {f : γ → β → α} {s : Finset γ}
    (hf : ∀ i ∈ s, Multipliable (f i)) : ∏' b, ∏ i ∈ s, f i b = ∏ i ∈ s, ∏' b, f i b :=
  (hasProd_prod fun i hi ↦ (hf i hi).hasProd).tprod_eq

Product of Unconditional Products over a Finite Index Set

Informal description

Let $f : \gamma \to \beta \to \alpha$ be a family of functions and $s$ be a finite subset of $\gamma$. If for every $i \in s$, the function $f(i)$ is multipliable, then the unconditional product of the pointwise product function $\prod_{i \in s} f(i)(b)$ over $\beta$ is equal to the product over $s$ of the unconditional products of $f(i)$ over $\beta$, i.e., \[ \prod'_{b} \prod_{i \in s} f(i)(b) = \prod_{i \in s} \prod'_{b} f(i)(b). \]

Multipliable.tprod_eq_mul_tprod_ite' theorem

 [DecidableEq β] {f : β → α} (b : β) (hf : Multipliable (update f b 1)) : ∏' x, f x = f b * ∏' x, ite (x = b) 1 (f x)

Full source

/-- Version of `tprod_eq_mul_tprod_ite` for `CommMonoid` rather than `CommGroup`.
Requires a different convergence assumption involving `Function.update`. -/
@[to_additive "Version of `tsum_eq_add_tsum_ite` for `AddCommMonoid` rather than `AddCommGroup`.
Requires a different convergence assumption involving `Function.update`."]
protected theorem Multipliable.tprod_eq_mul_tprod_ite' [DecidableEq β] {f : β → α} (b : β)
    (hf : Multipliable (update f b 1)) :
    ∏' x, f x = f b * ∏' x, ite (x = b) 1 (f x) :=
  calc
    ∏' x, f x = ∏' x, (ite (x = b) (f x) 1 * update f b 1 x) :=
      tprod_congr fun n ↦ by split_ifs with h <;> simp [update_apply, h]
    _ = (∏' x, ite (x = b) (f x) 1) * ∏' x, update f b 1 x :=
      Multipliable.tprod_mul ⟨ite (b = b) (f b) 1, hasProd_single b fun _ hb ↦ if_neg hb⟩ hf
    _ = ite (b = b) (f b) 1 * ∏' x, update f b 1 x := by
      congr
      exact tprod_eq_mulSingle b fun b' hb' ↦ if_neg hb'
    _ = f b * ∏' x, ite (x = b) 1 (f x) := by
      simp only [update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite]

Product Decomposition at a Point: $\prod' f = f(b) \cdot \prod'_{x \neq b} f(x)$

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid and $\beta$ a type with decidable equality. For any function $f \colon \beta \to \alpha$ and any element $b \in \beta$, if the function $\text{update } f \, b \, 1$ (which equals $f$ everywhere except at $b$ where it takes value $1$) is multipliable, then the unconditional product of $f$ satisfies: \[ \prod'_{x} f(x) = f(b) \cdot \prod'_{x} \begin{cases} 1 & \text{if } x = b, \\ f(x) & \text{otherwise.} \end{cases} \]

Multipliable.tprod_mul_tprod_compl theorem

 {s : Set β} (hs : Multipliable (f ∘ (↑) : s → α)) (hsc : Multipliable (f ∘ (↑) : ↑sᶜ → α)) :
  (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x

Full source

@[to_additive]
protected theorem Multipliable.tprod_mul_tprod_compl {s : Set β}
    (hs : Multipliable (f ∘ (↑) : s → α)) (hsc : Multipliable (f ∘ (↑) : ↑sᶜ → α)) :
    (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x :=
  (hs.hasProd.mul_compl hsc.hasProd).tprod_eq.symm

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

Informal description

Let $f : \beta \to \alpha$ be a function and $s \subseteq \beta$ a subset. If the restriction of $f$ to $s$ is multipliable and the restriction of $f$ to the complement $s^\complement$ is multipliable, then the product of $f$ over all of $\beta$ equals the product of the restrictions multiplied together, i.e., \[ \left(\prod'_{x \in s} f(x)\right) \cdot \left(\prod'_{x \in s^\complement} f(x)\right) = \prod'_{x} f(x). \]

Multipliable.tprod_union_disjoint theorem

 {s t : Set β} (hd : Disjoint s t) (hs : Multipliable (f ∘ (↑) : s → α)) (ht : Multipliable (f ∘ (↑) : t → α)) :
  ∏' x : ↑(s ∪ t), f x = (∏' x : s, f x) * ∏' x : t, f x

Full source

@[to_additive]
protected theorem Multipliable.tprod_union_disjoint {s t : Set β} (hd : Disjoint s t)
    (hs : Multipliable (f ∘ (↑) : s → α)) (ht : Multipliable (f ∘ (↑) : t → α)) :
    ∏' x : ↑(s ∪ t), f x = (∏' x : s, f x) * ∏' x : t, f x :=
  (hs.hasProd.mul_disjoint hd ht.hasProd).tprod_eq

Product Decomposition over Disjoint Union: $\prod'_{s \cup t} f = \prod'_s f \cdot \prod'_t f$

Informal description

Let $s$ and $t$ be disjoint subsets of $\beta$, and let $f : \beta \to \alpha$ be a function. If the restriction of $f$ to $s$ is multipliable and the restriction of $f$ to $t$ is multipliable, then the unconditional product of $f$ over $s \cup t$ is equal to the product of the unconditional products over $s$ and $t$, i.e., \[ \prod'_{x \in s \cup t} f(x) = \left(\prod'_{x \in s} f(x)\right) \cdot \left(\prod'_{x \in t} f(x)\right). \]

Multipliable.tprod_finset_bUnion_disjoint theorem

 {ι} {s : Finset ι} {t : ι → Set β} (hd : (s : Set ι).Pairwise (Disjoint on t))
  (hf : ∀ i ∈ s, Multipliable (f ∘ (↑) : t i → α)) : ∏' x : ⋃ i ∈ s, t i, f x = ∏ i ∈ s, ∏' x : t i, f x

Full source

@[to_additive]
protected theorem Multipliable.tprod_finset_bUnion_disjoint {ι} {s : Finset ι} {t : ι → Set β}
    (hd : (s : Set ι).Pairwise (DisjointDisjoint on t)) (hf : ∀ i ∈ s, Multipliable (f ∘ (↑) : t i → α)) :
    ∏' x : ⋃ i ∈ s, t i, f x = ∏ i ∈ s, ∏' x : t i, f x :=
  (hasProd_prod_disjoint _ hd fun i hi ↦ (hf i hi).hasProd).tprod_eq

Product Decomposition over Pairwise Disjoint Union: $\prod'_{\bigcup_{i \in s} t_i} f = \prod_{i \in s} \prod'_{t_i} f$

Informal description

Let $\{t_i\}_{i \in \iota}$ be a family of pairwise disjoint subsets of $\beta$, and let $s$ be a finite subset of $\iota$. If for each $i \in s$, the restriction of $f$ to $t_i$ is multipliable, then the unconditional product of $f$ over the union $\bigcup_{i \in s} t_i$ equals the finite product over $s$ of the unconditional products of $f$ over each $t_i$, i.e., \[ \prod'_{x \in \bigcup_{i \in s} t_i} f(x) = \prod_{i \in s} \prod'_{x \in t_i} f(x). \]

hasProd_zero_of_exists_eq_zero theorem

(hf : ∃ b, f b = 0) : HasProd f 0

Full source

lemma hasProd_zero_of_exists_eq_zero (hf : ∃ b, f b = 0) : HasProd f 0 := by
  obtain ⟨b, hb⟩ := hf
  apply tendsto_const_nhds.congr'
  filter_upwards [eventually_ge_atTop {b}] with s hs
  exact (Finset.prod_eq_zero (Finset.singleton_subset_iff.mp hs) hb).symm

Existence of Zero Implies Product Converges to Zero

Informal description

If there exists an element $b$ such that $f(b) = 0$, then the function $f$ has an unconditional product converging to $0$.

multipliable_of_exists_eq_zero theorem

(hf : ∃ b, f b = 0) : Multipliable f

Full source

lemma multipliable_of_exists_eq_zero (hf : ∃ b, f b = 0) : Multipliable f :=
  ⟨0, hasProd_zero_of_exists_eq_zero hf⟩

Multipliability from Existence of Zero

Informal description

If there exists an element $b$ such that $f(b) = 0$, then the function $f$ is multipliable.

tprod_of_exists_eq_zero theorem

[T2Space α] (hf : ∃ b, f b = 0) : ∏' b, f b = 0

Full source

lemma tprod_of_exists_eq_zero [T2Space α] (hf : ∃ b, f b = 0) : ∏' b, f b = 0 :=
  (hasProd_zero_of_exists_eq_zero hf).tprod_eq

Unconditional Product Vanishes When Function Has Zero in Hausdorff Monoid

Informal description

In a Hausdorff topological monoid $\alpha$, if there exists an element $b$ such that $f(b) = 0$, then the unconditional product $\prod'_{b} f(b)$ converges to $0$.