Mathlib.Topology.Algebra.InfiniteSum.Defs

Module docstring

{"# Infinite sum and product over a topological monoid

This file defines unconditionally convergent sums over a commutative topological additive monoid. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute convergence.

We also define unconditionally convergent products over a commutative topological multiplicative monoid.

Note: There are summable sequences which are not unconditionally convergent! The other way holds generally, see HasSum.tendsto_sum_nat.

Implementation notes

We say that a function f : β → α has an unconditional product of a if the function fun s : Finset β ↦ ∏ b ∈ s, f b converges to a on the atTop filter on Finset β. In other words, for every neighborhood U of a, there exists a finite set s : Finset β of indices such that ∏ b ∈ s', f b ∈ U for any finite set s' which is a superset of s.

This may yield some unexpected results. For example, according to this definition, the product ∏' n : ℕ, (1 : ℝ) / 2 unconditionally exists and is equal to 0. More strikingly, the product ∏' n : ℕ, (n : ℝ) unconditionally exists and is equal to 0, because one of its terms is 0 (even though the product of the remaining terms diverges). Users who would prefer that these products be considered not to exist can carry them out in the unit group ℝˣ rather than in ℝ.

References

Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)

HasProd definition

(f : β → α) (a : α) : Prop

Full source

/-- `HasProd f a` means that the (potentially infinite) product of the `f b` for `b : β` converges
to `a`.

The `atTop` filter on `Finset β` is the limit of all finite sets towards the entire type. So we take
the product over bigger and bigger sets. This product operation is invariant under reordering.

For the definition and many statements, `α` does not need to be a topological monoid. We only add
this assumption later, for the lemmas where it is relevant.

These are defined in an identical way to infinite sums (`HasSum`). For example, we say that
the function `ℕ → ℝ` sending `n` to `1 / 2` has a product of `0`, rather than saying that it does
not converge as some authors would. -/
@[to_additive "`HasSum f a` means that the (potentially infinite) sum of the `f b` for `b : β`
converges to `a`.

The `atTop` filter on `Finset β` is the limit of all finite sets towards the entire type. So we sum
up bigger and bigger sets. This sum operation is invariant under reordering. In particular,
the function `ℕ → ℝ` sending `n` to `(-1)^n / (n+1)` does not have a
sum for this definition, but a series which is absolutely convergent will have the correct sum.

This is based on Mario Carneiro's
[infinite sum `df-tsms` in Metamath](http://us.metamath.org/mpeuni/df-tsms.html).

For the definition and many statements, `α` does not need to be a topological monoid. We only add
this assumption later, for the lemmas where it is relevant."]
def HasProd (f : β → α) (a : α) : Prop :=
  Tendsto (fun s : Finset β ↦ ∏ b ∈ s, f b) atTop (𝓝 a)

Unconditional product convergence

Informal description

The product of a function $f : \beta \to \alpha$ has value $a$ if the finite partial products $\prod_{b \in s} f(b)$ converge to $a$ as the finite set $s \subseteq \beta$ grows to include all of $\beta$. More precisely, for every neighborhood $U$ of $a$, there exists a finite set $s \subseteq \beta$ such that for any finite superset $s' \supseteq s$, the product $\prod_{b \in s'} f(b)$ lies in $U$.

Multipliable definition

(f : β → α) : Prop

Full source

/-- `Multipliable f` means that `f` has some (infinite) product. Use `tprod` to get the value. -/
@[to_additive "`Summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value."]
def Multipliable (f : β → α) : Prop :=
  ∃ a, HasProd f a

Multipliable function

Informal description

A function $f : \beta \to \alpha$ is said to be multipliable if there exists some value $a \in \alpha$ such that the finite partial products $\prod_{b \in s} f(b)$ converge to $a$ as the finite set $s \subseteq \beta$ grows to include all of $\beta$. In other words, for every neighborhood $U$ of $a$, there exists a finite set $s \subseteq \beta$ such that for any finite superset $s' \supseteq s$, the product $\prod_{b \in s'} f(b)$ lies in $U$.

tprod definition

Full source

/-- `∏' i, f i` is the product of `f` if it exists and is unconditionally convergent,
or 1 otherwise. -/
@[to_additive "`∑' i, f i` is the sum of `f` if it exists and is unconditionally convergent,
or 0 otherwise."]
noncomputable irreducible_def tprod {β} (f : β → α) :=
  if h : Multipliable f then
  /- Note that the product might not be uniquely defined if the topology is not separated.
  When the multiplicative support of `f` is finite, we make the most reasonable choice to use the
  product over the multiplicative support. Otherwise, we choose arbitrarily an `a` satisfying
  `HasProd f a`. -/
    if (mulSupport f).Finite then finprod f
    else h.choose
  else 1

Unconditional product

Informal description

The unconditional product `∏' i, f i` of a function `f : β → α` over a commutative topological multiplicative monoid `α` is defined as the limit of the product over finite subsets of the domain if it exists and is unconditionally convergent, and is defined to be `1` otherwise. More precisely, if `f` is multipliable, then: - If the multiplicative support of `f` is finite, the product is taken over the support. - Otherwise, an arbitrary value satisfying the convergence condition is chosen. If `f` is not multipliable, the product is defined to be `1`.

tprod_def theorem

: eta_helper Eq✝ @tprod.{} @(delta% @definition✝)

Full source

/-- `∏' i, f i` is the product of `f` if it exists and is unconditionally convergent,
or 1 otherwise. -/
@[to_additive "`∑' i, f i` is the sum of `f` if it exists and is unconditionally convergent,
or 0 otherwise."]
noncomputable irreducible_def tprod {β} (f : β → α) :=
  if h : Multipliable f then
  /- Note that the product might not be uniquely defined if the topology is not separated.
  When the multiplicative support of `f` is finite, we make the most reasonable choice to use the
  product over the multiplicative support. Otherwise, we choose arbitrarily an `a` satisfying
  `HasProd f a`. -/
    if (mulSupport f).Finite then finprod f
    else h.choose
  else 1

Definition of Unconditional Product in Topological Monoid

Informal description

The unconditional product `∏' i, f i` of a function `f : β → α` over a commutative topological multiplicative monoid `α` is defined as follows: - If `f` is multipliable (i.e., the finite partial products converge to some limit `a`), then: - When the multiplicative support of `f` (the set where `f(x) ≠ 1`) is finite, the product is taken over this support - Otherwise, an arbitrary value satisfying the convergence condition is chosen - If `f` is not multipliable, the product is defined to be `1`

term∏'_,_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc tprod]
notation3 "∏' "(...)", "r:67:(scoped f => tprod f) => r

Unconditional product notation

Informal description

The notation `∏' i, f i` represents the unconditional product of the function `f` over its domain, defined as the limit of the product over finite subsets of the domain. Specifically, for a function `f : β → α` where `α` is a commutative topological multiplicative monoid, the unconditional product `∏' i, f i` is the value `a` such that for every neighborhood `U` of `a`, there exists a finite set `s` of indices such that for any finite superset `s'` of `s`, the product `∏ b ∈ s', f b` lies in `U`.

term∏'_,_.delab_app.tprod definition

: Delab✝

Full source

@[inherit_doc tprod]
notation3 "∏' "(...)", "r:67:(scoped f => tprod f) => r

Unconditional product notation

Informal description

The notation `∏' x, f x` represents the unconditional product of the function `f$ over its domain, defined as the limit of the product over finite subsets of the domain. Specifically, for a function `f : β → α` where `α$ is a commutative topological multiplicative monoid, the unconditional product `∏' x, f x` is the value `a$ such that for every neighborhood `U$ of `a$, there exists a finite set `s$ of indices such that for any finite superset `s'$ of `s$, the product `∏ b ∈ s', f b$ lies in `U$.

term∑'_,_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc tsum]
notation3 "∑' "(...)", "r:67:(scoped f => tsum f) => r

Unconditional sum notation

Informal description

The notation `∑' x, f x` represents the unconditional sum of the function `f` over its domain. This means that the sum converges to a limit regardless of the order of summation, and is defined as the limit of the finite partial sums `∑ x ∈ s, f x` as the finite set `s` grows to include all elements of the domain.

term∑'_,_.delab_app.tsum definition

: Delab✝

Full source

@[inherit_doc tsum]
notation3 "∑' "(...)", "r:67:(scoped f => tsum f) => r

Unconditional sum notation

Informal description

The notation `∑' x, f x` represents the unconditional sum of the function `f` over its domain, defined as the limit of the finite partial sums `∑ x ∈ s, f x` as the finite set `s` grows to include all elements of the domain.

HasProd.multipliable theorem

(h : HasProd f a) : Multipliable f

Full source

@[to_additive]
theorem HasProd.multipliable (h : HasProd f a) : Multipliable f :=
  ⟨a, h⟩

Existence of unconditional product implies multipliability

Informal description

If a function $f \colon \beta \to \alpha$ has an unconditional product converging to $a$, then $f$ is multipliable.

tprod_eq_one_of_not_multipliable theorem

(h : ¬Multipliable f) : ∏' b, f b = 1

Full source

@[to_additive]
theorem tprod_eq_one_of_not_multipliable (h : ¬Multipliable f) : ∏' b, f b = 1 := by
  simp [tprod_def, h]

Unconditional product equals one for non-multipliable functions

Informal description

If a function $f \colon \beta \to \alpha$ is not multipliable, then its unconditional product $\prod'_{b} f(b)$ equals $1$.

Function.Injective.hasProd_iff theorem

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

Full source

@[to_additive]
theorem Function.Injective.hasProd_iff {g : γ → β} (hg : Injective g)
    (hf : ∀ x, x ∉ Set.range g → f x = 1) : HasProdHasProd (f ∘ g) a ↔ HasProd f a := by
  simp only [HasProd, Tendsto, comp_apply, hg.map_atTop_finset_prod_eq hf]

Injective Function Preserves Product Convergence

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 product of $f \circ g$ converges to $a$ if and only if the product of $f$ converges to $a$.

hasProd_subtype_iff_of_mulSupport_subset theorem

{s : Set β} (hf : mulSupport f ⊆ s) : HasProd (f ∘ (↑) : s → α) a ↔ HasProd f a

Full source

@[to_additive]
theorem hasProd_subtype_iff_of_mulSupport_subset {s : Set β} (hf : mulSupportmulSupport f ⊆ s) :
    HasProdHasProd (f ∘ (↑) : s → α) a ↔ HasProd f a :=
  Subtype.coe_injective.hasProd_iff <| by simpa using mulSupport_subset_iff'.1 hf

Product convergence equivalence for functions with restricted support

Informal description

Let $f : \beta \to \alpha$ be a function with multiplicative support contained in a set $s \subseteq \beta$. Then the product of $f$ converges to $a$ if and only if the product of the restriction of $f$ to $s$ converges to $a$.

hasProd_fintype theorem

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

Full source

@[to_additive]
theorem hasProd_fintype [Fintype β] (f : β → α) : HasProd f (∏ b, f b) :=
  OrderTop.tendsto_atTop_nhds _

Unconditional Product Convergence for Finite Types

Informal description

For any finite type $\beta$ and any function $f \colon \beta \to \alpha$, the product $\prod_{b \in \beta} f(b)$ unconditionally converges to $\prod_{b \in \beta} f(b)$.

Finset.hasProd theorem

(s : Finset β) (f : β → α) : HasProd (f ∘ (↑) : (↑s : Set β) → α) (∏ b ∈ s, f b)

Full source

@[to_additive]
protected theorem Finset.hasProd (s : Finset β) (f : β → α) :
    HasProd (f ∘ (↑) : (↑s : Set β) → α) (∏ b ∈ s, f b) := by
  rw [← prod_attach]
  exact hasProd_fintype _

Unconditional Product Convergence for Finite Sets

Informal description

For any finite set $s \subseteq \beta$ and any function $f \colon \beta \to \alpha$, the product of $f$ restricted to $s$ converges unconditionally to the finite product $\prod_{b \in s} f(b)$. More precisely, the function $f \circ \iota \colon s \to \alpha$ (where $\iota$ is the inclusion map) has an unconditional product equal to $\prod_{b \in s} f(b)$.

hasProd_prod_of_ne_finset_one theorem

(hf : ∀ b ∉ s, f b = 1) : HasProd f (∏ b ∈ s, f b)

Full source

/-- If a function `f` is `1` outside of a finite set `s`, then it `HasProd` `∏ b ∈ s, f b`. -/
@[to_additive "If a function `f` vanishes outside of a finite set `s`, then it `HasSum`
`∑ b ∈ s, f b`."]
theorem hasProd_prod_of_ne_finset_one (hf : ∀ b ∉ s, f b = 1) :
    HasProd f (∏ b ∈ s, f b) :=
  (hasProd_subtype_iff_of_mulSupport_subset <| mulSupport_subset_iff'.2 hf).1 <| s.hasProd f

Unconditional Product Convergence for Functions with Finite Support: $\prod_{b \in s} f(b)$

Informal description

Let $f : \beta \to \alpha$ be a function such that $f(b) = 1$ for all $b \notin s$, where $s$ is a finite subset of $\beta$. Then the product of $f$ converges unconditionally to the finite product $\prod_{b \in s} f(b)$.

multipliable_of_ne_finset_one theorem

(hf : ∀ b ∉ s, f b = 1) : Multipliable f

Full source

@[to_additive]
theorem multipliable_of_ne_finset_one (hf : ∀ b ∉ s, f b = 1) : Multipliable f :=
  (hasProd_prod_of_ne_finset_one hf).multipliable

Multipliability of Functions with Finite Support

Informal description

Let $f : \beta \to \alpha$ be a function such that $f(b) = 1$ for all $b \notin s$, where $s$ is a finite subset of $\beta$. Then $f$ is multipliable.

Multipliable.hasProd theorem

(ha : Multipliable f) : HasProd f (∏' b, f b)

Full source

@[to_additive]
theorem Multipliable.hasProd (ha : Multipliable f) : HasProd f (∏' b, f b) := by
  simp only [tprod_def, ha, dite_true]
  by_cases H : (mulSupport f).Finite
  · simp [H, hasProd_prod_of_ne_finset_one, finprod_eq_prod]
  · simpa [H] using ha.choose_spec

Multipliability Implies Product Convergence to Unconditional Product

Informal description

If a function $f : \beta \to \alpha$ is multipliable (i.e., its finite partial products converge unconditionally), then it has a product equal to the unconditional product $\prod'_{b} f(b)$.

HasProd.unique theorem

{a₁ a₂ : α} [T2Space α] : HasProd f a₁ → HasProd f a₂ → a₁ = a₂

Full source

@[to_additive]
theorem HasProd.unique {a₁ a₂ : α} [T2Space α] : HasProd f a₁ → HasProd f a₂ → a₁ = a₂ := by
  classical exact tendsto_nhds_unique

Uniqueness of Unconditional Products in Hausdorff Spaces

Informal description

Let $\alpha$ be a Hausdorff space and $f : \beta \to \alpha$ a function. If $f$ has unconditional products converging to both $a_1$ and $a_2$ in $\alpha$, then $a_1 = a_2$.

HasProd.tprod_eq theorem

(ha : HasProd f a) : ∏' b, f b = a

Full source

@[to_additive]
theorem HasProd.tprod_eq (ha : HasProd f a) : ∏' b, f b = a :=
  (Multipliable.hasProd ⟨a, ha⟩).unique ha

Unconditional Product Equals Limit Value

Informal description

If a function $f : \beta \to \alpha$ has an unconditional product converging to $a$ in a topological monoid $\alpha$, then the unconditional product $\prod'_{b} f(b)$ is equal to $a$.

Multipliable.hasProd_iff theorem

(h : Multipliable f) : HasProd f a ↔ ∏' b, f b = a

Full source

@[to_additive]
theorem Multipliable.hasProd_iff (h : Multipliable f) : HasProdHasProd f a ↔ ∏' b, f b = a :=
  Iff.intro HasProd.tprod_eq fun eq ↦ eq ▸ h.hasProd

Characterization of Unconditional Product Convergence for Multipliable Functions

Informal description

Let $f : \beta \to \alpha$ be a multipliable function in a commutative topological multiplicative monoid $\alpha$. Then $f$ has an unconditional product converging to $a$ if and only if the unconditional product $\prod'_{b} f(b)$ equals $a$.