ENNReal manipulation lemmas

theorem ENNReal.coe_lt_iff_lt_toNNReal {a : ENNReal} {t : NNReal} (ha : a ≠ ⊤) : ↑t < a ↔ t < a.toNNReal

theorem ENNReal.le_mul_top_self {x : ENNReal} : x ≤ ⊤ * x

theorem ENNReal.coe_biSup {ι : Type u_2} {s : Set ι} {f : ι → NNReal} (hf : BddAbove (Set.range f)) : ↑(⨆ x ∈ s, f x) = ⨆ x ∈ s, ↑(f x)

theorem ENNReal.biSup_add_biSup {ι : Type u_2} {s : Set ι} {f g : ι → ENNReal} (h : ∀ i ∈ s, ∀ j ∈ s, ∃ k ∈ s, f i + g j ≤ f k + g k) : (⨆ i ∈ s, f i) + ⨆ i ∈ s, g i = ⨆ i ∈ s, f i + g i

theorem ENNReal.finsetSum_biSup {α : Type u_1} {ι : Type u_2} {s : Set ι} {t : Finset α} {f : α → ι → ENNReal} (hf : ∀ i ∈ s, ∀ j ∈ s, ∃ k ∈ s, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k) : ∑ a ∈ t, ⨆ i ∈ s, f a i = ⨆ i ∈ s, ∑ a ∈ t, f a i

theorem ENNReal.biSup_add_le_add_biSup {ι : Type u_2} {s : Set ι} {f g : ι → ENNReal} : ⨆ i ∈ s, f i + g i ≤ (⨆ i ∈ s, f i) + ⨆ i ∈ s, g i

theorem ENNReal.biSup_finsetSum_le_finsetSum_biSup {α : Type u_1} {ι : Type u_2} {s : Set ι} {t : Finset α} {f : α → ι → ENNReal} : ⨆ i ∈ s, ∑ a ∈ t, f a i ≤ ∑ a ∈ t, ⨆ i ∈ s, f a i

theorem ENNReal.edist_sum_le_sum_edist {α : Type u_1} {t : Finset α} {E : Type u_3} [SeminormedAddCommGroup E] {f g : α → E} : edist (∑ i ∈ t, f i) (∑ i ∈ t, g i) ≤ ∑ i ∈ t, edist (f i) (g i)

theorem ENNReal.enorm_sum_eq_sum_enorm {α : Type u_1} {t : Finset α} {f : α → ℝ} (hf : ∀ i ∈ t, 0 ≤ f i) : ‖∑ i ∈ t, f i‖ₑ = ∑ i ∈ t, ‖f i‖ₑ

theorem ENNReal.enorm_enorm_sub_enorm_le {E : Type u_4} [NormedAddCommGroup E] {x y : E} : ‖‖x‖ₑ - ‖y‖ₑ‖ₑ ≤ ‖x - y‖ₑ

The reverse triangle inequality for enorm.

theorem ENNReal.exists_biSup_le_enorm_add_eps {ι : Type u_2} {s : Set ι} {E : Type u_3} [SeminormedAddCommGroup E] {f : ι → E} {ε : NNReal} (εpos : 0 < ε) (hs : s.Nonempty) (hf : Bornology.IsBounded (f '' s)) : ∃ x ∈ s, ⨆ z ∈ s, ‖f z‖ₑ ≤ ‖f x‖ₑ + ↑ε

theorem ENNReal.exists_enorm_sub_eps_le_biInf {ι : Type u_2} {s : Set ι} {E : Type u_3} [SeminormedAddCommGroup E] {f : ι → E} {ε : NNReal} (εpos : 0 < ε) (hs : s.Nonempty) : ∃ x ∈ s, ‖f x‖ₑ - ↑ε ≤ ⨅ z ∈ s, ‖f z‖ₑ

theorem ENNReal.biInf_enorm_sub_le {ι : Type u_2} {s : Set ι} {E : Type u_3} [SeminormedAddCommGroup E] {f g : ι → E} : ⨅ x ∈ s, ‖f x - g x‖ₑ ≤ (⨅ x ∈ s, ‖f x‖ₑ) + ⨆ x ∈ s, ‖g x‖ₑ

theorem Real.enorm_le_enorm {x y : ℝ} (hx : 0 ≤ x) (hy : x ≤ y) : ‖x‖ₑ ≤ ‖y‖ₑ

Transfer an inequality over ℝ to one of ENorms over ℝ≥0∞.