Skip to content

Commit 9ee43a5

Browse files
YaelDilliesdagurtomas
YaelDillies
authored and
dagurtomas
committed
chore: Split off WithTop lemmas (#10239)
from `Algebra.BigOperators.Order` . Add the corresponding `WithBot` lemmas.
1 parent c4d7fd2 commit 9ee43a5

File tree

6 files changed

+87
-39
lines changed

6 files changed

+87
-39
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ import Mathlib.Algebra.BigOperators.Order
3434
import Mathlib.Algebra.BigOperators.Pi
3535
import Mathlib.Algebra.BigOperators.Ring
3636
import Mathlib.Algebra.BigOperators.RingEquiv
37+
import Mathlib.Algebra.BigOperators.WithTop
3738
import Mathlib.Algebra.Bounds
3839
import Mathlib.Algebra.Category.AlgebraCat.Basic
3940
import Mathlib.Algebra.Category.AlgebraCat.Limits

‎Mathlib/Algebra/BigOperators/Order.lean‎

Lines changed: 1 addition & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl
55
-/
6-
import Mathlib.Algebra.Order.AbsoluteValue
7-
import Mathlib.Algebra.Order.Ring.WithTop
86
import Mathlib.Algebra.BigOperators.Ring
9-
import Mathlib.Data.Fintype.Card
7+
import Mathlib.Algebra.Order.AbsoluteValue
108
import Mathlib.Tactic.GCongr.Core
119
import Mathlib.Tactic.Ring
1210

@@ -791,37 +789,6 @@ lemma prod_lt_one_iff_of_le_one (hf : f ≤ 1) : ∏ i, f i < 1 ↔ f < 1 := by
791789
end OrderedCancelCommMonoid
792790
end Fintype
793791

794-
namespace WithTop
795-
796-
open Finset
797-
798-
/-- A product of finite numbers is still finite -/
799-
theorem prod_lt_top [CommMonoidWithZero R] [NoZeroDivisors R] [Nontrivial R] [DecidableEq R] [LT R]
800-
{s : Finset ι} {f : ι → WithTop R} (h : ∀ i ∈ s, f i ≠ ⊤) : ∏ i in s, f i < ⊤ :=
801-
prod_induction f (fun a ↦ a < ⊤) (fun _ _ h₁ h₂ ↦ mul_lt_top' h₁ h₂) (coe_lt_top 1)
802-
fun a ha ↦ WithTop.lt_top_iff_ne_top.2 (h a ha)
803-
#align with_top.prod_lt_top WithTop.prod_lt_top
804-
805-
/-- A sum of numbers is infinite iff one of them is infinite -/
806-
theorem sum_eq_top_iff [AddCommMonoid M] {s : Finset ι} {f : ι → WithTop M} :
807-
∑ i in s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤ := by
808-
induction s using Finset.cons_induction <;> simp [*]
809-
#align with_top.sum_eq_top_iff WithTop.sum_eq_top_iff
810-
811-
/-- A sum of finite numbers is still finite -/
812-
theorem sum_lt_top_iff [AddCommMonoid M] [LT M] {s : Finset ι} {f : ι → WithTop M} :
813-
∑ i in s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤ := by
814-
simp only [WithTop.lt_top_iff_ne_top, ne_eq, sum_eq_top_iff, not_exists, not_and]
815-
#align with_top.sum_lt_top_iff WithTop.sum_lt_top_iff
816-
817-
/-- A sum of finite numbers is still finite -/
818-
theorem sum_lt_top [AddCommMonoid M] [LT M] {s : Finset ι} {f : ι → WithTop M}
819-
(h : ∀ i ∈ s, f i ≠ ⊤) : ∑ i in s, f i < ⊤ :=
820-
sum_lt_top_iff.2 fun i hi => WithTop.lt_top_iff_ne_top.2 (h i hi)
821-
#align with_top.sum_lt_top WithTop.sum_lt_top
822-
823-
end WithTop
824-
825792
section AbsoluteValue
826793

827794
variable {S : Type*}

‎Mathlib/Algebra/BigOperators/WithTop.lean‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
/-
2+
Copyright (c) 2024 Zhouhang Zhou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Zhouhang Zhou, Yaël Dillies
5+
-/
6+
import Mathlib.Algebra.BigOperators.Basic
7+
import Mathlib.Algebra.Order.Ring.WithTop
8+
9+
/-!
10+
# Sums in `WithTop`
11+
12+
This file proves results about finite sums over monoids extended by a bottom or top element.
13+
-/
14+
15+
open Finset
16+
open scoped BigOperators
17+
18+
variable {ι α : Type*}
19+
20+
namespace WithTop
21+
section AddCommMonoid
22+
variable [AddCommMonoid α] [LT α] {s : Finset ι} {f : ι → WithTop α}
23+
24+
@[simp, norm_cast] lemma coe_sum (s : Finset ι) (f : ι → α) :
25+
∑ i in s, f i = ∑ i in s, (f i : WithTop α) := map_sum addHom f s
26+
27+
/-- A sum is infinite iff one term is infinite. -/
28+
lemma sum_eq_top_iff : ∑ i in s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤ := by
29+
induction s using Finset.cons_induction <;> simp [*]
30+
#align with_top.sum_eq_top_iff WithTop.sum_eq_top_iff
31+
32+
/-- A sum is finite iff all terms are finite. -/
33+
lemma sum_lt_top_iff : ∑ i in s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤ := by
34+
simp only [WithTop.lt_top_iff_ne_top, ne_eq, sum_eq_top_iff, not_exists, not_and]
35+
#align with_top.sum_lt_top_iff WithTop.sum_lt_top_iff
36+
37+
/-- A sum of finite terms is finite. -/
38+
lemma sum_lt_top (h : ∀ i ∈ s, f i ≠ ⊤) : ∑ i in s, f i < ⊤ :=
39+
sum_lt_top_iff.2 fun i hi ↦ WithTop.lt_top_iff_ne_top.2 (h i hi)
40+
#align with_top.sum_lt_top WithTop.sum_lt_top
41+
42+
end AddCommMonoid
43+
44+
/-- A product of finite terms is finite. -/
45+
lemma prod_lt_top [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] [DecidableEq α] [LT α]
46+
{s : Finset ι} {f : ι → WithTop α} (h : ∀ i ∈ s, f i ≠ ⊤) : ∏ i in s, f i < ⊤ :=
47+
prod_induction f (· < ⊤) (fun _ _ h₁ h₂ ↦ mul_lt_top' h₁ h₂) (coe_lt_top 1)
48+
fun a ha ↦ WithTop.lt_top_iff_ne_top.2 (h a ha)
49+
#align with_top.prod_lt_top WithTop.prod_lt_top
50+
51+
end WithTop
52+
53+
namespace WithBot
54+
section AddCommMonoid
55+
variable [AddCommMonoid α] [LT α] {s : Finset ι} {f : ι → WithBot α}
56+
57+
@[simp, norm_cast] lemma coe_sum (s : Finset ι) (f : ι → α) :
58+
∑ i in s, f i = ∑ i in s, (f i : WithBot α) := map_sum addHom f s
59+
60+
/-- A sum is infinite iff one term is infinite. -/
61+
lemma sum_eq_bot_iff : ∑ i in s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥ := by
62+
induction s using Finset.cons_induction <;> simp [*]
63+
64+
/-- A sum is finite iff all terms are finite. -/
65+
lemma bot_lt_sum_iff : ⊥ < ∑ i in s, f i ↔ ∀ i ∈ s, ⊥ < f i := by
66+
simp only [WithBot.bot_lt_iff_ne_bot, ne_eq, sum_eq_bot_iff, not_exists, not_and]
67+
68+
/-- A sum of finite terms is finite. -/
69+
lemma sum_lt_bot (h : ∀ i ∈ s, f i ≠ ⊥) : ⊥ < ∑ i in s, f i :=
70+
bot_lt_sum_iff.2 fun i hi ↦ WithBot.bot_lt_iff_ne_bot.2 (h i hi)
71+
#align with_bot.sum_lt_bot WithBot.sum_lt_bot
72+
73+
end AddCommMonoid
74+
75+
/-- A product of finite terms is finite. -/
76+
lemma prod_lt_bot [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] [DecidableEq α] [LT α]
77+
{s : Finset ι} {f : ι → WithBot α} (h : ∀ i ∈ s, f i ≠ ⊥) : ⊥ < ∏ i in s, f i :=
78+
prod_induction f (⊥ < ·) (fun _ _ h₁ h₂ ↦ bot_lt_mul' h₁ h₂) (bot_lt_coe 1)
79+
fun a ha ↦ WithBot.bot_lt_iff_ne_bot.2 (h a ha)
80+
#align with_bot.prod_lt_bot WithBot.prod_lt_bot
81+
82+
end WithBot

‎Mathlib/Data/ENNReal/Basic.lean‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,10 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Yury Kudryashov
55
-/
6-
import Mathlib.Data.Real.NNReal
6+
import Mathlib.Algebra.Order.Ring.WithTop
77
import Mathlib.Algebra.Order.Sub.WithTop
8+
import Mathlib.Data.Real.NNReal
89
import Mathlib.Data.Set.Intervals.WithBotTop
9-
import Mathlib.Tactic.GCongr.Core
10-
import Mathlib.Algebra.GroupPower.Order
11-
import Mathlib.Data.Set.Lattice
1210

1311
#align_import data.real.ennreal from "leanprover-community/mathlib"@"c14c8fcde993801fca8946b0d80131a1a81d1520"
1412

‎Mathlib/Data/ENNReal/Operations.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Yury Kudryashov
55
-/
6+
import Mathlib.Algebra.BigOperators.WithTop
67
import Mathlib.Algebra.GroupPower.Ring
78
import Mathlib.Data.ENNReal.Basic
89

‎Mathlib/Data/Real/NNReal.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Johan Commelin
55
-/
66
import Mathlib.Algebra.Algebra.Basic
77
import Mathlib.Algebra.BigOperators.Order
8-
import Mathlib.Algebra.BigOperators.Ring
98
import Mathlib.Algebra.Order.Field.Canonical.Basic
109
import Mathlib.Algebra.Order.Nonneg.Field
1110
import Mathlib.Algebra.Order.Nonneg.Floor

0 commit comments

Comments
 (0)