Mathlib.Topology.Algebra.InfiniteSum.Constructions

hasProd_pi_single theorem

[DecidableEq β] (b : β) (a : α) : HasProd (Pi.mulSingle b a) a

Full source

@[to_additive]
theorem hasProd_pi_single [DecidableEq β] (b : β) (a : α) : HasProd (Pi.mulSingle b a) a := by
  convert hasProd_ite_eq b a
  simp [Pi.mulSingle_apply]

Product Convergence of Multiplicative Single Function: $\prod_{b'} \text{mulSingle}_b(a)(b') = a$

Informal description

For any type $\beta$ with decidable equality, any element $b \in \beta$, and any element $a$ in a commutative topological multiplicative monoid $\alpha$, the function $\text{mulSingle}_b(a) : \beta \to \alpha$ has an unconditional product converging to $a$. That is, the product $\prod_{b' \in \beta} \text{mulSingle}_b(a)(b')$ exists and equals $a$.

tprod_pi_single theorem

[DecidableEq β] (b : β) (a : α) : ∏' b', Pi.mulSingle b a b' = a

Full source

@[to_additive (attr := simp)]
theorem tprod_pi_single [DecidableEq β] (b : β) (a : α) : ∏' b', Pi.mulSingle b a b' = a := by
  rw [tprod_eq_mulSingle b]
  · simp
  · intro b' hb'; simp [hb']

Unconditional Product of Multiplicative Single Function

Informal description

For any type $\beta$ with decidable equality, any element $b \in \beta$, and any element $a$ in a commutative topological multiplicative monoid $\alpha$, the unconditional product of the multiplicative single function $\text{mulSingle } b \, a$ over all $b' \in \beta$ equals $a$, i.e., \[ \prod_{b' \in \beta} \text{mulSingle } b \, a \, b' = a. \]

tprod_setProd_singleton_left theorem

(b : β) (t : Set γ) (f : β × γ → α) : (∏' x : { b } ×ˢ t, f x) = ∏' c : t, f (b, c)

Full source

@[to_additive tsum_setProd_singleton_left]
lemma tprod_setProd_singleton_left (b : β) (t : Set γ) (f : β × γ → α) :
    (∏' x : {b} ×ˢ t, f x) = ∏' c : t, f (b, c) := by
  rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ (Prod.mk_right_injective b).injOn]

Unconditional Product over Left Singleton Cartesian Product: $\prod_{\{b\} \times t} f = \prod_{t} f(b, \cdot)$

Informal description

For any element $b \in \beta$, any set $t \subseteq \gamma$, and any function $f : \beta \times \gamma \to \alpha$, the unconditional product of $f$ over the Cartesian product $\{b\} \times t$ equals the unconditional product of $\lambda c, f(b, c)$ over $t$. That is, \[ \prod_{x \in \{b\} \times t} f(x) = \prod_{c \in t} f(b, c). \]

tprod_setProd_singleton_right theorem

(s : Set β) (c : γ) (f : β × γ → α) : (∏' x : s ×ˢ { c }, f x) = ∏' b : s, f (b, c)

Full source

@[to_additive tsum_setProd_singleton_right]
lemma tprod_setProd_singleton_right (s : Set β) (c : γ) (f : β × γ → α) :
    (∏' x : s ×ˢ {c}, f x) = ∏' b : s, f (b, c) := by
  rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ (Prod.mk_left_injective c).injOn]

Unconditional Product over Cartesian Product with Singleton: $\prod_{s \times \{c\}} f = \prod_{s} f(\cdot, c)$

Informal description

For any set $s \subseteq \beta$, any element $c \in \gamma$, and any function $f : \beta \times \gamma \to \alpha$, the unconditional product of $f$ over the Cartesian product $s \times \{c\}$ equals the unconditional product of $\lambda b \in s, f(b, c)$ over $s$. That is, \[ \prod_{x \in s \times \{c\}} f(x) = \prod_{b \in s} f(b, c). \]

Multipliable.prod_symm theorem

{f : β × γ → α} (hf : Multipliable f) : Multipliable fun p : γ × β ↦ f p.swap

Full source

@[to_additive Summable.prod_symm]
theorem Multipliable.prod_symm {f : β × γ → α} (hf : Multipliable f) :
    Multipliable fun p : γ × β ↦ f p.swap :=
  (Equiv.prodComm γ β).multipliable_iff.2 hf

Multipliability under Pair Swapping

Informal description

Let $f : \beta \times \gamma \to \alpha$ be a multipliable function. Then the function $p \mapsto f(p.\text{swap})$, where $p.\text{swap}$ denotes the swapped pair $(p_2, p_1)$ for $p = (p_1, p_2) \in \gamma \times \beta$, is also multipliable.

HasProd.prodMk theorem

 {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasProd f a) (hg : HasProd g b) :
  HasProd (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩

Full source

@[to_additive HasSum.prodMk]
theorem HasProd.prodMk {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasProd f a)
    (hg : HasProd g b) : HasProd (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ := by
  simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prodMk_nhds hf hg]

Product of Convergent Products in Product Space

Informal description

Let $f : \beta \to \alpha$ and $g : \beta \to \gamma$ be functions with unconditional products converging to $a \in \alpha$ and $b \in \gamma$ respectively. Then the function $x \mapsto (f(x), g(x))$ has an unconditional product converging to $(a, b)$ in $\alpha \times \gamma$.

HasProd.sum theorem

 {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : α ⊕ β → M} {a b : M}
  (h₁ : HasProd (f ∘ Sum.inl) a) (h₂ : HasProd (f ∘ Sum.inr) b) : HasProd f (a * b)

Full source

@[to_additive]
lemma HasProd.sum {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M]
    {f : α ⊕ β → M} {a b : M}
    (h₁ : HasProd (f ∘ Sum.inl) a) (h₂ : HasProd (f ∘ Sum.inr) b) : HasProd f (a * b) := by
  have : Tendsto ((∏ b ∈ ·, f b) ∘ sumEquiv.symm) (atTop.map sumEquiv) (nhds (a * b)) := by
    rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]
    convert (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))
    ext s
    simp
  simpa [Tendsto, ← Filter.map_map] using this

Product Convergence over Sum Type: $(\prod_{x \in \alpha} f(x)) \cdot (\prod_{y \in \beta} f(y)) = \prod_{z \in \alpha \oplus \beta} f(z)$

Informal description

Let $M$ be a topological commutative monoid with continuous multiplication and $f : \alpha \oplus \beta \to M$ be a function. If the restriction of $f$ to $\alpha$ has a product converging to $a \in M$ and the restriction of $f$ to $\beta$ has a product converging to $b \in M$, then the product of $f$ over $\alpha \oplus \beta$ converges to $a \cdot b$.

Multipliable.tprod_sum theorem

 {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : α ⊕ β → M}
  (h₁ : Multipliable (f ∘ .inl)) (h₂ : Multipliable (f ∘ .inr)) : ∏' i, f i = (∏' i, f (.inl i)) * (∏' i, f (.inr i))

Full source

@[to_additive "For the statement that `tsum` commutes with `Finset.sum`,
  see `Summable.tsum_finsetSum`."]
protected lemma Multipliable.tprod_sum {α β M : Type*} [CommMonoid M] [TopologicalSpace M]
    [ContinuousMul M] [T2Space M] {f : α ⊕ β → M} (h₁ : Multipliable (f ∘ .inl))
    (h₂ : Multipliable (f ∘ .inr)) : ∏' i, f i = (∏' i, f (.inl i)) * (∏' i, f (.inr i)) :=
  (h₁.hasProd.sum h₂.hasProd).tprod_eq

Unconditional Product Decomposition over Sum Type: $\prod'_{i} f(i) = (\prod'_{i} f(\mathrm{inl}(i))) \cdot (\prod'_{i} f(\mathrm{inr}(i)))$

Informal description

Let $M$ be a Hausdorff topological commutative monoid with continuous multiplication, and let $f : \alpha \oplus \beta \to M$ be a function. If the restrictions $f \circ \mathrm{inl} : \alpha \to M$ and $f \circ \mathrm{inr} : \beta \to M$ are multipliable, then the unconditional product of $f$ over $\alpha \oplus \beta$ equals the product of the unconditional products of $f \circ \mathrm{inl}$ and $f \circ \mathrm{inr}$, i.e., \[ \prod'_{i} f(i) = \left(\prod'_{i} f(\mathrm{inl}(i))\right) \cdot \left(\prod'_{i} f(\mathrm{inr}(i))\right). \]

Multipliable.sum theorem

 {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] (f : α ⊕ β → M) (h₁ : Multipliable (f ∘ Sum.inl))
  (h₂ : Multipliable (f ∘ Sum.inr)) : Multipliable f

Full source

@[to_additive]
lemma Multipliable.sum {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M]
    (f : α ⊕ β → M) (h₁ : Multipliable (f ∘ Sum.inl)) (h₂ : Multipliable (f ∘ Sum.inr)) :
    Multipliable f :=
  ⟨_, .sum h₁.hasProd h₂.hasProd⟩

Multipliability of a Function over a Sum Type

Informal description

Let $M$ be a topological commutative monoid with continuous multiplication and $f : \alpha \oplus \beta \to M$ be a function. If the restriction of $f$ to $\alpha$ (i.e., $f \circ \mathrm{inl}$) is multipliable and the restriction of $f$ to $\beta$ (i.e., $f \circ \mathrm{inr}$) is multipliable, then $f$ itself is multipliable.

HasProd.sigma theorem

 {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α} (ha : HasProd f a)
  (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) : HasProd g a

Full source

@[to_additive]
theorem HasProd.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
    (ha : HasProd f a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) : HasProd g a := by
  classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
  have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finset_prod _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩

Convergence of Fiberwise Products Implies Convergence of the Global Product

Informal description

Let $\alpha$ be a topological space, $\beta$ an index type, and $\gamma : \beta \to \text{Type}$ a family of types. Given a function $f : (\Sigma b : \beta, \gamma b) \to \alpha$ and a function $g : \beta \to \alpha$, suppose that: 1. The product of $f$ converges to $a \in \alpha$ (i.e., $\text{HasProd} f a$ holds), and 2. For every $b \in \beta$, the product of the function $c \mapsto f \langle b, c \rangle$ converges to $g(b)$ (i.e., $\text{HasProd} (c \mapsto f \langle b, c \rangle) (g b)$ holds for all $b$). Then the product of $g$ converges to $a$ (i.e., $\text{HasProd} g a$ holds).

HasProd.prod_fiberwise theorem

 {f : β × γ → α} {g : β → α} {a : α} (ha : HasProd f a) (hf : ∀ b, HasProd (fun c ↦ f (b, c)) (g b)) : HasProd g a

Full source

/-- If a function `f` on `β × γ` has product `a` and for each `b` the restriction of `f` to
`{b} × γ` has product `g b`, then the function `g` has product `a`. -/
@[to_additive HasSum.prod_fiberwise "If a series `f` on `β × γ` has sum `a` and for each `b` the
restriction of `f` to `{b} × γ` has sum `g b`, then the series `g` has sum `a`."]
theorem HasProd.prod_fiberwise {f : β × γ → α} {g : β → α} {a : α} (ha : HasProd f a)
    (hf : ∀ b, HasProd (fun c ↦ f (b, c)) (g b)) : HasProd g a :=
  HasProd.sigma ((Equiv.sigmaEquivProd β γ).hasProd_iff.2 ha) hf

Fiberwise Product Convergence Implies Global Product Convergence

Informal description

Let $f : \beta \times \gamma \to \alpha$ be a function such that its product converges to $a \in \alpha$ (i.e., $\text{HasProd} f a$ holds). Suppose that for each $b \in \beta$, the product of the function $c \mapsto f(b, c)$ converges to $g(b)$. Then the product of $g$ converges to $a$ (i.e., $\text{HasProd} g a$ holds).

Multipliable.sigma' theorem

 {γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f) (hf : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) :
  Multipliable fun b ↦ ∏' c, f ⟨b, c⟩

Full source

@[to_additive]
theorem Multipliable.sigma' {γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f)
    (hf : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) : Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ :=
  (ha.hasProd.sigma fun b ↦ (hf b).hasProd).multipliable

Multipliability of Fiberwise Products Implies Multipliability of Global Product

Informal description

Let $\alpha$ be a topological space, $\beta$ an index type, and $\gamma : \beta \to \text{Type}$ a family of types. Given a function $f : (\Sigma b : \beta, \gamma b) \to \alpha$, suppose that: 1. $f$ is multipliable, and 2. For every $b \in \beta$, the function $c \mapsto f \langle b, c \rangle$ is multipliable. Then the function $b \mapsto \prod'_{c} f \langle b, c \rangle$ is multipliable.

HasProd.sigma_of_hasProd theorem

 {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α} (ha : HasProd g a)
  (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Multipliable f) : HasProd f a

Full source

@[to_additive]
theorem HasProd.sigma_of_hasProd {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α}
    {a : α} (ha : HasProd g a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Multipliable f) :
    HasProd f a := by simpa [(hf'.hasProd.sigma hf).unique ha] using hf'.hasProd

Convergence of Fiberwise Products and Multipliability Imply Global Product Convergence

Informal description

Let $\alpha$ be a topological space, $\beta$ an index type, and $\gamma : \beta \to \text{Type}$ a family of types. Given a function $f : (\Sigma b : \beta, \gamma b) \to \alpha$ and a function $g : \beta \to \alpha$, suppose that: 1. The product of $g$ converges to $a \in \alpha$ (i.e., $\text{HasProd} g a$ holds), 2. For every $b \in \beta$, the product of the function $c \mapsto f \langle b, c \rangle$ converges to $g(b)$ (i.e., $\text{HasProd} (c \mapsto f \langle b, c \rangle) (g b)$ holds for all $b$), and 3. The function $f$ is multipliable (i.e., $\text{Multipliable} f$ holds). Then the product of $f$ converges to $a$ (i.e., $\text{HasProd} f a$ holds).

Multipliable.tprod_sigma' theorem

 {γ : β → Type*} {f : (Σ b : β, γ b) → α} (h₁ : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) (h₂ : Multipliable f) :
  ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩

Full source

@[to_additive]
protected theorem Multipliable.tprod_sigma' {γ : β → Type*} {f : (Σ b : β, γ b) → α}
    (h₁ : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) (h₂ : Multipliable f) :
    ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
  (h₂.hasProd.sigma fun b ↦ (h₁ b).hasProd).tprod_eq.symm

Sigma-Type Unconditional Product Decomposition: $\prod'_{p} f(p) = \prod'_{b,c} f \langle b, c \rangle$

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid, $\beta$ an index type, and $\gamma : \beta \to \text{Type}$ a family of types. Given a function $f : (\Sigma b : \beta, \gamma b) \to \alpha$ such that: 1. For every $b \in \beta$, the function $c \mapsto f \langle b, c \rangle$ is multipliable, and 2. The function $f$ itself is multipliable, then the unconditional product $\prod'_{p} f(p)$ equals the iterated unconditional product $\prod'_{b} \prod'_{c} f \langle b, c \rangle$.

Multipliable.tprod_prod' theorem

 {f : β × γ → α} (h : Multipliable f) (h₁ : ∀ b, Multipliable fun c ↦ f (b, c)) : ∏' p, f p = ∏' (b) (c), f (b, c)

Full source

@[to_additive Summable.tsum_prod']
protected theorem Multipliable.tprod_prod' {f : β × γ → α} (h : Multipliable f)
    (h₁ : ∀ b, Multipliable fun c ↦ f (b, c)) :
    ∏' p, f p = ∏' (b) (c), f (b, c) :=
  (h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm

Product Decomposition of Unconditional Product: $\prod'_{p} f(p) = \prod'_{b,c} f(b, c)$

Informal description

Let $f : \beta \times \gamma \to \alpha$ be a multipliable function in a commutative topological multiplicative monoid $\alpha$. Suppose that for every $b \in \beta$, the function $c \mapsto f(b, c)$ is multipliable. Then the unconditional product $\prod'_{p \in \beta \times \gamma} f(p)$ equals the iterated unconditional product $\prod'_{b \in \beta} \prod'_{c \in \gamma} f(b, c)$.

Multipliable.tprod_prod_uncurry theorem

 {f : β → γ → α} (h : Multipliable (Function.uncurry f)) (h₁ : ∀ b, Multipliable fun c ↦ f b c) :
  ∏' p : β × γ, uncurry f p = ∏' (b) (c), f b c

Full source

@[to_additive Summable.tsum_prod_uncurry]
protected theorem Multipliable.tprod_prod_uncurry {f : β → γ → α}
    (h : Multipliable (Function.uncurry f)) (h₁ : ∀ b, Multipliable fun c ↦ f b c) :
    ∏' p : β × γ, uncurry f p = ∏' (b) (c), f b c :=
  (h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm

Unconditional Product of Uncurried Function Equals Iterated Product: $\prod'_{(b,c)} f(b, c) = \prod'_b \prod'_c f(b, c)$

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid, and let $f : \beta \to \gamma \to \alpha$ be a function. If the uncurried function $\text{uncurry}\, f : \beta \times \gamma \to \alpha$ is multipliable, and for each $b \in \beta$, the function $c \mapsto f(b, c)$ is multipliable, then the unconditional product $\prod'_{(b,c)} f(b, c)$ equals the iterated unconditional product $\prod'_b \prod'_c f(b, c)$.

Multipliable.tprod_comm' theorem

 {f : β → γ → α} (h : Multipliable (Function.uncurry f)) (h₁ : ∀ b, Multipliable (f b))
  (h₂ : ∀ c, Multipliable fun b ↦ f b c) : ∏' (c) (b), f b c = ∏' (b) (c), f b c

Full source

@[to_additive]
protected theorem Multipliable.tprod_comm' {f : β → γ → α} (h : Multipliable (Function.uncurry f))
    (h₁ : ∀ b, Multipliable (f b)) (h₂ : ∀ c, Multipliable fun b ↦ f b c) :
    ∏' (c) (b), f b c = ∏' (b) (c), f b c := by
  rw [← h.tprod_prod_uncurry h₁, ← h.prod_symm.tprod_prod_uncurry h₂,
    ← (Equiv.prodComm γ β).tprod_eq (uncurry f)]
  rfl

Commutativity of Iterated Unconditional Products: $\prod'_c \prod'_b f(b, c) = \prod'_b \prod'_c f(b, c)$

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid, and let $f : \beta \to \gamma \to \alpha$ be a function. Suppose that: 1. The uncurried function $\text{uncurry}\, f : \beta \times \gamma \to \alpha$ is multipliable. 2. For each $b \in \beta$, the function $c \mapsto f(b, c)$ is multipliable. 3. For each $c \in \gamma$, the function $b \mapsto f(b, c)$ is multipliable. Then the iterated unconditional products satisfy $\prod'_{c \in \gamma} \prod'_{b \in \beta} f(b, c) = \prod'_{b \in \beta} \prod'_{c \in \gamma} f(b, c)$.

HasProd.of_sigma theorem

 {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α} (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b))
  (hg : HasProd g a) (h : CauchySeq (fun (s : Finset (Σ b : β, γ b)) ↦ ∏ i ∈ s, f i)) : HasProd f a

Full source

@[to_additive]
theorem HasProd.of_sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
    (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hg : HasProd g a)
    (h : CauchySeq (fun (s : Finset (Σ b : β, γ b)) ↦ ∏ i ∈ s, f i)) :
    HasProd f a := by
  classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop, ge_iff_le,
    le_eq_subset]
  intro u hu s
  rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
  obtain ⟨t0, st0, ht0⟩ : ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ s.image Sigma.fst ⊆ t0 := by
    have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
    exact (A.and (Ici_mem_atTop _)).exists
  have L : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop
      (𝓝 <| ∏ b ∈ t0, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finset_prod _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
    ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists
  obtain ⟨t, tv, st⟩ := this
  refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
  simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)

Product Convergence via Sigma-Type Decomposition

Informal description

Let $\gamma : \beta \to \text{Type}^*$ be a family of types indexed by $\beta$, and let $f : (\Sigma b : \beta, \gamma b) \to \alpha$ be a function. Suppose that: 1. For each $b \in \beta$, the function $c \mapsto f \langle b, c \rangle$ has product $g(b)$. 2. The function $g : \beta \to \alpha$ has product $a$. 3. The sequence of partial products $\prod_{i \in s} f(i)$, where $s$ ranges over finite subsets of $\Sigma b : \beta, \gamma b$, is a Cauchy sequence. Then the function $f$ has product $a$.

Multipliable.sigma_factor theorem

{γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f) (b : β) : Multipliable fun c ↦ f ⟨b, c⟩

Full source

@[to_additive]
theorem Multipliable.sigma_factor {γ : β → Type*} {f : (Σ b : β, γ b) → α}
    (ha : Multipliable f) (b : β) :
    Multipliable fun c ↦ f ⟨b, c⟩ :=
  ha.comp_injective sigma_mk_injective

Multipliability of Fiber Functions in Sigma Type

Informal description

Let $\gamma : \beta \to \text{Type}^*$ be a family of types indexed by $\beta$, and let $f : (\Sigma b : \beta, \gamma b) \to \alpha$ be a function. If $f$ is multipliable, then for any fixed $b \in \beta$, the function $c \mapsto f \langle b, c \rangle$ is multipliable.

Multipliable.sigma theorem

{γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f) : Multipliable fun b ↦ ∏' c, f ⟨b, c⟩

Full source

@[to_additive]
theorem Multipliable.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f) :
    Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ :=
  ha.sigma' fun b ↦ ha.sigma_factor b

Multipliability of Fiberwise Products in Sigma Type

Informal description

Let $\gamma : \beta \to \text{Type}$ be a family of types indexed by $\beta$, and let $f : (\Sigma b : \beta, \gamma b) \to \alpha$ be a function. If $f$ is multipliable, then the function $b \mapsto \prod'_{c} f \langle b, c \rangle$ is multipliable.

Multipliable.prod_factor theorem

{f : β × γ → α} (h : Multipliable f) (b : β) : Multipliable fun c ↦ f (b, c)

Full source

@[to_additive Summable.prod_factor]
theorem Multipliable.prod_factor {f : β × γ → α} (h : Multipliable f) (b : β) :
    Multipliable fun c ↦ f (b, c) :=
  h.comp_injective fun _ _ h ↦ (Prod.ext_iff.1 h).2

Multipliability of Fiber Functions in Product Type

Informal description

Let $f : \beta \times \gamma \to \alpha$ be a multipliable function. Then for any fixed $b \in \beta$, the function $c \mapsto f(b, c)$ is multipliable.

Multipliable.prod theorem

{f : β × γ → α} (h : Multipliable f) : Multipliable fun b ↦ ∏' c, f (b, c)

Full source

@[to_additive Summable.prod]
lemma Multipliable.prod {f : β × γ → α} (h : Multipliable f) :
    Multipliable fun b ↦ ∏' c, f (b, c) :=
  ((Equiv.sigmaEquivProd β γ).multipliable_iff.mpr h).sigma

Multipliability of Fiberwise Products in Cartesian Product Type

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid, and let $f : \beta \times \gamma \to \alpha$ be a multipliable function. Then for each $b \in \beta$, the function $c \mapsto f(b, c)$ is multipliable, and the function $b \mapsto \prod'_{c} f(b, c)$ is also multipliable.

HasProd.tprod_fiberwise theorem

 [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) : HasProd (fun c : γ ↦ ∏' b : g ⁻¹' { c }, f b) a

Full source

@[to_additive]
lemma HasProd.tprod_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) :
    HasProd (fun c : γ ↦ ∏' b : g ⁻¹' {c}, f b) a :=
  (((Equiv.sigmaFiberEquiv g).hasProd_iff).mpr hf).sigma <|
    fun _ ↦ ((hf.multipliable.subtype _).hasProd_iff).mpr rfl

Fiberwise Product Convergence Theorem in Hausdorff Spaces

Informal description

Let $\alpha$ be a Hausdorff topological space, $\beta$ and $\gamma$ index types, and $f : \beta \to \alpha$ a function. Suppose that: 1. The product of $f$ converges to $a \in \alpha$ (i.e., $\text{HasProd} f a$ holds), and 2. $g : \beta \to \gamma$ is any function partitioning $\beta$ into fibers over $\gamma$. Then the product of the fiberwise products $\prod'_{b \in g^{-1}\{c\}} f(b)$ converges to $a$ (i.e., $\text{HasProd} (c \mapsto \prod'_{b \in g^{-1}\{c\}} f(b)) a$ holds).

Multipliable.tprod_sigma theorem

{γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f) : ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩

Full source

@[to_additive]
protected theorem Multipliable.tprod_sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α}
    (ha : Multipliable f) : ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
  Multipliable.tprod_sigma' (fun b ↦ ha.sigma_factor b) ha

Sigma-Type Unconditional Product Decomposition: $\prod'_{p} f(p) = \prod'_{b,c} f \langle b, c \rangle$

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid, $\beta$ an index type, and $\gamma : \beta \to \text{Type}$ a family of types. Given a multipliable function $f : (\Sigma b : \beta, \gamma b) \to \alpha$, the unconditional product $\prod'_{p} f(p)$ equals the iterated unconditional product $\prod'_{b} \prod'_{c} f \langle b, c \rangle$.

Multipliable.tprod_prod theorem

{f : β × γ → α} (h : Multipliable f) : ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩

Full source

@[to_additive Summable.tsum_prod]
protected theorem Multipliable.tprod_prod {f : β × γ → α} (h : Multipliable f) :
    ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
  h.tprod_prod' h.prod_factor

Product Decomposition of Unconditional Product: $\prod'_{p} f(p) = \prod'_{b,c} f(b, c)$

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid and $f : \beta \times \gamma \to \alpha$ be a multipliable function. Then the unconditional product $\prod'_{p \in \beta \times \gamma} f(p)$ equals the iterated unconditional product $\prod'_{b \in \beta} \prod'_{c \in \gamma} f(b, c)$.

Multipliable.tprod_comm theorem

{f : β → γ → α} (h : Multipliable (Function.uncurry f)) : ∏' (c) (b), f b c = ∏' (b) (c), f b c

Full source

@[to_additive]
protected theorem Multipliable.tprod_comm {f : β → γ → α} (h : Multipliable (Function.uncurry f)) :
    ∏' (c) (b), f b c = ∏' (b) (c), f b c :=
  h.tprod_comm' h.prod_factor h.prod_symm.prod_factor

Commutativity of Iterated Unconditional Products: $\prod'_c \prod'_b f(b, c) = \prod'_b \prod'_c f(b, c)$

Informal description

Let $\alpha$ be a commutative topological multiplicative monoid and $f : \beta \to \gamma \to \alpha$ be a function such that the uncurried function $(b, c) \mapsto f(b, c)$ is multipliable. Then the iterated unconditional products satisfy $\prod'_{c \in \gamma} \prod'_{b \in \beta} f(b, c) = \prod'_{b \in \beta} \prod'_{c \in \gamma} f(b, c)$.

Pi.hasProd theorem

{f : ι → ∀ x, π x} {g : ∀ x, π x} : HasProd f g ↔ ∀ x, HasProd (fun i ↦ f i x) (g x)

Full source

@[to_additive]
theorem Pi.hasProd {f : ι → ∀ x, π x} {g : ∀ x, π x} :
    HasProdHasProd f g ↔ ∀ x, HasProd (fun i ↦ f i x) (g x) := by
  simp only [HasProd, tendsto_pi_nhds, prod_apply]

Pointwise Product Convergence Criterion for Indexed Families

Informal description

For a family of functions $f : \iota \to \prod_{x \in \alpha} \pi(x)$ and a function $g : \prod_{x \in \alpha} \pi(x)$, the product of $f$ converges to $g$ if and only if for every $x \in \alpha$, the product of the functions $\lambda i, f(i)(x)$ converges to $g(x)$.

Pi.multipliable theorem

{f : ι → ∀ x, π x} : Multipliable f ↔ ∀ x, Multipliable fun i ↦ f i x

Full source

@[to_additive]
theorem Pi.multipliable {f : ι → ∀ x, π x} : MultipliableMultipliable f ↔ ∀ x, Multipliable fun i ↦ f i x := by
  simp only [Multipliable, Pi.hasProd, Classical.skolem]

Multipliability Criterion for Pointwise Functions: $\prod$-Multipliability iff Componentwise Multipliability

Informal description

A function $f : \iota \to \prod_{x \in \alpha} \pi(x)$ is multipliable if and only if for every $x \in \alpha$, the function $\lambda i, f(i)(x)$ is multipliable.

tprod_apply theorem

[∀ x, T2Space (π x)] {f : ι → ∀ x, π x} {x : α} (hf : Multipliable f) : (∏' i, f i) x = ∏' i, f i x

Full source

@[to_additive]
theorem tprod_apply [∀ x, T2Space (π x)] {f : ι → ∀ x, π x} {x : α} (hf : Multipliable f) :
    (∏' i, f i) x = ∏' i, f i x :=
  (Pi.hasProd.mp hf.hasProd x).tprod_eq.symm

Pointwise Evaluation of Unconditional Product in Hausdorff Spaces

Informal description

Let $\{Y_x\}_{x \in \alpha}$ be a family of Hausdorff topological spaces and let $f : \iota \to \prod_{x \in \alpha} Y_x$ be a multipliable function. Then for any $x \in \alpha$, the evaluation of the unconditional product at $x$ equals the unconditional product of the evaluations: $$ \left(\prod'_{i} f_i\right)(x) = \prod'_{i} f_i(x). $$

HasSum.op theorem

(hf : HasSum f a) : HasSum (fun a ↦ op (f a)) (op a)

Full source

theorem HasSum.op (hf : HasSum f a) : HasSum (fun a ↦ op (f a)) (op a) :=
  (hf.map (@opAddEquiv α _) continuous_op :)

Sum Preservation under Multiplicative Opposite: $(\text{op} \circ f)$ has sum $\text{op}(a)$ if $f$ has sum $a$

Informal description

Given a function $f : \beta \to \alpha$ and an element $a \in \alpha$ such that $f$ has sum $a$, the function $\text{op} \circ f : \beta \to \alpha^\text{op}$ has sum $\text{op}(a)$ in the multiplicative opposite $\alpha^\text{op}$.

Summable.op theorem

(hf : Summable f) : Summable (op ∘ f)

Full source

theorem Summable.op (hf : Summable f) : Summable (opop ∘ f) :=
  hf.hasSum.op.summable

Summability Preservation under Multiplicative Opposite

Informal description

If a function $f : \beta \to \alpha$ is summable, then the composition $\text{op} \circ f : \beta \to \alpha^\text{op}$ is also summable, where $\text{op} : \alpha \to \alpha^\text{op}$ is the canonical embedding into the multiplicative opposite of $\alpha$.

HasSum.unop theorem

{f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} (hf : HasSum f a) : HasSum (fun a ↦ unop (f a)) (unop a)

Full source

theorem HasSum.unop {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} (hf : HasSum f a) :
    HasSum (fun a ↦ unop (f a)) (unop a) :=
  (hf.map (@opAddEquiv α _).symm continuous_unop :)

Sum Preservation under Unary Operation from Opposite to Original Space

Informal description

Let $\alpha$ be a type with an additive structure, and let $\alpha^\text{op}$ be its multiplicative opposite. Given a function $f : \beta \to \alpha^\text{op}$ and an element $a \in \alpha^\text{op}$, if $f$ has sum $a$ in $\alpha^\text{op}$, then the function $\text{unop} \circ f : \beta \to \alpha$ has sum $\text{unop}(a)$ in $\alpha$.

Summable.unop theorem

{f : β → αᵐᵒᵖ} (hf : Summable f) : Summable (unop ∘ f)

Full source

theorem Summable.unop {f : β → αᵐᵒᵖ} (hf : Summable f) : Summable (unopunop ∘ f) :=
  hf.hasSum.unop.summable

Summability under projection from multiplicative opposite to original space

Informal description

Let $\alpha$ be a type with a topological space structure and an additive commutative monoid structure, and let $\alpha^\text{op}$ be its multiplicative opposite. Given a function $f : \beta \to \alpha^\text{op}$, if $f$ is summable in $\alpha^\text{op}$, then the function $\text{unop} \circ f : \beta \to \alpha$ is summable in $\alpha$.

hasSum_op theorem

: HasSum (fun a ↦ op (f a)) (op a) ↔ HasSum f a

Full source

@[simp]
theorem hasSum_op : HasSumHasSum (fun a ↦ op (f a)) (op a) ↔ HasSum f a :=
  ⟨HasSum.unop, HasSum.op⟩

Equivalence of Summability in Original and Opposite Spaces: $\text{op} \circ f$ has sum $\text{op}(a)$ iff $f$ has sum $a$

Informal description

For a function $f : \beta \to \alpha$ and an element $a \in \alpha$, the function $\text{op} \circ f : \beta \to \alpha^\text{op}$ has sum $\text{op}(a)$ in the multiplicative opposite $\alpha^\text{op}$ if and only if $f$ has sum $a$ in $\alpha$.

hasSum_unop theorem

{f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} : HasSum (fun a ↦ unop (f a)) (unop a) ↔ HasSum f a

Full source

@[simp]
theorem hasSum_unop {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} :
    HasSumHasSum (fun a ↦ unop (f a)) (unop a) ↔ HasSum f a :=
  ⟨HasSum.op, HasSum.unop⟩

Sum Equivalence under Unary Operation from Opposite to Original Space

Informal description

For a function $f : \beta \to \alpha^\text{op}$ and an element $a \in \alpha^\text{op}$, the function $\text{unop} \circ f : \beta \to \alpha$ has sum $\text{unop}(a)$ if and only if $f$ has sum $a$ in $\alpha^\text{op}$.

summable_op theorem

: (Summable fun a ↦ op (f a)) ↔ Summable f

Full source

@[simp]
theorem summable_op : (Summable fun a ↦ op (f a)) ↔ Summable f :=
  ⟨Summable.unop, Summable.op⟩

Summability Equivalence under Multiplicative Opposite: $\text{op} \circ f$ is summable iff $f$ is summable

Informal description

For a function $f : \beta \to \alpha$, the composition $\text{op} \circ f : \beta \to \alpha^\text{op}$ is summable if and only if $f$ is summable in $\alpha$.

summable_unop theorem

{f : β → αᵐᵒᵖ} : (Summable fun a ↦ unop (f a)) ↔ Summable f

Full source

theorem summable_unop {f : β → αᵐᵒᵖ} : (Summable fun a ↦ unop (f a)) ↔ Summable f :=
  ⟨Summable.op, Summable.unop⟩

Summability Equivalence under Projection from Multiplicative Opposite

Informal description

For a function $f \colon \beta \to \alpha^\text{op}$ mapping into the multiplicative opposite of $\alpha$, the composition $\text{unop} \circ f \colon \beta \to \alpha$ is summable if and only if $f$ is summable in $\alpha^\text{op}$.

tsum_op theorem

[T2Space α] : ∑' x, op (f x) = op (∑' x, f x)

Full source

theorem tsum_op [T2Space α] :
    ∑' x, op (f x) = op (∑' x, f x) := by
  by_cases h : Summable f
  · exact h.hasSum.op.tsum_eq
  · have ho := summable_op.not.mpr h
    rw [tsum_eq_zero_of_not_summable h, tsum_eq_zero_of_not_summable ho, op_zero]

Sum of Opposites Equals Opposite of Sum in Hausdorff Spaces

Informal description

Let $\alpha$ be a Hausdorff topological space. For any function $f \colon \beta \to \alpha$, the sum of the multiplicative opposites $\sum'_{x} \text{op}(f(x))$ in $\alpha^\text{op}$ equals the multiplicative opposite of the sum $\text{op}\left(\sum'_{x} f(x)\right)$.

tsum_unop theorem

[T2Space α] {f : β → αᵐᵒᵖ} : ∑' x, unop (f x) = unop (∑' x, f x)

Full source

theorem tsum_unop [T2Space α] {f : β → αᵐᵒᵖ} :
    ∑' x, unop (f x) = unop (∑' x, f x) :=
  op_injective tsum_op.symm

Sum Projection from Multiplicative Opposite Equals Sum of Projections in Hausdorff Spaces

Informal description

Let $\alpha$ be a Hausdorff topological space and $f \colon \beta \to \alpha^\text{op}$ a function. The sum $\sum'_{x} \text{unop}(f(x))$ in $\alpha$ equals the projection of the sum $\text{unop}\left(\sum'_{x} f(x)\right)$ from $\alpha^\text{op}$ to $\alpha$.

HasSum.star theorem

(h : HasSum f a) : HasSum (fun b ↦ star (f b)) (star a)

Full source

theorem HasSum.star (h : HasSum f a) : HasSum (fun b ↦ star (f b)) (star a) := by
  simpa only using h.map (starAddEquiv : α ≃+ α) continuous_star

Star Operation Preserves Summability

Informal description

If a function $f$ has sum $a$ in a topological space with a continuous star operation, then the function $\lambda b, \star(f(b))$ has sum $\star(a)$.

Summable.star theorem

(hf : Summable f) : Summable fun b ↦ star (f b)

Full source

theorem Summable.star (hf : Summable f) : Summable fun b ↦ star (f b) :=
  hf.hasSum.star.summable

Summability under Star Operation

Informal description

If a function $f$ is summable in a topological space with a continuous star operation, then the function $\lambda b, \star(f(b))$ is also summable.

Summable.ofStar theorem

(hf : Summable fun b ↦ Star.star (f b)) : Summable f

Full source

theorem Summable.ofStar (hf : Summable fun b ↦ Star.star (f b)) : Summable f := by
  simpa only [star_star] using hf.star

Summability of Function Implies Summability under Star Operation

Informal description

If the function $\lambda b, \star(f(b))$ is summable in a topological space with a continuous star operation, then the function $f$ is also summable.

summable_star_iff theorem

: (Summable fun b ↦ star (f b)) ↔ Summable f

Full source

@[simp]
theorem summable_star_iff : (Summable fun b ↦ star (f b)) ↔ Summable f :=
  ⟨Summable.ofStar, Summable.star⟩

Summability under Star Operation is Equivalent to Summability of Original Function

Informal description

For a function $f$ in a topological space with a continuous star operation, the function $\lambda b, \star(f(b))$ is summable if and only if $f$ is summable.

summable_star_iff' theorem

: Summable (star f) ↔ Summable f

Full source

@[simp]
theorem summable_star_iff' : SummableSummable (star f) ↔ Summable f :=
  summable_star_iff

Summability under Star Operation is Equivalent to Summability of Original Function (Pointwise Version)

Informal description

For a function $f$ in a topological space with a continuous star operation, the function $\star \circ f$ is summable if and only if $f$ is summable.

tsum_star theorem

[T2Space α] : star (∑' b, f b) = ∑' b, star (f b)

Full source

theorem tsum_star [T2Space α] : star (∑' b, f b) = ∑' b, star (f b) := by
  by_cases hf : Summable f
  · exact hf.hasSum.star.tsum_eq.symm
  · rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt Summable.ofStar hf),
      star_zero]

Star-Sum Commutation in Hausdorff Spaces

Informal description

In a Hausdorff topological space $\alpha$ with a continuous star operation, the star of the sum of a family of elements $(f_b)_{b}$ is equal to the sum of the stars of the elements, i.e., \[ \star\left(\sum_{b} f_b\right) = \sum_{b} \star(f_b). \]