import data.real.nnreal

import algebra.order.sub.with_top

open classical set

open_locale classical big_operators nnreal

variables {α : Type*} {β : Type*}

linear_ordered_add_comm_monoid_with_top, char_zero]]

def ennreal := with_top ℝ≥0

localized "notation (name := ennreal) `ℝ≥0∞` := ennreal" in ennreal

localized "notation (name := ennreal.top) `∞` := (⊤ : ennreal)" in ennreal

namespace ennreal

variables {a b c d : ℝ≥0∞} {r p q : ℝ≥0}

instance covariant_class_mul_le : covariant_class ℝ≥0∞ ℝ≥0∞ (*) (≤) :=

canonically_ordered_comm_semiring.to_covariant_mul_le

instance covariant_class_add_le : covariant_class ℝ≥0∞ ℝ≥0∞ (+) (≤) :=

ordered_add_comm_monoid.to_covariant_class_left ℝ≥0∞

noncomputable instance : linear_ordered_comm_monoid_with_zero ℝ≥0∞ :=

{ mul_le_mul_left := λ a b, mul_le_mul_left',

zero_le_one := zero_le 1,

.. ennreal.linear_ordered_add_comm_monoid_with_top,

.. (show comm_semiring ℝ≥0∞, from infer_instance) }

instance : unique (add_units ℝ≥0∞) :=

{ default := 0,

uniq := λ a, add_units.ext $ le_zero_iff.1 $ by { rw ←a.add_neg, exact le_self_add } }

instance : inhabited ℝ≥0∞ := ⟨0⟩

instance : has_coe ℝ≥0 ℝ≥0∞ := ⟨ option.some ⟩

instance can_lift : can_lift ℝ≥0∞ ℝ≥0 coe (λ r, r ≠ ∞) :=

{ prf := λ x hx, ⟨option.get $ option.ne_none_iff_is_some.1 hx, option.some_get _⟩ }

@[simp] lemma none_eq_top : (none : ℝ≥0∞) = ∞ := rfl

@[simp] lemma some_eq_coe (a : ℝ≥0) : (some a : ℝ≥0∞) = (↑a : ℝ≥0∞) := rfl

protected def to_nnreal : ℝ≥0∞ → ℝ≥0 := with_top.untop' 0

protected def to_real (a : ℝ≥0∞) : real := coe (a.to_nnreal)

protected noncomputable def of_real (r : real) : ℝ≥0∞ := coe (real.to_nnreal r)

@[simp, norm_cast] lemma to_nnreal_coe : (r : ℝ≥0∞).to_nnreal = r := rfl

@[simp] lemma coe_to_nnreal : ∀{a:ℝ≥0∞}, a ≠ ∞ → ↑(a.to_nnreal) = a

| (some r) h := rfl

| none h := (h rfl).elim

@[simp] lemma of_real_to_real {a : ℝ≥0∞} (h : a ≠ ∞) : ennreal.of_real (a.to_real) = a :=

by simp [ennreal.to_real, ennreal.of_real, h]

@[simp] lemma to_real_of_real {r : ℝ} (h : 0 ≤ r) : ennreal.to_real (ennreal.of_real r) = r :=

by simp [ennreal.to_real, ennreal.of_real, real.coe_to_nnreal _ h]

lemma to_real_of_real' {r : ℝ} : ennreal.to_real (ennreal.of_real r) = max r 0 := rfl

lemma coe_to_nnreal_le_self : ∀{a:ℝ≥0∞}, ↑(a.to_nnreal) ≤ a

| (some r) := by rw [some_eq_coe, to_nnreal_coe]; exact le_rfl

| none := le_top

lemma coe_nnreal_eq (r : ℝ≥0) : (r : ℝ≥0∞) = ennreal.of_real r :=

by { rw [ennreal.of_real, real.to_nnreal], cases r with r h, congr, dsimp, rw max_eq_left h }

lemma of_real_eq_coe_nnreal {x : ℝ} (h : 0 ≤ x) :

ennreal.of_real x = @coe ℝ≥0 ℝ≥0∞ _ (⟨x, h⟩ : ℝ≥0) :=

by { rw [coe_nnreal_eq], refl }

@[simp] lemma of_real_coe_nnreal : ennreal.of_real p = p := (coe_nnreal_eq p).symm

@[simp, norm_cast] lemma coe_zero : ↑(0 : ℝ≥0) = (0 : ℝ≥0∞) := rfl

@[simp, norm_cast] lemma coe_one : ↑(1 : ℝ≥0) = (1 : ℝ≥0∞) := rfl

@[simp] lemma to_real_nonneg {a : ℝ≥0∞} : 0 ≤ a.to_real := by simp [ennreal.to_real]

@[simp] lemma top_to_nnreal : ∞.to_nnreal = 0 := rfl

@[simp] lemma top_to_real : ∞.to_real = 0 := rfl

@[simp] lemma one_to_real : (1 : ℝ≥0∞).to_real = 1 := rfl

@[simp] lemma one_to_nnreal : (1 : ℝ≥0∞).to_nnreal = 1 := rfl

@[simp] lemma coe_to_real (r : ℝ≥0) : (r : ℝ≥0∞).to_real = r := rfl

@[simp] lemma zero_to_nnreal : (0 : ℝ≥0∞).to_nnreal = 0 := rfl

@[simp] lemma zero_to_real : (0 : ℝ≥0∞).to_real = 0 := rfl

@[simp] lemma of_real_zero : ennreal.of_real (0 : ℝ) = 0 :=

by simp [ennreal.of_real]; refl

@[simp] lemma of_real_one : ennreal.of_real (1 : ℝ) = (1 : ℝ≥0∞) :=

by simp [ennreal.of_real]

lemma of_real_to_real_le {a : ℝ≥0∞} : ennreal.of_real (a.to_real) ≤ a :=

if ha : a = ∞ then ha.symm ▸ le_top else le_of_eq (of_real_to_real ha)

lemma forall_ennreal {p : ℝ≥0∞ → Prop} : (∀a, p a) ↔ (∀r:ℝ≥0, p r) ∧ p ∞ :=

⟨assume h, ⟨assume r, h _, h _⟩,

assume ⟨h₁, h₂⟩ a, match a with some r := h₁ _ | none := h₂ end⟩

lemma forall_ne_top {p : ℝ≥0∞ → Prop} : (∀ a ≠ ∞, p a) ↔ ∀ r : ℝ≥0, p r :=

option.ball_ne_none

lemma exists_ne_top {p : ℝ≥0∞ → Prop} : (∃ a ≠ ∞, p a) ↔ ∃ r : ℝ≥0, p r :=

option.bex_ne_none

lemma to_nnreal_eq_zero_iff (x : ℝ≥0∞) : x.to_nnreal = 0 ↔ x = 0 ∨ x = ∞ :=

⟨begin

cases x,

{ simp [none_eq_top] },

{ rintro (rfl : x = 0),

exact or.inl rfl },

end,

by rintro (h | h); simp [h]⟩

lemma to_real_eq_zero_iff (x : ℝ≥0∞) : x.to_real = 0 ↔ x = 0 ∨ x = ∞ :=

by simp [ennreal.to_real, to_nnreal_eq_zero_iff]

lemma to_nnreal_ne_zero : a.to_nnreal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞ :=

a.to_nnreal_eq_zero_iff.not.trans not_or_distrib

lemma to_real_ne_zero : a.to_real ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞ :=

a.to_real_eq_zero_iff.not.trans not_or_distrib

lemma to_nnreal_eq_one_iff (x : ℝ≥0∞) : x.to_nnreal = 1 ↔ x = 1 :=

refine ⟨λ h, _, congr_arg _⟩,

cases x,

{ exact false.elim (zero_ne_one $ ennreal.top_to_nnreal.symm.trans h) },

{ exact congr_arg _ h }

lemma to_real_eq_one_iff (x : ℝ≥0∞) : x.to_real = 1 ↔ x = 1 :=

by rw [ennreal.to_real, nnreal.coe_eq_one, ennreal.to_nnreal_eq_one_iff]

lemma to_nnreal_ne_one : a.to_nnreal ≠ 1 ↔ a ≠ 1 := a.to_nnreal_eq_one_iff.not

lemma to_real_ne_one : a.to_real ≠ 1 ↔ a ≠ 1 := a.to_real_eq_one_iff.not

@[simp] lemma coe_ne_top : (r : ℝ≥0∞) ≠ ∞ := with_top.coe_ne_top

@[simp] lemma top_ne_coe : ∞ ≠ (r : ℝ≥0∞) := with_top.top_ne_coe

@[simp] lemma of_real_ne_top {r : ℝ} : ennreal.of_real r ≠ ∞ := by simp [ennreal.of_real]

@[simp] lemma of_real_lt_top {r : ℝ} : ennreal.of_real r < ∞ := lt_top_iff_ne_top.2 of_real_ne_top

@[simp] lemma top_ne_of_real {r : ℝ} : ∞ ≠ ennreal.of_real r := by simp [ennreal.of_real]

@[simp] lemma of_real_to_real_eq_iff : ennreal.of_real a.to_real = a ↔ a ≠ ⊤ :=

⟨λ h, by { rw ←h, exact of_real_ne_top }, of_real_to_real⟩

@[simp] lemma to_real_of_real_eq_iff {a : ℝ} : (ennreal.of_real a).to_real = a ↔ 0 ≤ a :=

⟨λ h, by { rw ←h, exact to_real_nonneg }, to_real_of_real⟩

@[simp] lemma zero_ne_top : 0 ≠ ∞ := coe_ne_top

@[simp] lemma top_ne_zero : ∞ ≠ 0 := top_ne_coe

@[simp] lemma one_ne_top : 1 ≠ ∞ := coe_ne_top

@[simp] lemma top_ne_one : ∞ ≠ 1 := top_ne_coe

@[simp, norm_cast] lemma coe_eq_coe : (↑r : ℝ≥0∞) = ↑q ↔ r = q := with_top.coe_eq_coe

@[simp, norm_cast] lemma coe_le_coe : (↑r : ℝ≥0∞) ≤ ↑q ↔ r ≤ q := with_top.coe_le_coe

@[simp, norm_cast] lemma coe_lt_coe : (↑r : ℝ≥0∞) < ↑q ↔ r < q := with_top.coe_lt_coe

lemma coe_mono : monotone (coe : ℝ≥0 → ℝ≥0∞) := λ _ _, coe_le_coe.2

@[simp, norm_cast] lemma coe_eq_zero : (↑r : ℝ≥0∞) = 0 ↔ r = 0 := coe_eq_coe

@[simp, norm_cast] lemma zero_eq_coe : 0 = (↑r : ℝ≥0∞) ↔ 0 = r := coe_eq_coe

@[simp, norm_cast] lemma coe_eq_one : (↑r : ℝ≥0∞) = 1 ↔ r = 1 := coe_eq_coe

@[simp, norm_cast] lemma one_eq_coe : 1 = (↑r : ℝ≥0∞) ↔ 1 = r := coe_eq_coe

@[simp, norm_cast] lemma coe_pos : 0 < (↑r : ℝ≥0∞) ↔ 0 < r := coe_lt_coe

lemma coe_ne_zero : (r : ℝ≥0∞) ≠ 0 ↔ r ≠ 0 := not_congr coe_eq_coe

@[simp, norm_cast] lemma coe_add : ↑(r + p) = (r + p : ℝ≥0∞) := with_top.coe_add

@[simp, norm_cast] lemma coe_mul : ↑(r * p) = (r * p : ℝ≥0∞) := with_top.coe_mul

@[simp, norm_cast] lemma coe_bit0 : (↑(bit0 r) : ℝ≥0∞) = bit0 r := coe_add

@[simp, norm_cast] lemma coe_bit1 : (↑(bit1 r) : ℝ≥0∞) = bit1 r := by simp [bit1]

lemma coe_two : ((2:ℝ≥0) : ℝ≥0∞) = 2 := by norm_cast

lemma to_nnreal_eq_to_nnreal_iff (x y : ℝ≥0∞) :

x.to_nnreal = y.to_nnreal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0 :=

cases x,

{ simp only [@eq_comm ℝ≥0 _ y.to_nnreal, @eq_comm ℝ≥0∞ _ y, to_nnreal_eq_zero_iff,

none_eq_top, top_to_nnreal, top_ne_zero, false_and, eq_self_iff_true,

true_and, false_or, or_comm (y = ⊤)] },

{ cases y; simp }

lemma to_real_eq_to_real_iff (x y : ℝ≥0∞) :

x.to_real = y.to_real ↔ x = y ∨ (x = 0 ∧ y = ⊤) ∨ (x = ⊤ ∧ y = 0) :=

by simp only [ennreal.to_real, nnreal.coe_eq, to_nnreal_eq_to_nnreal_iff]

lemma to_nnreal_eq_to_nnreal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

x.to_nnreal = y.to_nnreal ↔ x = y :=

by simp only [ennreal.to_nnreal_eq_to_nnreal_iff x y, hx, hy, and_false, false_and, or_false]

lemma to_real_eq_to_real_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

x.to_real = y.to_real ↔ x = y :=

by simp only [ennreal.to_real, nnreal.coe_eq, to_nnreal_eq_to_nnreal_iff' hx hy]

@[simp] lemma one_lt_two : (1 : ℝ≥0∞) < 2 :=

coe_one ▸ coe_two ▸ by exact_mod_cast (one_lt_two : 1 < 2)

lemma two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_two ▸ coe_ne_top

instance _root_.fact_one_le_one_ennreal : fact ((1 : ℝ≥0∞) ≤ 1) := ⟨le_rfl⟩

instance _root_.fact_one_le_two_ennreal : fact ((1 : ℝ≥0∞) ≤ 2) := ⟨one_le_two⟩

instance _root_.fact_one_le_top_ennreal : fact ((1 : ℝ≥0∞) ≤ ∞) := ⟨le_top⟩

def ne_top_equiv_nnreal : {a | a ≠ ∞} ≃ ℝ≥0 :=

{ to_fun := λ x, ennreal.to_nnreal x,

inv_fun := λ x, ⟨x, coe_ne_top⟩,

left_inv := λ ⟨x, hx⟩, subtype.eq $ coe_to_nnreal hx,

right_inv := λ x, to_nnreal_coe }

lemma cinfi_ne_top [has_Inf α] (f : ℝ≥0∞ → α) : (⨅ x : {x // x ≠ ∞}, f x) = ⨅ x : ℝ≥0, f x :=

eq.symm $ ne_top_equiv_nnreal.symm.surjective.infi_congr _$ λ x, rfl

lemma infi_ne_top [complete_lattice α] (f : ℝ≥0∞ → α) : (⨅ x ≠ ∞, f x) = ⨅ x : ℝ≥0, f x :=

by rw [infi_subtype', cinfi_ne_top]

lemma csupr_ne_top [has_Sup α] (f : ℝ≥0∞ → α) : (⨆ x : {x // x ≠ ∞}, f x) = ⨆ x : ℝ≥0, f x :=

@cinfi_ne_top αᵒᵈ _ _

lemma supr_ne_top [complete_lattice α] (f : ℝ≥0∞ → α) : (⨆ x ≠ ∞, f x) = ⨆ x : ℝ≥0, f x :=

@infi_ne_top αᵒᵈ _ _

lemma infi_ennreal {α : Type*} [complete_lattice α] {f : ℝ≥0∞ → α} :

(⨅ n, f n) = (⨅ n : ℝ≥0, f n) ⊓ f ∞ :=

le_antisymm

(le_inf (le_infi $ assume i, infi_le _ _) (infi_le _ _))

(le_infi $ forall_ennreal.2 ⟨λ r, inf_le_of_left_le $ infi_le _ _, inf_le_right⟩)

lemma supr_ennreal {α : Type*} [complete_lattice α] {f : ℝ≥0∞ → α} :

(⨆ n, f n) = (⨆ n : ℝ≥0, f n) ⊔ f ∞ :=

@infi_ennreal αᵒᵈ _ _

def of_nnreal_hom : ℝ≥0 →+* ℝ≥0∞ :=

⟨coe, coe_one, λ _ _, coe_mul, coe_zero, λ _ _, coe_add⟩

@[simp] lemma coe_of_nnreal_hom : ⇑of_nnreal_hom = coe := rfl

section actions

noncomputable instance {M : Type*} [mul_action ℝ≥0∞ M] : mul_action ℝ≥0 M :=

mul_action.comp_hom M of_nnreal_hom.to_monoid_hom

lemma smul_def {M : Type*} [mul_action ℝ≥0∞ M] (c : ℝ≥0) (x : M) :

c • x = (c : ℝ≥0∞) • x := rfl

instance {M N : Type*} [mul_action ℝ≥0∞ M] [mul_action ℝ≥0∞ N] [has_smul M N]

[is_scalar_tower ℝ≥0∞ M N] : is_scalar_tower ℝ≥0 M N :=

{ smul_assoc := λ r, (smul_assoc (r : ℝ≥0∞) : _)}

instance smul_comm_class_left {M N : Type*} [mul_action ℝ≥0∞ N] [has_smul M N]

[smul_comm_class ℝ≥0∞ M N] : smul_comm_class ℝ≥0 M N :=

{ smul_comm := λ r, (smul_comm (r : ℝ≥0∞) : _)}

instance smul_comm_class_right {M N : Type*} [mul_action ℝ≥0∞ N] [has_smul M N]

[smul_comm_class M ℝ≥0∞ N] : smul_comm_class M ℝ≥0 N :=

{ smul_comm := λ m r, (smul_comm m (r : ℝ≥0∞) : _)}

noncomputable instance {M : Type*} [add_monoid M] [distrib_mul_action ℝ≥0∞ M] :

distrib_mul_action ℝ≥0 M :=

distrib_mul_action.comp_hom M of_nnreal_hom.to_monoid_hom

noncomputable instance {M : Type*} [add_comm_monoid M] [module ℝ≥0∞ M] : module ℝ≥0 M :=

module.comp_hom M of_nnreal_hom

noncomputable instance {A : Type*} [semiring A] [algebra ℝ≥0∞ A] : algebra ℝ≥0 A :=

{ smul := (•),

commutes' := λ r x, by simp [algebra.commutes],

smul_def' := λ r x, by simp [←algebra.smul_def (r : ℝ≥0∞) x, smul_def],

to_ring_hom := ((algebra_map ℝ≥0∞ A).comp (of_nnreal_hom : ℝ≥0 →+* ℝ≥0∞)) }

noncomputable example : algebra ℝ≥0 ℝ≥0∞ := infer_instance

noncomputable example : distrib_mul_action ℝ≥0ˣ ℝ≥0∞ := infer_instance

lemma coe_smul {R} (r : R) (s : ℝ≥0) [has_smul R ℝ≥0] [has_smul R ℝ≥0∞]

[is_scalar_tower R ℝ≥0 ℝ≥0] [is_scalar_tower R ℝ≥0 ℝ≥0∞] :

(↑(r • s) : ℝ≥0∞) = r • ↑s :=

by rw [←smul_one_smul ℝ≥0 r (s: ℝ≥0∞), smul_def, smul_eq_mul, ←ennreal.coe_mul, smul_mul_assoc,

one_mul]

end actions

@[simp, norm_cast] lemma coe_indicator {α} (s : set α) (f : α → ℝ≥0) (a : α) :

((s.indicator f a : ℝ≥0) : ℝ≥0∞) = s.indicator (λ x, f x) a :=

(of_nnreal_hom : ℝ≥0 →+ ℝ≥0∞).map_indicator _ _ _

@[simp, norm_cast] lemma coe_pow (n : ℕ) : (↑(r^n) : ℝ≥0∞) = r^n :=

of_nnreal_hom.map_pow r n

@[simp] lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top

@[simp] lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top

lemma to_nnreal_add {r₁ r₂ : ℝ≥0∞} (h₁ : r₁ ≠ ∞) (h₂ : r₂ ≠ ∞) :

(r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal :=

by { lift r₁ to ℝ≥0 using h₁, lift r₂ to ℝ≥0 using h₂, refl }

lemma not_lt_top {x : ℝ≥0∞} : ¬ x < ∞ ↔ x = ∞ := by rw [lt_top_iff_ne_top, not_not]

lemma add_ne_top : a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞ :=

by simpa only [lt_top_iff_ne_top] using add_lt_top

lemma mul_top : a * ∞ = (if a = 0 then 0 else ∞) :=

begin split_ifs, { simp [h] }, { exact with_top.mul_top h } end

lemma top_mul : ∞ * a = (if a = 0 then 0 else ∞) :=

begin split_ifs, { simp [h] }, { exact with_top.top_mul h } end

@[simp] lemma top_mul_top : ∞ * ∞ = ∞ := with_top.top_mul_top

lemma smul_top {R} [has_zero R] [smul_with_zero R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞]

[no_zero_smul_divisors R ℝ≥0∞] (c : R) :

c • ∞ = (if c = 0 then 0 else ∞) :=

rw [←smul_one_mul, mul_top],

simp_rw [smul_eq_zero, or_iff_left one_ne_zero],

lemma top_pow {n:ℕ} (h : 0 < n) : ∞^n = ∞ :=

nat.le_induction (pow_one _) (λ m hm hm', by rw [pow_succ, hm', top_mul_top])

_ (nat.succ_le_of_lt h)

lemma mul_eq_top : a * b = ∞ ↔ (a ≠ 0 ∧ b = ∞) ∨ (a = ∞ ∧ b ≠ 0) :=

with_top.mul_eq_top_iff

lemma mul_lt_top : a ≠ ∞ → b ≠ ∞ → a * b < ∞ :=

with_top.mul_lt_top

lemma mul_ne_top : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ :=

by simpa only [lt_top_iff_ne_top] using mul_lt_top

lemma lt_top_of_mul_ne_top_left (h : a * b ≠ ∞) (hb : b ≠ 0) : a < ∞ :=

lt_top_iff_ne_top.2 $ λ ha, h $ mul_eq_top.2 (or.inr ⟨ha, hb⟩)

lemma lt_top_of_mul_ne_top_right (h : a * b ≠ ∞) (ha : a ≠ 0) : b < ∞ :=

lt_top_of_mul_ne_top_left (by rwa [mul_comm]) ha

lemma mul_lt_top_iff {a b : ℝ≥0∞} : a * b < ∞ ↔ (a < ∞ ∧ b < ∞) ∨ a = 0 ∨ b = 0 :=

split,

{ intro h, rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right], intros hb ha,

exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩ },

{ rintro (⟨ha, hb⟩|rfl|rfl); [exact mul_lt_top ha.ne hb.ne, simp, simp] }

lemma mul_self_lt_top_iff {a : ℝ≥0∞} : a * a < ⊤ ↔ a < ⊤ :=

by { rw [ennreal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp], rintro rfl, norm_num }

lemma mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b := canonically_ordered_comm_semiring.mul_pos

lemma mul_pos (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a * b :=

mul_pos_iff.2 ⟨pos_iff_ne_zero.2 ha, pos_iff_ne_zero.2 hb⟩

@[simp] lemma pow_eq_top_iff {n : ℕ} : a ^ n = ∞ ↔ a = ∞ ∧ n ≠ 0 :=

induction n with n ihn, { simp },

rw [pow_succ, mul_eq_top, ihn],

fsplit,

{ rintro (⟨-,rfl,h0⟩|⟨rfl,h0⟩); exact ⟨rfl, n.succ_ne_zero⟩ },

{ rintro ⟨rfl, -⟩, exact or.inr ⟨rfl, pow_ne_zero n top_ne_zero⟩ }

lemma pow_eq_top (n : ℕ) (h : a ^ n = ∞) : a = ∞ :=

(pow_eq_top_iff.1 h).1

lemma pow_ne_top (h : a ≠ ∞) {n:ℕ} : a^n ≠ ∞ :=

mt (pow_eq_top n) h

lemma pow_lt_top : a < ∞ → ∀ n:ℕ, a^n < ∞ :=

by simpa only [lt_top_iff_ne_top] using pow_ne_top

@[simp, norm_cast] lemma coe_finset_sum {s : finset α} {f : α → ℝ≥0} :

↑(∑ a in s, f a) = (∑ a in s, f a : ℝ≥0∞) :=

of_nnreal_hom.map_sum f s

@[simp, norm_cast] lemma coe_finset_prod {s : finset α} {f : α → ℝ≥0} :

↑(∏ a in s, f a) = ((∏ a in s, f a) : ℝ≥0∞) :=

of_nnreal_hom.map_prod f s

section order

@[simp] lemma bot_eq_zero : (⊥ : ℝ≥0∞) = 0 := rfl

@[simp] lemma coe_lt_top : coe r < ∞ := with_top.coe_lt_top r

@[simp] lemma not_top_le_coe : ¬ ∞ ≤ ↑r := with_top.not_top_le_coe r

@[simp, norm_cast] lemma one_le_coe_iff : (1:ℝ≥0∞) ≤ ↑r ↔ 1 ≤ r := coe_le_coe

@[simp, norm_cast] lemma coe_le_one_iff : ↑r ≤ (1:ℝ≥0∞) ↔ r ≤ 1 := coe_le_coe

@[simp, norm_cast] lemma coe_lt_one_iff : (↑p : ℝ≥0∞) < 1 ↔ p < 1 := coe_lt_coe

@[simp, norm_cast] lemma one_lt_coe_iff : 1 < (↑p : ℝ≥0∞) ↔ 1 < p := coe_lt_coe

@[simp, norm_cast] lemma coe_nat (n : ℕ) : ((n : ℝ≥0) : ℝ≥0∞) = n := with_top.coe_nat n

@[simp] lemma of_real_coe_nat (n : ℕ) : ennreal.of_real n = n := by simp [ennreal.of_real]

@[simp] lemma nat_ne_top (n : ℕ) : (n : ℝ≥0∞) ≠ ∞ := with_top.nat_ne_top n

@[simp] lemma top_ne_nat (n : ℕ) : ∞ ≠ n := with_top.top_ne_nat n

@[simp] lemma one_lt_top : 1 < ∞ := coe_lt_top

@[simp, norm_cast] lemma to_nnreal_nat (n : ℕ) : (n : ℝ≥0∞).to_nnreal = n :=

by conv_lhs { rw [← ennreal.coe_nat n, ennreal.to_nnreal_coe] }

@[simp, norm_cast] lemma to_real_nat (n : ℕ) : (n : ℝ≥0∞).to_real = n :=

by conv_lhs { rw [← ennreal.of_real_coe_nat n, ennreal.to_real_of_real (nat.cast_nonneg _)] }

lemma le_coe_iff : a ≤ ↑r ↔ (∃p:ℝ≥0, a = p ∧ p ≤ r) := with_top.le_coe_iff

lemma coe_le_iff : ↑r ≤ a ↔ (∀p:ℝ≥0, a = p → r ≤ p) := with_top.coe_le_iff

lemma lt_iff_exists_coe : a < b ↔ (∃p:ℝ≥0, a = p ∧ ↑p < b) := with_top.lt_iff_exists_coe

lemma to_real_le_coe_of_le_coe {a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ b) : a.to_real ≤ b :=

show ↑a.to_nnreal ≤ ↑b,

have : ↑a.to_nnreal = a := ennreal.coe_to_nnreal (lt_of_le_of_lt h coe_lt_top).ne,

rw ← this at h,

exact_mod_cast h

@[simp, norm_cast] lemma coe_finset_sup {s : finset α} {f : α → ℝ≥0} :

↑(s.sup f) = s.sup (λ x, (f x : ℝ≥0∞)) :=

finset.comp_sup_eq_sup_comp_of_is_total _ coe_mono rfl

@[simp] lemma max_eq_zero_iff : max a b = 0 ↔ a = 0 ∧ b = 0 :=

by simp only [nonpos_iff_eq_zero.symm, max_le_iff]

@[simp] lemma max_zero_left : max 0 a = a := max_eq_right (zero_le a)

@[simp] lemma max_zero_right : max a 0 = a := max_eq_left (zero_le a)

@[simp] lemma sup_eq_max : a ⊔ b = max a b :=

rfl

protected lemma pow_pos : 0 < a → ∀ n : ℕ, 0 < a^n :=

canonically_ordered_comm_semiring.pow_pos

protected lemma pow_ne_zero : a ≠ 0 → ∀ n : ℕ, a^n ≠ 0 :=

by simpa only [pos_iff_ne_zero] using ennreal.pow_pos

@[simp] lemma not_lt_zero : ¬ a < 0 := by simp

protected lemma le_of_add_le_add_left : a ≠ ∞ → a + b ≤ a + c → b ≤ c :=

with_top.le_of_add_le_add_left

protected lemma le_of_add_le_add_right : a ≠ ∞ → b + a ≤ c + a → b ≤ c :=

with_top.le_of_add_le_add_right

protected lemma add_lt_add_left : a ≠ ∞ → b < c → a + b < a + c := with_top.add_lt_add_left

protected lemma add_lt_add_right : a ≠ ∞ → b < c → b + a < c + a := with_top.add_lt_add_right

protected lemma add_le_add_iff_left : a ≠ ∞ → (a + b ≤ a + c ↔ b ≤ c) :=

with_top.add_le_add_iff_left

protected lemma add_le_add_iff_right : a ≠ ∞ → (b + a ≤ c + a ↔ b ≤ c) :=

with_top.add_le_add_iff_right

protected lemma add_lt_add_iff_left : a ≠ ∞ → (a + b < a + c ↔ b < c) :=

with_top.add_lt_add_iff_left

protected lemma add_lt_add_iff_right : a ≠ ∞ → (b + a < c + a ↔ b < c) :=

with_top.add_lt_add_iff_right

protected lemma add_lt_add_of_le_of_lt : a ≠ ∞ → a ≤ b → c < d → a + c < b + d :=

with_top.add_lt_add_of_le_of_lt

protected lemma add_lt_add_of_lt_of_le : c ≠ ∞ → a < b → c ≤ d → a + c < b + d :=

with_top.add_lt_add_of_lt_of_le

instance contravariant_class_add_lt : contravariant_class ℝ≥0∞ ℝ≥0∞ (+) (<) :=

with_top.contravariant_class_add_lt

lemma lt_add_right (ha : a ≠ ∞) (hb : b ≠ 0) : a < a + b :=

by rwa [← pos_iff_ne_zero, ←ennreal.add_lt_add_iff_left ha, add_zero] at hb

lemma le_of_forall_pos_le_add : ∀{a b : ℝ≥0∞}, (∀ε : ℝ≥0, 0 < ε → b < ∞ → a ≤ b + ε) → a ≤ b

| a none h := le_top

| none (some a) h :=

have ∞ ≤ ↑a + ↑(1:ℝ≥0), from h 1 zero_lt_one coe_lt_top,

by rw [← coe_add] at this; exact (not_top_le_coe this).elim

| (some a) (some b) h :=

by simp only [none_eq_top, some_eq_coe, coe_add.symm, coe_le_coe, coe_lt_top, true_implies_iff]

at *; exact nnreal.le_of_forall_pos_le_add h

lemma lt_iff_exists_rat_btwn :

a < b ↔ (∃q:ℚ, 0 ≤ q ∧ a < real.to_nnreal q ∧ (real.to_nnreal q:ℝ≥0∞) < b) :=

⟨λ h,

begin

rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩,

rcases exists_between h with ⟨c, pc, cb⟩,

rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩,

rcases (nnreal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩,

exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩

end,

λ ⟨q, q0, qa, qb⟩, lt_trans qa qb⟩

lemma lt_iff_exists_real_btwn :

a < b ↔ (∃r:ℝ, 0 ≤ r ∧ a < ennreal.of_real r ∧ (ennreal.of_real r:ℝ≥0∞) < b) :=

⟨λ h, let ⟨q, q0, aq, qb⟩ := ennreal.lt_iff_exists_rat_btwn.1 h in

⟨q, rat.cast_nonneg.2 q0, aq, qb⟩,

λ ⟨q, q0, qa, qb⟩, lt_trans qa qb⟩

lemma lt_iff_exists_nnreal_btwn :

a < b ↔ (∃r:ℝ≥0, a < r ∧ (r : ℝ≥0∞) < b) :=

with_top.lt_iff_exists_coe_btwn

lemma lt_iff_exists_add_pos_lt : a < b ↔ (∃ r : ℝ≥0, 0 < r ∧ a + r < b) :=

refine ⟨λ hab, _, λ ⟨r, rpos, hr⟩, lt_of_le_of_lt (le_self_add) hr⟩,

cases a, { simpa using hab },

rcases lt_iff_exists_real_btwn.1 hab with ⟨c, c_nonneg, ac, cb⟩,

let d : ℝ≥0 := ⟨c, c_nonneg⟩,

have ad : a < d,

{ rw of_real_eq_coe_nnreal c_nonneg at ac,

exact coe_lt_coe.1 ac },

refine ⟨d-a, tsub_pos_iff_lt.2 ad, _⟩,

rw [some_eq_coe, ← coe_add],

convert cb,

have : real.to_nnreal c = d,

by { rw [← nnreal.coe_eq, real.coe_to_nnreal _ c_nonneg], refl },

rw [add_comm, this],

exact tsub_add_cancel_of_le ad.le

@[simp, norm_cast] lemma coe_nat_lt_coe {n : ℕ} : (n : ℝ≥0∞) < r ↔ ↑n < r :=

ennreal.coe_nat n ▸ coe_lt_coe

@[simp, norm_cast] lemma coe_lt_coe_nat {n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n :=

ennreal.coe_nat n ▸ coe_lt_coe

protected lemma exists_nat_gt {r : ℝ≥0∞} (h : r ≠ ∞) : ∃n:ℕ, r < n :=

lift r to ℝ≥0 using h,

rcases exists_nat_gt r with ⟨n, hn⟩,

exact ⟨n, coe_lt_coe_nat.2 hn⟩,

@[simp] lemma Union_Iio_coe_nat : (⋃ n : ℕ, Iio (n : ℝ≥0∞)) = {∞}ᶜ :=

ext x,

rw [mem_Union],

exact ⟨λ ⟨n, hn⟩, ne_top_of_lt hn, ennreal.exists_nat_gt⟩

@[simp] lemma Union_Iic_coe_nat : (⋃ n : ℕ, Iic (n : ℝ≥0∞)) = {∞}ᶜ :=

subset.antisymm (Union_subset $ λ n x hx, ne_top_of_le_ne_top (nat_ne_top n) hx) $

Union_Iio_coe_nat ▸ Union_mono (λ n, Iio_subset_Iic_self)

@[simp] lemma Union_Ioc_coe_nat : (⋃ n : ℕ, Ioc a n) = Ioi a \ {∞} :=

by simp only [← Ioi_inter_Iic, ← inter_Union, Union_Iic_coe_nat, diff_eq]

@[simp] lemma Union_Ioo_coe_nat : (⋃ n : ℕ, Ioo a n) = Ioi a \ {∞} :=

by simp only [← Ioi_inter_Iio, ← inter_Union, Union_Iio_coe_nat, diff_eq]

@[simp] lemma Union_Icc_coe_nat : (⋃ n : ℕ, Icc a n) = Ici a \ {∞} :=

by simp only [← Ici_inter_Iic, ← inter_Union, Union_Iic_coe_nat, diff_eq]

@[simp] lemma Union_Ico_coe_nat : (⋃ n : ℕ, Ico a n) = Ici a \ {∞} :=

by simp only [← Ici_inter_Iio, ← inter_Union, Union_Iio_coe_nat, diff_eq]

@[simp] lemma Inter_Ici_coe_nat : (⋂ n : ℕ, Ici (n : ℝ≥0∞)) = {∞} :=

by simp only [← compl_Iio, ← compl_Union, Union_Iio_coe_nat, compl_compl]

@[simp] lemma Inter_Ioi_coe_nat : (⋂ n : ℕ, Ioi (n : ℝ≥0∞)) = {∞} :=

by simp only [← compl_Iic, ← compl_Union, Union_Iic_coe_nat, compl_compl]

lemma add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d :=

lift a to ℝ≥0 using ne_top_of_lt ac,

lift b to ℝ≥0 using ne_top_of_lt bd,

cases c, { simp }, cases d, { simp },

simp only [← coe_add, some_eq_coe, coe_lt_coe] at *,

exact add_lt_add ac bd

@[norm_cast] lemma coe_min : ((min r p:ℝ≥0):ℝ≥0∞) = min r p :=

coe_mono.map_min

@[norm_cast] lemma coe_max : ((max r p:ℝ≥0):ℝ≥0∞) = max r p :=

coe_mono.map_max

lemma le_of_top_imp_top_of_to_nnreal_le {a b : ℝ≥0∞} (h : a = ⊤ → b = ⊤)

(h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.to_nnreal ≤ b.to_nnreal) :

a ≤ b :=

by_cases ha : a = ⊤,

{ rw h ha,

exact le_top, },

by_cases hb : b = ⊤,

{ rw hb,

exact le_top, },

rw [←coe_to_nnreal hb, ←coe_to_nnreal ha, coe_le_coe],

exact h_nnreal ha hb,

end order

section complete_lattice

lemma coe_Sup {s : set ℝ≥0} : bdd_above s → (↑(Sup s) : ℝ≥0∞) = (⨆a∈s, ↑a) := with_top.coe_Sup

lemma coe_Inf {s : set ℝ≥0} : s.nonempty → (↑(Inf s) : ℝ≥0∞) = (⨅a∈s, ↑a) := with_top.coe_Inf

lemma coe_supr {ι : Sort*} {f : ι → ℝ≥0} (hf : bdd_above (range f)) :

(↑(supr f) : ℝ≥0∞) = ⨆a, ↑(f a) :=

with_top.coe_supr _ hf

lemma coe_infi {ι : Sort*} [nonempty ι] (f : ι → ℝ≥0) : (↑(infi f) : ℝ≥0∞) = (⨅ a, ↑(f a)) :=

with_top.coe_infi f

lemma coe_mem_upper_bounds {s : set ℝ≥0} :

↑r ∈ upper_bounds ((coe : ℝ≥0 → ℝ≥0∞) '' s) ↔ r ∈ upper_bounds s :=

by simp [upper_bounds, ball_image_iff, -mem_image, *] {contextual := tt}

end complete_lattice

section mul

@[mono] lemma mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d :=

rcases lt_iff_exists_nnreal_btwn.1 ac with ⟨a', aa', a'c⟩,

lift a to ℝ≥0 using ne_top_of_lt aa',

rcases lt_iff_exists_nnreal_btwn.1 bd with ⟨b', bb', b'd⟩,

lift b to ℝ≥0 using ne_top_of_lt bb',

norm_cast at *,

calc ↑(a * b) < ↑(a' * b') :

coe_lt_coe.2 (mul_lt_mul' aa'.le bb' (zero_le _) ((zero_le a).trans_lt aa'))

... = ↑a' * ↑b' : coe_mul

... ≤ c * d : mul_le_mul' a'c.le b'd.le

lemma mul_left_mono : monotone ((*) a) := λ b c, mul_le_mul' le_rfl

lemma mul_right_mono : monotone (λ x, x * a) := λ b c h, mul_le_mul' h le_rfl

lemma pow_strict_mono {n : ℕ} (hn : n ≠ 0) : strict_mono (λ (x : ℝ≥0∞), x^n) :=

assume x y hxy,

obtain ⟨n, rfl⟩ := nat.exists_eq_succ_of_ne_zero hn,

induction n with n IH,

{ simp only [hxy, pow_one] },

{ simp only [pow_succ _ n.succ, mul_lt_mul hxy (IH (nat.succ_pos _).ne')] }

lemma max_mul : max a b * c = max (a * c) (b * c) :=

mul_right_mono.map_max

lemma mul_max : a * max b c = max (a * b) (a * c) :=

mul_left_mono.map_max

theorem mul_left_strictMono (h0 : a ≠ 0) (hinf : a ≠ ∞) : strict_mono ((*) a) :=

lift a to ℝ≥0 using hinf,

rw [coe_ne_zero] at h0,

intros x y h,

contrapose! h,

simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel h0, coe_one, one_mul]

using mul_le_mul_left' h (↑a⁻¹)

lemma mul_eq_mul_left (h₀ : a ≠ 0) (hinf : a ≠ ∞) : a * b = a * c ↔ b = c :=

(mul_left_strictMono h₀ hinf).injective.eq_iff

lemma mul_eq_mul_right : c ≠ 0 → c ≠ ∞ → (a * c = b * c ↔ a = b) :=

mul_comm c a ▸ mul_comm c b ▸ mul_eq_mul_left

lemma mul_le_mul_left (h₀ : a ≠ 0) (hinf : a ≠ ∞) : a * b ≤ a * c ↔ b ≤ c :=

(mul_left_strictMono h₀ hinf).le_iff_le

lemma mul_le_mul_right : c ≠ 0 → c ≠ ∞ → (a * c ≤ b * c ↔ a ≤ b) :=

mul_comm c a ▸ mul_comm c b ▸ mul_le_mul_left

lemma mul_lt_mul_left (h₀ : a ≠ 0) (hinf : a ≠ ∞) : a * b < a * c ↔ b < c :=

(mul_left_strictMono h₀ hinf).lt_iff_lt

lemma mul_lt_mul_right : c ≠ 0 → c ≠ ∞ → (a * c < b * c ↔ a < b) :=

mul_comm c a ▸ mul_comm c b ▸ mul_lt_mul_left

end mul

section cancel

lemma add_le_cancellable_iff_ne {a : ℝ≥0∞} : add_le_cancellable a ↔ a ≠ ∞ :=

split,

{ rintro h rfl, refine zero_lt_one.not_le (h _), simp, },

{ rintro h b c hbc, apply ennreal.le_of_add_le_add_left h hbc }

lemma cancel_of_ne {a : ℝ≥0∞} (h : a ≠ ∞) : add_le_cancellable a :=

add_le_cancellable_iff_ne.mpr h

lemma cancel_of_lt {a : ℝ≥0∞} (h : a < ∞) : add_le_cancellable a :=

cancel_of_ne h.ne

lemma cancel_of_lt' {a b : ℝ≥0∞} (h : a < b) : add_le_cancellable a :=

cancel_of_ne h.ne_top

lemma cancel_coe {a : ℝ≥0} : add_le_cancellable (a : ℝ≥0∞) :=

cancel_of_ne coe_ne_top

lemma add_right_inj (h : a ≠ ∞) : a + b = a + c ↔ b = c :=

(cancel_of_ne h).inj

lemma add_left_inj (h : a ≠ ∞) : b + a = c + a ↔ b = c :=

(cancel_of_ne h).inj_left

end cancel

section sub

lemma sub_eq_Inf {a b : ℝ≥0∞} : a - b = Inf {d | a ≤ d + b} :=

le_antisymm (le_Inf $ λ c, tsub_le_iff_right.mpr) $ Inf_le le_tsub_add

lemma coe_sub : (↑(r - p) : ℝ≥0∞) = ↑r - ↑p :=

with_top.coe_sub

lemma top_sub_coe : ∞ - ↑r = ∞ :=

with_top.top_sub_coe

lemma sub_top : a - ∞ = 0 :=

with_top.sub_top

lemma sub_eq_top_iff : a - b = ∞ ↔ a = ∞ ∧ b ≠ ∞ :=

by { cases a; cases b; simp [← with_top.coe_sub] }

lemma sub_ne_top (ha : a ≠ ∞) : a - b ≠ ∞ :=

mt sub_eq_top_iff.mp $ mt and.left ha

@[simp, norm_cast] lemma nat_cast_sub (m n : ℕ) : ↑(m - n) = (m - n : ℝ≥0∞) :=

by rw [← coe_nat, nat.cast_tsub, coe_sub, coe_nat, coe_nat]

protected lemma sub_eq_of_eq_add (hb : b ≠ ∞) : a = c + b → a - b = c :=

(cancel_of_ne hb).tsub_eq_of_eq_add

protected lemma eq_sub_of_add_eq (hc : c ≠ ∞) : a + c = b → a = b - c :=

(cancel_of_ne hc).eq_tsub_of_add_eq

protected lemma sub_eq_of_eq_add_rev (hb : b ≠ ∞) : a = b + c → a - b = c :=

(cancel_of_ne hb).tsub_eq_of_eq_add_rev

lemma sub_eq_of_add_eq (hb : b ≠ ∞) (hc : a + b = c) : c - b = a :=

ennreal.sub_eq_of_eq_add hb hc.symm

@[simp] protected lemma add_sub_cancel_left (ha : a ≠ ∞) : a + b - a = b :=

(cancel_of_ne ha).add_tsub_cancel_left

@[simp] protected lemma add_sub_cancel_right (hb : b ≠ ∞) : a + b - b = a :=

(cancel_of_ne hb).add_tsub_cancel_right

protected lemma lt_add_of_sub_lt_left (h : a ≠ ∞ ∨ b ≠ ∞) : a - b < c → a < b + c :=

obtain rfl | hb := eq_or_ne b ∞,

{ rw [top_add, lt_top_iff_ne_top],

exact λ _, h.resolve_right (not_not.2 rfl) },

{ exact (cancel_of_ne hb).lt_add_of_tsub_lt_left }

protected lemma lt_add_of_sub_lt_right (h : a ≠ ∞ ∨ c ≠ ∞) : a - c < b → a < b + c :=

add_comm c b ▸ ennreal.lt_add_of_sub_lt_left h

lemma le_sub_of_add_le_left (ha : a ≠ ∞) : a + b ≤ c → b ≤ c - a :=

(cancel_of_ne ha).le_tsub_of_add_le_left

lemma le_sub_of_add_le_right (hb : b ≠ ∞) : a + b ≤ c → a ≤ c - b :=

(cancel_of_ne hb).le_tsub_of_add_le_right

protected lemma sub_lt_of_lt_add (hac : c ≤ a) (h : a < b + c) : a - c < b :=

((cancel_of_lt' $ hac.trans_lt h).tsub_lt_iff_right hac).mpr h

protected lemma sub_lt_iff_lt_right (hb : b ≠ ∞) (hab : b ≤ a) : a - b < c ↔ a < c + b :=

(cancel_of_ne hb).tsub_lt_iff_right hab

protected lemma sub_lt_self (ha : a ≠ ∞) (ha₀ : a ≠ 0) (hb : b ≠ 0) : a - b < a :=

(cancel_of_ne ha).tsub_lt_self (pos_iff_ne_zero.2 ha₀) (pos_iff_ne_zero.2 hb)

protected lemma sub_lt_self_iff (ha : a ≠ ∞) : a - b < a ↔ 0 < a ∧ 0 < b :=

(cancel_of_ne ha).tsub_lt_self_iff

lemma sub_lt_of_sub_lt (h₂ : c ≤ a) (h₃ : a ≠ ∞ ∨ b ≠ ∞) (h₁ : a - b < c) : a - c < b :=

ennreal.sub_lt_of_lt_add h₂ (add_comm c b ▸ ennreal.lt_add_of_sub_lt_right h₃ h₁)

lemma sub_sub_cancel (h : a ≠ ∞) (h2 : b ≤ a) : a - (a - b) = b :=

(cancel_of_ne $ sub_ne_top h).tsub_tsub_cancel_of_le h2

lemma sub_right_inj {a b c : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≤ a) (hc : c ≤ a) :

a - b = a - c ↔ b = c :=

(cancel_of_ne ha).tsub_right_inj (cancel_of_ne $ ne_top_of_le_ne_top ha hb)

(cancel_of_ne $ ne_top_of_le_ne_top ha hc) hb hc

lemma sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c :=

cases le_or_lt a b with hab hab, { simp [hab, mul_right_mono hab] },

rcases eq_or_lt_of_le (zero_le b) with rfl|hb, { simp },

exact (cancel_of_ne $ mul_ne_top hab.ne_top (h hb hab)).tsub_mul

lemma mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c :=

by { simp only [mul_comm a], exact sub_mul h }

end sub

section sum

open finset

lemma prod_lt_top {s : finset α} {f : α → ℝ≥0∞} (h : ∀ a ∈ s, f a ≠ ∞) : (∏ a in s, f a) < ∞ :=

with_top.prod_lt_top h

lemma sum_lt_top {s : finset α} {f : α → ℝ≥0∞} (h : ∀ a ∈ s, f a ≠ ∞) : ∑ a in s, f a < ∞ :=

with_top.sum_lt_top h

lemma sum_lt_top_iff {s : finset α} {f : α → ℝ≥0∞} :

∑ a in s, f a < ∞ ↔ (∀ a ∈ s, f a < ∞) :=

with_top.sum_lt_top_iff

lemma sum_eq_top_iff {s : finset α} {f : α → ℝ≥0∞} :

(∑ x in s, f x) = ∞ ↔ (∃ a ∈ s, f a = ∞) :=

with_top.sum_eq_top_iff

lemma lt_top_of_sum_ne_top {s : finset α} {f : α → ℝ≥0∞} (h : (∑ x in s, f x) ≠ ∞) {a : α}

(ha : a ∈ s) : f a < ∞ :=

sum_lt_top_iff.1 h.lt_top a ha

lemma to_nnreal_sum {s : finset α} {f : α → ℝ≥0∞} (hf : ∀a∈s, f a ≠ ∞) :

ennreal.to_nnreal (∑ a in s, f a) = ∑ a in s, ennreal.to_nnreal (f a) :=

rw [← coe_eq_coe, coe_to_nnreal, coe_finset_sum, sum_congr rfl],

{ intros x hx, exact (coe_to_nnreal (hf x hx)).symm },

{ exact (sum_lt_top hf).ne }

lemma to_real_sum {s : finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :

ennreal.to_real (∑ a in s, f a) = ∑ a in s, ennreal.to_real (f a) :=

by { rw [ennreal.to_real, to_nnreal_sum hf, nnreal.coe_sum], refl }

lemma of_real_sum_of_nonneg {s : finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :

ennreal.of_real (∑ i in s, f i) = ∑ i in s, ennreal.of_real (f i) :=

simp_rw [ennreal.of_real, ←coe_finset_sum, coe_eq_coe],

exact real.to_nnreal_sum_of_nonneg hf,

theorem sum_lt_sum_of_nonempty {s : finset α} (hs : s.nonempty)

{f g : α → ℝ≥0∞} (Hlt : ∀ i ∈ s, f i < g i) :

∑ i in s, f i < ∑ i in s, g i :=

induction hs using finset.nonempty.cons_induction with a a s as hs IH,

{ simp [Hlt _ (finset.mem_singleton_self _)] },

{ simp only [as, finset.sum_cons, not_false_iff],

exact ennreal.add_lt_add (Hlt _ (finset.mem_cons_self _ _))

(IH (λ i hi, Hlt _ (finset.mem_cons.2 $ or.inr hi))) }

theorem exists_le_of_sum_le {s : finset α} (hs : s.nonempty)

{f g : α → ℝ≥0∞} (Hle : ∑ i in s, f i ≤ ∑ i in s, g i) :

∃ i ∈ s, f i ≤ g i :=

contrapose! Hle,

apply ennreal.sum_lt_sum_of_nonempty hs Hle,

end sum

section interval

variables {x y z : ℝ≥0∞} {ε ε₁ ε₂ : ℝ≥0∞} {s : set ℝ≥0∞}

protected lemma Ico_eq_Iio : (Ico 0 y) = (Iio y) := Ico_bot

lemma mem_Iio_self_add : x ≠ ∞ → ε ≠ 0 → x ∈ Iio (x + ε) :=

assume xt ε0, lt_add_right xt ε0

lemma mem_Ioo_self_sub_add : x ≠ ∞ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Ioo (x - ε₁) (x + ε₂) :=

assume xt x0 ε0 ε0', ⟨ennreal.sub_lt_self xt x0 ε0, lt_add_right xt ε0'⟩

end interval

section bit

@[mono] lemma bit0_strict_mono : strict_mono (bit0 : ℝ≥0∞ → ℝ≥0∞) := λ a b h, add_lt_add h h

lemma bit0_injective : function.injective (bit0 : ℝ≥0∞ → ℝ≥0∞) := bit0_strict_mono.injective

@[simp] lemma bit0_lt_bit0 : bit0 a < bit0 b ↔ a < b := bit0_strict_mono.lt_iff_lt

@[simp, mono] lemma bit0_le_bit0 : bit0 a ≤ bit0 b ↔ a ≤ b := bit0_strict_mono.le_iff_le

@[simp] lemma bit0_inj : bit0 a = bit0 b ↔ a = b := bit0_injective.eq_iff

@[simp] lemma bit0_eq_zero_iff : bit0 a = 0 ↔ a = 0 := bit0_injective.eq_iff' bit0_zero

@[simp] lemma bit0_top : bit0 ∞ = ∞ := add_top _

@[simp] lemma bit0_eq_top_iff : bit0 a = ∞ ↔ a = ∞ := bit0_injective.eq_iff' bit0_top

@[mono] lemma bit1_strict_mono : strict_mono (bit1 : ℝ≥0∞ → ℝ≥0∞) :=

λ a b h, ennreal.add_lt_add_right one_ne_top (bit0_strict_mono h)

lemma bit1_injective : function.injective (bit1 : ℝ≥0∞ → ℝ≥0∞) := bit1_strict_mono.injective

@[simp] lemma bit1_lt_bit1 : bit1 a < bit1 b ↔ a < b := bit1_strict_mono.lt_iff_lt

@[simp, mono] lemma bit1_le_bit1 : bit1 a ≤ bit1 b ↔ a ≤ b := bit1_strict_mono.le_iff_le

@[simp] lemma bit1_inj : bit1 a = bit1 b ↔ a = b := bit1_injective.eq_iff

@[simp] lemma bit1_ne_zero : bit1 a ≠ 0 := by simp [bit1]

@[simp] lemma bit1_top : bit1 ∞ = ∞ := by rw [bit1, bit0_top, top_add]

@[simp] lemma bit1_eq_top_iff : bit1 a = ∞ ↔ a = ∞ := bit1_injective.eq_iff' bit1_top

@[simp] lemma bit1_eq_one_iff : bit1 a = 1 ↔ a = 0 := bit1_injective.eq_iff' bit1_zero