Mathlib.Topology.Algebra.InfiniteSum.Order

hasProd_le_of_prod_le theorem

[ClosedIicTopology α] (hf : HasProd f a) (h : ∀ s, ∏ i ∈ s, f i ≤ c) : a ≤ c

Full source

@[to_additive]
lemma hasProd_le_of_prod_le [ClosedIicTopology α]
    (hf : HasProd f a) (h : ∀ s, ∏ i ∈ s, f i ≤ c) : a ≤ c :=
  le_of_tendsto' hf h

Infinite Product Bound Under Finite Product Constraints

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. Given a function $f : \beta \to \alpha$ and elements $a, c \in \alpha$, if $f$ has product $a$ (i.e., the infinite product $\prod f$ converges to $a$) and for every finite subset $s \subseteq \beta$ the finite product $\prod_{i \in s} f(i) \leq c$, then $a \leq c$.

le_hasProd_of_le_prod theorem

[ClosedIciTopology α] (hf : HasProd f a) (h : ∀ s, c ≤ ∏ i ∈ s, f i) : c ≤ a

Full source

@[to_additive]
theorem le_hasProd_of_le_prod [ClosedIciTopology α]
    (hf : HasProd f a) (h : ∀ s, c ≤ ∏ i ∈ s, f i) : c ≤ a :=
  ge_of_tendsto' hf h

Lower bound preservation for infinite products in `ClosedIciTopology` spaces

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. Given a function $f : \beta \to \alpha$ and an element $c \in \alpha$, if the product of $f$ converges to $a$ and for every finite subset $s \subseteq \beta$ we have $c \leq \prod_{i \in s} f(i)$, then $c \leq a$.

Multipliable.tprod_le_of_prod_range_le theorem

 [ClosedIicTopology α] {f : ℕ → α} (hf : Multipliable f) (h : ∀ n, ∏ i ∈ range n, f i ≤ c) : ∏' n, f n ≤ c

Full source

@[to_additive]
protected theorem Multipliable.tprod_le_of_prod_range_le [ClosedIicTopology α] {f : ℕ → α}
    (hf : Multipliable f) (h : ∀ n, ∏ i ∈ range n, f i ≤ c) : ∏' n, f n ≤ c :=
  le_of_tendsto' hf.hasProd.tendsto_prod_nat h

Unconditional Product Bound via Finite Partial Products in `ClosedIicTopology` Spaces

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. Given a multipliable function $f : \mathbb{N} \to \alpha$ and an element $c \in \alpha$, if for every natural number $n$ the finite product $\prod_{i \in \{0, \dots, n-1\}} f(i) \leq c$, then the unconditional product $\prod'_{n} f(n) \leq c$.

hasProd_le theorem

(h : ∀ i, f i ≤ g i) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂

Full source

@[to_additive]
theorem hasProd_le (h : ∀ i, f i ≤ g i) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂ :=
  le_of_tendsto_of_tendsto' hf hg fun _ ↦ prod_le_prod' fun i _ ↦ h i

Comparison of Infinite Products in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. Given two functions $f, g : \beta \to \alpha$ such that $f(i) \leq g(i)$ for all $i \in \beta$, if the product of $f$ converges to $a_1$ and the product of $g$ converges to $a_2$, then $a_1 \leq a_2$.

hasProd_mono theorem

(hf : HasProd f a₁) (hg : HasProd g a₂) (h : f ≤ g) : a₁ ≤ a₂

Full source

@[to_additive]
theorem hasProd_mono (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f ≤ g) : a₁ ≤ a₂ :=
  hasProd_le h hf hg

Monotonicity of Infinite Products in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. Given two functions $f, g : \beta \to \alpha$ such that $f(i) \leq g(i)$ for all $i \in \beta$, if the product of $f$ converges to $a_1$ and the product of $g$ converges to $a_2$, then $a_1 \leq a_2$.

hasProd_le_inj theorem

 {g : κ → α} (e : ι → κ) (he : Injective e) (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c) (h : ∀ i, f i ≤ g (e i))
  (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂

Full source

@[to_additive]
theorem hasProd_le_inj {g : κ → α} (e : ι → κ) (he : Injective e)
    (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : HasProd f a₁)
    (hg : HasProd g a₂) : a₁ ≤ a₂ := by
  rw [← hasProd_extend_one he] at hf
  refine hasProd_le (fun c ↦ ?_) hf hg
  obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
  · rw [he.extend_apply]
    exact h _
  · rw [extend_apply' _ _ _ h]
    exact hs _ h

Comparison of Infinite Products via Injective Mapping in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. Given two functions $f : \iota \to \alpha$ and $g : \kappa \to \alpha$, and an injective function $e : \iota \to \kappa$ such that: 1. For all $c \in \kappa$ not in the range of $e$, $1 \leq g(c)$, 2. For all $i \in \iota$, $f(i) \leq g(e(i))$, if the product of $f$ converges to $a_1$ and the product of $g$ converges to $a_2$, then $a_1 \leq a_2$.

Multipliable.tprod_le_tprod_of_inj theorem

 {g : κ → α} (e : ι → κ) (he : Injective e) (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c) (h : ∀ i, f i ≤ g (e i))
  (hf : Multipliable f) (hg : Multipliable g) : tprod f ≤ tprod g

Full source

@[to_additive]
protected theorem Multipliable.tprod_le_tprod_of_inj {g : κ → α} (e : ι → κ) (he : Injective e)
    (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : Multipliable f)
    (hg : Multipliable g) : tprod f ≤ tprod g :=
  hasProd_le_inj _ he hs h hf.hasProd hg.hasProd

Comparison of Unconditional Products via Injective Mapping in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. Given two functions $f : \iota \to \alpha$ and $g : \kappa \to \alpha$, and an injective function $e : \iota \to \kappa$ such that: 1. For all $c \in \kappa$ not in the range of $e$, $1 \leq g(c)$, 2. For all $i \in \iota$, $f(i) \leq g(e(i))$, if $f$ and $g$ are multipliable, then the unconditional product of $f$ is less than or equal to the unconditional product of $g$, i.e., \[ \prod'_{i} f(i) \leq \prod'_{c} g(c). \]

Multipliable.tprod_subtype_le theorem

 {κ γ : Type*} [CommGroup γ] [PartialOrder γ] [IsOrderedMonoid γ] [UniformSpace γ] [IsUniformGroup γ]
  [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ a : κ, 1 ≤ f a) (hf : Multipliable f) :
  (∏' (b : β), f b) ≤ (∏' (a : κ), f a)

Full source

@[to_additive]
protected lemma Multipliable.tprod_subtype_le {κ γ : Type*} [CommGroup γ] [PartialOrder γ]
    [IsOrderedMonoid γ] [UniformSpace γ] [IsUniformGroup γ] [OrderClosedTopology γ]
    [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ a : κ, 1 ≤ f a) (hf : Multipliable f) :
    (∏' (b : β), f b) ≤ (∏' (a : κ), f a) := by
  apply Multipliable.tprod_le_tprod_of_inj _
    (Subtype.coe_injective)
    (by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, h, implies_true])
    (by simp only [le_refl, Subtype.forall, implies_true])
    (by apply hf.subtype)
  apply hf

Subset Product Inequality for Unconditional Products in Ordered Groups

Informal description

Let $\gamma$ be a complete, partially ordered commutative group with an order-closed topology and uniform group structure. Given a function $f : \kappa \to \gamma$ such that $1 \leq f(a)$ for all $a \in \kappa$, and a subset $\beta \subseteq \kappa$, if $f$ is multipliable, then the unconditional product over $\beta$ is less than or equal to the unconditional product over $\kappa$, i.e., \[ \prod'_{b \in \beta} f(b) \leq \prod'_{a \in \kappa} f(a). \]

prod_le_hasProd theorem

(s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i) (hf : HasProd f a) : ∏ i ∈ s, f i ≤ a

Full source

@[to_additive]
theorem prod_le_hasProd (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i) (hf : HasProd f a) :
    ∏ i ∈ s, f i ≤ a :=
  ge_of_tendsto hf (eventually_atTop.2
    ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst fun i _ hbs ↦ hs i hbs⟩)

Finite product bound for convergent infinite products in ordered monoids

Informal description

Let $\alpha$ be an ordered commutative monoid, and let $f : \iota \to \alpha$ be a function such that $1 \leq f(i)$ for all $i \notin s$, where $s$ is a finite subset of $\iota$. If the infinite product of $f$ converges to $a \in \alpha$, then the finite product of $f$ over $s$ is less than or equal to $a$, i.e., \[ \prod_{i \in s} f(i) \leq a. \]

isLUB_hasProd theorem

(h : ∀ i, 1 ≤ f i) (hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Full source

@[to_additive]
theorem isLUB_hasProd (h : ∀ i, 1 ≤ f i) (hf : HasProd f a) :
    IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a := by
  classical
  exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

Least Upper Bound Property of Convergent Products in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f : \iota \to \alpha$ be a function such that $1 \leq f(i)$ for all $i \in \iota$. If the product of $f$ converges to $a \in \alpha$, then $a$ is the least upper bound of the set of all finite partial products $\prod_{i \in s} f(i)$, where $s$ ranges over all finite subsets of $\iota$.

le_hasProd theorem

(hf : HasProd f a) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) : f i ≤ a

Full source

@[to_additive]
theorem le_hasProd (hf : HasProd f a) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) : f i ≤ a :=
  calc
    f i = ∏ i ∈ {i}, f i := by rw [prod_singleton]
    _ ≤ a := prod_le_hasProd _ (by simpa) hf

Elementwise bound in convergent products: $f(i) \leq a$ under non-negativity conditions

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f : \iota \to \alpha$ be a function. If the product of $f$ converges to $a \in \alpha$, and for some index $i \in \iota$ we have $1 \leq f(j)$ for all $j \neq i$, then $f(i) \leq a$.

lt_hasProd theorem

 [MulRightStrictMono α] (hf : HasProd f a) (i : ι) (hi : ∀ (j : ι), j ≠ i → 1 ≤ f j) (j : ι) (hij : j ≠ i)
  (hj : 1 < f j) : f i < a

Full source

@[to_additive]
theorem lt_hasProd [MulRightStrictMono α] (hf : HasProd f a) (i : ι)
    (hi : ∀ (j : ι), j ≠ i → 1 ≤ f j) (j : ι) (hij : j ≠ i) (hj : 1 < f j) :
    f i < a := by
  classical
  calc
    f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
    _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
    _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf

Strict elementwise bound in convergent products: $f(i) < a$ under positivity conditions

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology and right-strictly monotone multiplication. Suppose $f : \iota \to \alpha$ is a function whose product converges to $a \in \alpha$. If for some index $i \in \iota$ we have: 1. $1 \leq f(j)$ for all $j \neq i$, 2. There exists $j \neq i$ with $1 < f(j)$, then $f(i) < a$.

Multipliable.prod_le_tprod theorem

 {f : ι → α} (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i) (hf : Multipliable f) : ∏ i ∈ s, f i ≤ ∏' i, f i

Full source

@[to_additive]
protected theorem Multipliable.prod_le_tprod {f : ι → α} (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i)
    (hf : Multipliable f) : ∏ i ∈ s, f i ≤ ∏' i, f i :=
  prod_le_hasProd s hs hf.hasProd

Finite Product Bound for Multipliable Functions in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid, and let $f : \iota \to \alpha$ be a multipliable function such that $1 \leq f(i)$ for all $i \notin s$, where $s$ is a finite subset of $\iota$. Then the finite product of $f$ over $s$ is less than or equal to the unconditional product of $f$, i.e., \[ \prod_{i \in s} f(i) \leq \prod'_{i} f(i). \]

Multipliable.le_tprod theorem

(hf : Multipliable f) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) : f i ≤ ∏' i, f i

Full source

@[to_additive]
protected theorem Multipliable.le_tprod (hf : Multipliable f) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) :
    f i ≤ ∏' i, f i :=
  le_hasProd hf.hasProd i hb

Elementwise bound in unconditional products: $f(i) \leq \prod' f$ under non-negativity conditions

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f : \iota \to \alpha$ be a multipliable function. If for some index $i \in \iota$ we have $1 \leq f(j)$ for all $j \neq i$, then $f(i) \leq \prod'_{i} f(i)$.

Multipliable.tprod_le_tprod theorem

(h : ∀ i, f i ≤ g i) (hf : Multipliable f) (hg : Multipliable g) : ∏' i, f i ≤ ∏' i, g i

Full source

@[to_additive]
protected theorem Multipliable.tprod_le_tprod (h : ∀ i, f i ≤ g i) (hf : Multipliable f)
    (hg : Multipliable g) : ∏' i, f i ≤ ∏' i, g i :=
  hasProd_le h hf.hasProd hg.hasProd

Comparison of Unconditional Products in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f, g : \beta \to \alpha$ be functions such that $f(i) \leq g(i)$ for all $i \in \beta$. If both $f$ and $g$ are multipliable, then the unconditional product of $f$ is less than or equal to the unconditional product of $g$, i.e., \[ \prod'_{i} f(i) \leq \prod'_{i} g(i). \]

Multipliable.tprod_mono theorem

(hf : Multipliable f) (hg : Multipliable g) (h : f ≤ g) : ∏' n, f n ≤ ∏' n, g n

Full source

@[to_additive (attr := mono)]
protected theorem Multipliable.tprod_mono (hf : Multipliable f) (hg : Multipliable g) (h : f ≤ g) :
    ∏' n, f n ≤ ∏' n, g n :=
  hf.tprod_le_tprod h hg

Monotonicity of Unconditional Products in Ordered Monoids

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f, g : \beta \to \alpha$ be multipliable functions such that $f(i) \leq g(i)$ for all $i \in \beta$. Then the unconditional product of $f$ is less than or equal to the unconditional product of $g$, i.e., \[ \prod'_{i} f(i) \leq \prod'_{i} g(i). \]

Multipliable.tprod_le_of_prod_le theorem

(hf : Multipliable f) (h : ∀ s, ∏ i ∈ s, f i ≤ a₂) : ∏' i, f i ≤ a₂

Full source

@[to_additive]
protected theorem Multipliable.tprod_le_of_prod_le (hf : Multipliable f)
    (h : ∀ s, ∏ i ∈ s, f i ≤ a₂) : ∏' i, f i ≤ a₂ :=
  hasProd_le_of_prod_le hf.hasProd h

Infinite Product Bound Under Finite Product Constraints

Informal description

Let $\alpha$ be a topological space with a partial order and closed lower interval topology. Given a multipliable function $f : \beta \to \alpha$ and an element $a_2 \in \alpha$, if for every finite subset $s \subseteq \beta$ the finite product $\prod_{i \in s} f(i) \leq a_2$, then the unconditional product $\prod'_{i} f(i) \leq a_2$.

tprod_le_of_prod_le' theorem

(ha₂ : 1 ≤ a₂) (h : ∀ s, ∏ i ∈ s, f i ≤ a₂) : ∏' i, f i ≤ a₂

Full source

@[to_additive]
theorem tprod_le_of_prod_le' (ha₂ : 1 ≤ a₂) (h : ∀ s, ∏ i ∈ s, f i ≤ a₂) : ∏' i, f i ≤ a₂ := by
  by_cases hf : Multipliable f
  · exact hf.tprod_le_of_prod_le h
  · rw [tprod_eq_one_of_not_multipliable hf]
    exact ha₂

Unconditional product bound under finite product constraints with lower bound condition

Informal description

Let $\alpha$ be a topological space with a partial order and order-closed topology, and let $f : \beta \to \alpha$ be a function. If $1 \leq a_2$ and for every finite subset $s \subseteq \beta$ the finite product $\prod_{i \in s} f(i) \leq a_2$, then the unconditional product $\prod'_{i} f(i) \leq a_2$.

HasProd.one_le theorem

(h : ∀ i, 1 ≤ g i) (ha : HasProd g a) : 1 ≤ a

Full source

@[to_additive]
theorem HasProd.one_le (h : ∀ i, 1 ≤ g i) (ha : HasProd g a) : 1 ≤ a :=
  hasProd_le h hasProd_one ha

Lower Bound for Infinite Product of Elements Greater Than One

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. Given a function $g : \beta \to \alpha$ such that $1 \leq g(i)$ for all $i \in \beta$, if the product of $g$ converges to $a$, then $1 \leq a$.

HasProd.le_one theorem

(h : ∀ i, g i ≤ 1) (ha : HasProd g a) : a ≤ 1

Full source

@[to_additive]
theorem HasProd.le_one (h : ∀ i, g i ≤ 1) (ha : HasProd g a) : a ≤ 1 :=
  hasProd_le h ha hasProd_one

Upper Bound for Infinite Product of Elements Bounded by One

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. Given a function $g : \beta \to \alpha$ such that $g(i) \leq 1$ for all $i \in \beta$, if the product of $g$ converges to $a$, then $a \leq 1$.

one_le_tprod theorem

(h : ∀ i, 1 ≤ g i) : 1 ≤ ∏' i, g i

Full source

@[to_additive tsum_nonneg]
theorem one_le_tprod (h : ∀ i, 1 ≤ g i) : 1 ≤ ∏' i, g i := by
  by_cases hg : Multipliable g
  · exact hg.hasProd.one_le h
  · rw [tprod_eq_one_of_not_multipliable hg]

Lower Bound for Unconditional Product of Elements Greater Than One

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. For any function $g \colon \beta \to \alpha$ such that $1 \leq g(i)$ for all $i \in \beta$, the unconditional product $\prod'_{i} g(i)$ satisfies $1 \leq \prod'_{i} g(i)$.

tprod_le_one theorem

(h : ∀ i, f i ≤ 1) : ∏' i, f i ≤ 1

Full source

@[to_additive]
theorem tprod_le_one (h : ∀ i, f i ≤ 1) : ∏' i, f i ≤ 1 := by
  by_cases hf : Multipliable f
  · exact hf.hasProd.le_one h
  · rw [tprod_eq_one_of_not_multipliable hf]

Upper bound for unconditional product of elements bounded by one

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology. Given a function $f \colon \beta \to \alpha$ such that $f(i) \leq 1$ for all $i \in \beta$, the unconditional product $\prod'_{i} f(i)$ satisfies $\prod'_{i} f(i) \leq 1$.

hasProd_one_iff_of_one_le theorem

(hf : ∀ i, 1 ≤ f i) : HasProd f 1 ↔ f = 1

Full source

@[to_additive]
theorem hasProd_one_iff_of_one_le (hf : ∀ i, 1 ≤ f i) : HasProdHasProd f 1 ↔ f = 1 := by
  refine ⟨fun hf' ↦ ?_, ?_⟩
  · ext i
    exact (hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j)
  · rintro rfl
    exact hasProd_one

Convergence to One in Ordered Monoids: $\prod f = 1 \leftrightarrow f \equiv 1$ under non-negativity

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f \colon \beta \to \alpha$ be a function such that $1 \leq f(i)$ for all $i \in \beta$. Then the product of $f$ converges to $1$ if and only if $f$ is identically equal to the constant function $1$.

hasProd_lt theorem

(h : f ≤ g) (hi : f i < g i) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ < a₂

Full source

@[to_additive]
theorem hasProd_lt (h : f ≤ g) (hi : f i < g i) (hf : HasProd f a₁) (hg : HasProd g a₂) :
    a₁ < a₂ := by
  classical
  have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
  have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
  simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this

Strict Comparison of Infinite Products in Ordered Monoids: $f \leq g$ and $f(i) < g(i)$ implies $\prod f < \prod g$

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f, g : \beta \to \alpha$ be functions such that $f \leq g$ (i.e., $f(i) \leq g(i)$ for all $i \in \beta$) and $f(i) < g(i)$ for some $i \in \beta$. If the product of $f$ converges to $a_1$ and the product of $g$ converges to $a_2$, then $a_1 < a_2$.

hasProd_strict_mono theorem

(hf : HasProd f a₁) (hg : HasProd g a₂) (h : f < g) : a₁ < a₂

Full source

@[to_additive (attr := mono)]
theorem hasProd_strict_mono (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f < g) : a₁ < a₂ :=
  let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  hasProd_lt hle hi hf hg

Strict Monotonicity of Infinite Products in Ordered Monoids: $f < g$ implies $\prod f < \prod g$

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f, g : \beta \to \alpha$ be functions such that $f < g$ (i.e., $f(i) \leq g(i)$ for all $i \in \beta$ and $f(i) < g(i)$ for some $i \in \beta$). If the product of $f$ converges to $a_1$ and the product of $g$ converges to $a_2$, then $a_1 < a_2$.

Multipliable.tprod_lt_tprod theorem

(h : f ≤ g) (hi : f i < g i) (hf : Multipliable f) (hg : Multipliable g) : ∏' n, f n < ∏' n, g n

Full source

@[to_additive]
protected theorem Multipliable.tprod_lt_tprod (h : f ≤ g) (hi : f i < g i) (hf : Multipliable f)
    (hg : Multipliable g) : ∏' n, f n < ∏' n, g n :=
  hasProd_lt h hi hf.hasProd hg.hasProd

Strict Inequality of Unconditional Products: $f \leq g$ and $f(i) < g(i)$ implies $\prod' f < \prod' g$

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f, g : \beta \to \alpha$ be functions such that $f \leq g$ (i.e., $f(i) \leq g(i)$ for all $i \in \beta$) and $f(i) < g(i)$ for some $i \in \beta$. If $f$ and $g$ are multipliable, then the unconditional product of $f$ is strictly less than the unconditional product of $g$, i.e., $\prod'_{n} f(n) < \prod'_{n} g(n)$.

Multipliable.tprod_strict_mono theorem

(hf : Multipliable f) (hg : Multipliable g) (h : f < g) : ∏' n, f n < ∏' n, g n

Full source

@[to_additive (attr := mono)]
protected theorem Multipliable.tprod_strict_mono (hf : Multipliable f) (hg : Multipliable g)
    (h : f < g) : ∏' n, f n < ∏' n, g n :=
  let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  hf.tprod_lt_tprod hle hi hg

Strict Monotonicity of Unconditional Products: $f < g$ implies $\prod' f < \prod' g$

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $f, g : \beta \to \alpha$ be multipliable functions such that $f < g$ (i.e., $f(i) \leq g(i)$ for all $i \in \beta$ and $f(i) < g(i)$ for some $i \in \beta$). Then the unconditional product of $f$ is strictly less than the unconditional product of $g$, i.e., $\prod'_{n} f(n) < \prod'_{n} g(n)$.

Multipliable.one_lt_tprod theorem

(hsum : Multipliable g) (hg : ∀ i, 1 ≤ g i) (i : ι) (hi : 1 < g i) : 1 < ∏' i, g i

Full source

@[to_additive Summable.tsum_pos]
protected theorem Multipliable.one_lt_tprod (hsum : Multipliable g) (hg : ∀ i, 1 ≤ g i) (i : ι)
    (hi : 1 < g i) : 1 < ∏' i, g i := by
  rw [← tprod_one]
  exact multipliable_one.tprod_lt_tprod hg hi hsum

Strict lower bound for unconditional product: $1 < \prod' g$ when $1 < g(i)$ for some $i$

Informal description

Let $\alpha$ be an ordered commutative monoid with order-closed topology, and let $g : \iota \to \alpha$ be a multipliable function such that $1 \leq g(i)$ for all $i \in \iota$. If there exists an index $i \in \iota$ such that $1 < g(i)$, then the unconditional product satisfies $1 < \prod'_{i} g(i)$.

le_hasProd' theorem

(hf : HasProd f a) (i : ι) : f i ≤ a

Full source

@[to_additive]
theorem le_hasProd' (hf : HasProd f a) (i : ι) : f i ≤ a :=
  le_hasProd hf i fun _ _ ↦ one_le _

Elementwise bound in convergent products: $f(i) \leq a$

Informal description

Let $\alpha$ be a topological space with an order-closed topology and a partial order, and let $f : \iota \to \alpha$ be a function. If the product of $f$ converges to $a \in \alpha$, then for any index $i \in \iota$, we have $f(i) \leq a$.

Multipliable.le_tprod' theorem

(hf : Multipliable f) (i : ι) : f i ≤ ∏' i, f i

Full source

@[to_additive]
protected theorem Multipliable.le_tprod' (hf : Multipliable f) (i : ι) : f i ≤ ∏' i, f i :=
  hf.le_tprod i fun _ _ ↦ one_le _

Elementwise Bound in Unconditional Products: $f(i) \leq \prod' f$

Informal description

Let $\alpha$ be an ordered commutative monoid with an order-closed topology, and let $f : \iota \to \alpha$ be a multipliable function. For any index $i \in \iota$, the value $f(i)$ is less than or equal to the unconditional product $\prod'_{i} f(i)$.

hasProd_one_iff theorem

: HasProd f 1 ↔ ∀ x, f x = 1

Full source

@[to_additive]
theorem hasProd_one_iff : HasProdHasProd f 1 ↔ ∀ x, f x = 1 :=
  (hasProd_one_iff_of_one_le fun _ ↦ one_le _).trans funext_iff

Convergence to One in Ordered Monoids: $\prod f = 1 \leftrightarrow f \equiv 1$

Informal description

Let $\alpha$ be a topological space with an order-closed topology and a partial order, and let $f : \beta \to \alpha$ be a function. The product of $f$ converges to $1$ if and only if $f(x) = 1$ for all $x \in \beta$.

Multipliable.tprod_eq_one_iff theorem

(hf : Multipliable f) : ∏' i, f i = 1 ↔ ∀ x, f x = 1

Full source

@[to_additive]
protected theorem Multipliable.tprod_eq_one_iff (hf : Multipliable f) :
    ∏' i, f i∏' i, f i = 1 ↔ ∀ x, f x = 1 := by
  rw [← hasProd_one_iff, hf.hasProd_iff]

Characterization of Unconditional Product Being One: $\prod' f = 1 \leftrightarrow f \equiv 1$

Informal description

Let $\alpha$ be a topological space with an order-closed topology and a partial order, and let $f : \beta \to \alpha$ be a multipliable function. The unconditional product $\prod'_{x} f(x)$ equals $1$ if and only if $f(x) = 1$ for all $x \in \beta$.

Multipliable.tprod_ne_one_iff theorem

(hf : Multipliable f) : ∏' i, f i ≠ 1 ↔ ∃ x, f x ≠ 1

Full source

@[to_additive]
protected theorem Multipliable.tprod_ne_one_iff (hf : Multipliable f) :
    ∏' i, f i∏' i, f i ≠ 1∏' i, f i ≠ 1 ↔ ∃ x, f x ≠ 1 := by
  rw [Ne, hf.tprod_eq_one_iff, not_forall]

Characterization of Unconditional Product Not Being One: $\prod' f \neq 1 \leftrightarrow \exists x, f(x) \neq 1$

Informal description

Let $\alpha$ be a topological space with an order-closed topology and a partial order, and let $f : \beta \to \alpha$ be a multipliable function. The unconditional product $\prod'_{x} f(x)$ is not equal to $1$ if and only if there exists some $x \in \beta$ such that $f(x) \neq 1$.

isLUB_hasProd' theorem

(hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Full source

@[to_additive]
theorem isLUB_hasProd' (hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a := by
  classical
  exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

Least Upper Bound Property of Convergent Infinite Products in Ordered Monoids

Informal description

Let $\alpha$ be a commutative monoid with a linear order and order topology, and let $f : \iota \to \alpha$ be a function. If the infinite product $\prod_{i \in \iota} f(i)$ converges to $a \in \alpha$ (i.e., $\text{HasProd}(f, a)$ holds), then $a$ is the least upper bound of the set of finite partial products $\left\{ \prod_{i \in s} f(i) \mid s \text{ finite subset of } \iota \right\}$.

hasProd_of_isLUB_of_one_le theorem

 [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α)
  (h : ∀ i, 1 ≤ f i) (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) i) : HasProd f i

Full source

@[to_additive]
theorem hasProd_of_isLUB_of_one_le [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]
    [TopologicalSpace α]
    [OrderTopology α] {f : ι → α} (i : α) (h : ∀ i, 1 ≤ f i)
    (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) i) : HasProd f i :=
  tendsto_atTop_isLUB (Finset.prod_mono_set_of_one_le' h) hf

Convergence of Infinite Product via Least Upper Bound in Ordered Monoid

Informal description

Let $\alpha$ be a linearly ordered commutative monoid with the order topology, and let $f : \iota \to \alpha$ be a function such that $1 \leq f(i)$ for all $i \in \iota$. If $i \in \alpha$ is the least upper bound of the set of finite partial products $\left\{ \prod_{i \in s} f(i) \mid s \text{ finite subset of } \iota \right\}$, then the infinite product $\prod_{i \in \iota} f(i)$ converges to $i$.

hasProd_of_isLUB theorem

 [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderTopology α]
  {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) b) : HasProd f b

Full source

@[to_additive]
theorem hasProd_of_isLUB [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]
    [CanonicallyOrderedMul α] [TopologicalSpace α]
    [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) b) :
    HasProd f b :=
  tendsto_atTop_isLUB (Finset.prod_mono_set' f) hf

Convergence of Infinite Product via Least Upper Bound in Canonically Ordered Monoid

Informal description

Let $\alpha$ be a linearly ordered commutative monoid with the order topology and the canonical ordering induced by divisibility. Given a function $f \colon \iota \to \alpha$ and an element $b \in \alpha$, if $b$ is the least upper bound of the set of finite partial products $\left\{ \prod_{i \in s} f(i) \mid s \text{ finite subset of } \iota \right\}$, then the infinite product $\prod_{i \in \iota} f(i)$ converges to $b$.

multipliable_mabs_iff theorem

 [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] {f : ι → α} :
  (Multipliable fun x ↦ mabs (f x)) ↔ Multipliable f

Full source

@[to_additive]
theorem multipliable_mabs_iff [CommGroup α] [LinearOrder α] [IsOrderedMonoid α]
    [UniformSpace α] [IsUniformGroup α]
    [CompleteSpace α] {f : ι → α} : (Multipliable fun x ↦ mabs (f x)) ↔ Multipliable f :=
  let s := { x | 1 ≤ f x }
  have h1 : ∀ x : s, mabs (f x) = f x := fun x ↦ mabs_of_one_le x.2
  have h2 : ∀ x : ↑sᶜ, mabs (f x) = (f x)⁻¹ := fun x ↦ mabs_of_lt_one (not_le.1 x.2)
  calc (Multipliable fun x ↦ mabs (f x)) ↔
      (Multipliable fun x : s ↦ mabs (f x)) ∧ Multipliable fun x : ↑sᶜ ↦ mabs (f x) :=
        multipliable_subtype_and_compl.symm
  _ ↔ (Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ (f x)⁻¹calc (Multipliable fun x ↦ mabs (f x)) ↔
      (Multipliable fun x : s ↦ mabs (f x)) ∧ Multipliable fun x : ↑sᶜ ↦ mabs (f x) :=
        multipliable_subtype_and_compl.symm
  _ ↔ (Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ (f x)⁻¹ := by simp only [h1, h2]
  _ ↔ Multipliable f := by simp only [multipliable_inv_iff, multipliable_subtype_and_compl]

Convergence of Infinite Product via Multiplicative Absolute Value: $\prod |f(x)|_m$ converges iff $\prod f(x)$ converges

Informal description

Let $\alpha$ be a complete uniform space equipped with a commutative group structure, a linear order, and an ordered monoid structure, such that the group operations are uniformly continuous. For any function $f \colon \iota \to \alpha$, the infinite product $\prod_{x \in \iota} |f(x)|_m$ converges if and only if the infinite product $\prod_{x \in \iota} f(x)$ converges. Here, $|a|_m$ denotes the multiplicative absolute value of $a \in \alpha$, defined as the supremum of $a$ and its multiplicative inverse $a^{-1}$.

Finite.of_summable_const theorem

 [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [Archimedean α] [OrderClosedTopology α]
  {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) : Finite ι

Full source

theorem Finite.of_summable_const [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]
    [TopologicalSpace α] [Archimedean α]
    [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) :
    Finite ι := by
  have H : ∀ s : Finset ι, #s • b ≤ ∑' _ : ι, b := fun s ↦ by
    simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum
  obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb
  have : ∀ s : Finset ι, #s ≤ n := fun s ↦ by
    simpa [nsmul_le_nsmul_iff_left hb] using (H s).trans hn
  have : Fintype ι := fintypeOfFinsetCardLe n this
  infer_instance

Finiteness of Index Type from Summability of Positive Constant Function

Informal description

Let $\alpha$ be a linearly ordered additive commutative group with an order-closed topology and the Archimedean property. For any positive element $b \in \alpha$ (i.e., $0 < b$), if the constant function $\lambda (_ : \iota), b$ is summable, then the index type $\iota$ is finite.

Set.Finite.of_summable_const theorem

 [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [Archimedean α] [OrderClosedTopology α]
  {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) : (Set.univ : Set ι).Finite

Full source

theorem Set.Finite.of_summable_const [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]
    [TopologicalSpace α]
    [Archimedean α] [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) :
    (Set.univ : Set ι).Finite :=
  finite_univ_iff.2 <| .of_summable_const hb hf

Finiteness of Universal Set from Summability of Positive Constant Function

Informal description

Let $\alpha$ be a linearly ordered additive commutative group with an order-closed topology and the Archimedean property. For any positive element $b \in \alpha$ (i.e., $0 < b$), if the constant function $\lambda (_ : \iota), b$ is summable, then the universal set $\text{univ} : \text{Set}\, \iota$ is finite.

HasProd.abs theorem

(hfx : HasProd f x) : HasProd (|f ·|) |x|

Full source

nonrec theorem HasProd.abs (hfx : HasProd f x) : HasProd (|f ·|) |x| := by
  simpa only [HasProd, ← abs_prod] using hfx.abs

Absolute Value Preserves Product Convergence

Informal description

If a function $f$ has a product converging to $x$, then the function $|f|$ (absolute value of $f$) has a product converging to $|x|$.

Multipliable.abs theorem

(hf : Multipliable f) : Multipliable (|f ·|)

Full source

theorem Multipliable.abs (hf : Multipliable f) : Multipliable (|f ·|) :=
  let ⟨x, hx⟩ := hf; ⟨|x|, hx.abs⟩

Multipliability of Absolute Value Function

Informal description

If a function $f : \beta \to \alpha$ is multipliable, then the function $|f|$ (absolute value of $f$) is also multipliable.

Multipliable.abs_tprod theorem

(hf : Multipliable f) : |∏' i, f i| = ∏' i, |f i|

Full source

protected theorem Multipliable.abs_tprod (hf : Multipliable f) : |∏' i, f i| = ∏' i, |f i| :=
  hf.hasProd.abs.tprod_eq.symm

Absolute Value of Unconditional Product Equals Unconditional Product of Absolute Values

Informal description

For any multipliable function $f : \beta \to \alpha$ in a topological monoid $\alpha$, the absolute value of the unconditional product $\prod'_{i} f(i)$ is equal to the unconditional product of the absolute values $\prod'_{i} |f(i)|$.

Summable.tendsto_atTop_of_pos theorem

 [Field α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α] {f : ℕ → α}
  (hf : Summable f⁻¹) (hf' : ∀ n, 0 < f n) : Tendsto f atTop atTop

Full source

theorem Summable.tendsto_atTop_of_pos [Field α] [LinearOrder α] [IsStrictOrderedRing α]
    [TopologicalSpace α] [OrderTopology α]
    {f : ℕ → α} (hf : Summable f⁻¹) (hf' : ∀ n, 0 < f n) : Tendsto f atTop atTop :=
  inv_inv f ▸ Filter.Tendsto.inv_tendsto_nhdsGT_zero <|
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf.tendsto_atTop_zero <|
      Eventually.of_forall fun _ ↦ inv_pos.2 (hf' _)

Divergence to Infinity of Positive Sequences with Summable Reciprocals

Informal description

Let $\alpha$ be a field with a linear order, a strict ordered ring structure, and an order topology. Given a sequence $f : \mathbb{N} \to \alpha$ such that the sum of the reciprocals $\sum_{n} f(n)^{-1}$ converges and $f(n) > 0$ for all $n$, then $f$ tends to infinity as $n$ tends to infinity, i.e., $\lim_{n \to \infty} f(n) = \infty$.

Mathlib.Meta.Positivity.evalTsum definition

: PositivityExt

Full source

/-- Positivity extension for infinite sums.

This extension only proves non-negativity, strict positivity is more delicate for infinite sums and
requires more assumptions. -/
@[positivity tsum _]
def evalTsum : PositivityExt where eval {u α} zα pα e := do
  match e with
  | ~q(@tsum _ $instCommMonoid $instTopSpace $ι $f) =>
    lambdaBoundedTelescope f 1 fun args (body : Q($α)) => do
      let #[(i : Q($ι))] := args | failure
      let rbody ← core zα pα body
      let pbody ← rbody.toNonneg
      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
      let mα' ← synthInstanceQ q(AddCommMonoid $α)
      let oα' ← synthInstanceQ q(PartialOrder $α)
      let pα' ← synthInstanceQ q(IsOrderedAddMonoid $α)
      let instOrderClosed ← synthInstanceQ q(OrderClosedTopology $α)
      assertInstancesCommute
      return .nonnegative q(@tsum_nonneg $ι $α $mα' $oα' $pα' $instTopSpace $instOrderClosed $f $pr)
  | _ => throwError "not tsum"

Positivity extension for infinite sums

Informal description

The positivity extension for infinite sums, which proves non-negativity of a tsum expression when all its terms are non-negative. Given a summable function $ f : \iota \to \alpha $ where $ \alpha $ is an ordered additive commutative monoid with order-closed topology, if $ 0 \leq f(i) $ for all $ i \in \iota $, then $ 0 \leq \sum' i, f(i) $.