@@ -74,8 +74,8 @@ lemma sInf_eq_zero : sInf s = 0 ↔ 0 ∈ s := by
7474lemma sSup_eq_zero' : sSup s = 0 ↔ s = ∅ ∨ s = {0 } :=
7575 sSup_eq_bot'
7676
77- lemma iSup_eq_zero : iSup f = 0 ↔ ∀ i, f i = 0 :=
78- iSup_eq_bot
77+ @[simp] lemma iSup_eq_zero : iSup f = 0 ↔ ∀ i, f i = 0 := iSup_eq_bot
78+ @[simp] lemma iSup_zero : ⨆ _ : ι, ( 0 : ℕ∞) = 0 := by simp
7979
8080lemma sSup_eq_top_of_infinite (h : s.Infinite) : sSup s = ⊤ := by
8181 apply (sSup_eq_top ..).mpr
@@ -109,4 +109,103 @@ lemma exists_eq_iSup₂_of_lt_top {ι₁ ι₂ : Type*} {f : ι₁ → ι₂ →
109109 rw [iSup_prod'] at h ⊢
110110 exact Prod.exists'.mp (exists_eq_iSup_of_lt_top h)
111111
112+ variable {ι κ : Sort *} {f g : ι → ℕ∞} {s : Set ℕ∞} {a : ℕ∞}
113+
114+ lemma iSup_natCast : ⨆ n : ℕ, (n : ℕ∞) = ⊤ :=
115+ (iSup_eq_top _).2 fun _b hb ↦ ENat.exists_nat_gt (lt_top_iff_ne_top.1 hb)
116+
117+ proof_wanted mul_iSup (a : ℕ∞) (f : ι → ℕ∞) : a * ⨆ i, f i = ⨆ i, a * f i
118+ proof_wanted iSup_mul (f : ι → ℕ∞) (a : ℕ∞) : (⨆ i, f i) * a = ⨆ i, f i * a
119+ proof_wanted mul_sSup : a * sSup s = ⨆ b ∈ s, a * b
120+ proof_wanted sSup_mul : sSup s * a = ⨆ b ∈ s, b * a
121+
122+ proof_wanted mul_iInf' (_h₀ : a = 0 → Nonempty ι) :
123+ a * ⨅ i, f i = ⨅ i, a * f i
124+
125+ proof_wanted iInf_mul' (_h₀ : a = 0 → Nonempty ι) : (⨅ i, f i) * a = ⨅ i, f i * a
126+
127+ /-- If `a ≠ 0` and `a ≠ ⊤`, then right multiplication by `a` maps infimum to infimum.
128+ See also `ENNReal.iInf_mul` that assumes `[Nonempty ι]` but does not require `a ≠ 0`. -/
129+ proof_wanted mul_iInf_of_ne (_ha₀ : a ≠ 0 ) (_ha : a ≠ ⊤) : a * ⨅ i, f i = ⨅ i, a * f i
130+
131+ /-- If `a ≠ 0` and `a ≠ ⊤`, then right multiplication by `a` maps infimum to infimum.
132+ See also `ENNReal.iInf_mul` that assumes `[Nonempty ι]` but does not require `a ≠ 0`. -/
133+ proof_wanted iInf_mul_of_ne (_ha₀ : a ≠ 0 ) (_ha : a ≠ ⊤) : (⨅ i, f i) * a = ⨅ i, f i * a
134+
135+ proof_wanted mul_iInf [Nonempty ι] : a * ⨅ i, f i = ⨅ i, a * f i
136+ proof_wanted iInf_mul [Nonempty ι] : (⨅ i, f i) * a = ⨅ i, f i * a
137+
138+ lemma add_iSup [Nonempty ι] (f : ι → ℕ∞) : a + ⨆ i, f i = ⨆ i, a + f i := by
139+ obtain rfl | ha := eq_or_ne a ⊤
140+ · simp
141+ refine le_antisymm ?_ <| iSup_le fun i ↦ add_le_add_left (le_iSup ..) _
142+ refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_
143+ exact iSup_le fun i ↦ ENat.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i
144+
145+ lemma iSup_add [Nonempty ι] (f : ι → ℕ∞) : (⨆ i, f i) + a = ⨆ i, f i + a := by
146+ simp [add_comm, add_iSup]
147+
148+ lemma add_biSup' {p : ι → Prop } (h : ∃ i, p i) (f : ι → ℕ∞) :
149+ a + ⨆ i, ⨆ _ : p i, f i = ⨆ i, ⨆ _ : p i, a + f i := by
150+ haveI : Nonempty {i // p i} := nonempty_subtype.2 h
151+ simp only [iSup_subtype', add_iSup]
152+
153+ lemma biSup_add' {p : ι → Prop } (h : ∃ i, p i) (f : ι → ℕ∞) :
154+ (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, f i + a := by simp only [add_comm, add_biSup' h]
155+
156+ lemma add_biSup {ι : Type *} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) :
157+ a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i := add_biSup' hs _
158+
159+ lemma biSup_add {ι : Type *} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) :
160+ (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a := biSup_add' hs _
161+
162+ lemma add_sSup (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b := by
163+ rw [sSup_eq_iSup, add_biSup hs]
164+
165+ lemma sSup_add (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a := by
166+ rw [sSup_eq_iSup, biSup_add hs]
167+
168+ lemma iSup_add_iSup_le [Nonempty ι] [Nonempty κ] {g : κ → ℕ∞} (h : ∀ i j, f i + g j ≤ a) :
169+ iSup f + iSup g ≤ a := by simp_rw [iSup_add, add_iSup]; exact iSup₂_le h
170+
171+ lemma biSup_add_biSup_le' {p : ι → Prop } {q : κ → Prop } (hp : ∃ i, p i) (hq : ∃ j, q j)
172+ {g : κ → ℕ∞} (h : ∀ i, p i → ∀ j, q j → f i + g j ≤ a) :
173+ (⨆ i, ⨆ _ : p i, f i) + ⨆ j, ⨆ _ : q j, g j ≤ a := by
174+ simp_rw [biSup_add' hp, add_biSup' hq]
175+ exact iSup₂_le fun i hi => iSup₂_le (h i hi)
176+
177+ lemma biSup_add_biSup_le {ι κ : Type *} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty)
178+ {f : ι → ℕ∞} {g : κ → ℕ∞} {a : ℕ∞} (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) :
179+ (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a := biSup_add_biSup_le' hs ht h
180+
181+ lemma iSup_add_iSup (h : ∀ i j, ∃ k, f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ i, f i + g i := by
182+ cases isEmpty_or_nonempty ι
183+ · simp only [iSup_of_empty, bot_eq_zero, zero_add]
184+ · refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
185+ refine iSup_add_iSup_le fun i j => ?_
186+ rcases h i j with ⟨k, hk⟩
187+ exact le_iSup_of_le k hk
188+
189+ lemma iSup_add_iSup_of_monotone {ι : Type *} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → ℕ∞}
190+ (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ a, f a + g a :=
191+ iSup_add_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ ↦ by gcongr <;> apply_rules
192+
193+ proof_wanted smul_iSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R) :
194+ c • ⨆ i, f i = ⨆ i, c • f i
195+
196+ proof_wanted smul_sSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (s : Set ℕ∞) (c : R) :
197+ c • sSup s = ⨆ a ∈ s, c • a
198+
199+ lemma sub_iSup [Nonempty ι] (ha : a ≠ ⊤) : a - ⨆ i, f i = ⨅ i, a - f i := by
200+ obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
201+ · rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, (iInf_eq_bot _).2 , bot_eq_zero]
202+ exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩
203+ simp_rw [not_exists, not_lt] at h
204+ refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
205+ ENat.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
206+ add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
207+ iSup_le fun i ↦ ?_
208+ rw [← ENat.sub_sub_cancel ha (h _)]
209+ exact tsub_le_tsub_left (iInf_le (a - f ·) i) _
210+
112211end ENat
0 commit comments