feat(topology/ennreal): add extended non-negative real numbers

Author: johoelzl

algebra/big_operators.lean

@@ -255,10 +255,10 @@ section semiring
 variables [semiring β]
 
 lemma sum_mul : s.sum f * b = s.sum (λx, f x * b) :=
-(sum_hom (λx, x * b) (zero_mul b) (assume a b, add_mul _ _ _)).symm
+(sum_hom (λx, x * b) (zero_mul b) (assume a c, add_mul a c b)).symm
 
 lemma mul_sum : b * s.sum f = s.sum (λx, b * f x) :=
-(sum_hom (λx, b * x) (mul_zero b) (assume a b, mul_add _ _ _)).symm
+(sum_hom (λx, b * x) (mul_zero b) (assume a c, mul_add b a c)).symm
 
 end semiring
 

topology/ennreal.lean

@@ -0,0 +1,377 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Johannes Hölzl
+
+Extended non-negative reals
+-/
+import order.bounds topology.real
+noncomputable theory
+open classical set lattice
+local attribute [instance] decidable_inhabited prop_decidable
+
+universe u
+-- TODO: this is necessary additionally to mul_nonneg otherwise the simplifier can not match
+lemma zero_le_mul {α : Type u} [ordered_semiring α] {a b : α} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
+mul_nonneg
+
+inductive ennreal : Type
+| of_nonneg_real : Πr:real, 0 ≤ r → ennreal
+| infinity : ennreal
+
+local notation `∞` := ennreal.infinity
+
+namespace ennreal
+variables {a b c d : ennreal} {r p q : ℝ}
+
+section projections
+
+def of_real (r : ℝ) : ennreal := of_nonneg_real (max 0 r) (le_max_left 0 r)
+
+def of_ennreal : ennreal → ℝ
+| (of_nonneg_real r _) := r
+| ∞ := 0
+
+@[simp] lemma of_ennreal_of_real (h : 0 ≤ r) : of_ennreal (of_real r) = r := max_eq_right h
+
+lemma zero_le_of_ennreal : ∀{a}, 0 ≤ of_ennreal a
+| (of_nonneg_real r hr) := hr
+| ∞ := le_refl 0
+
+@[simp] lemma of_real_of_ennreal : ∀{a}, a ≠ ∞ → of_real (of_ennreal a) = a
+| (of_nonneg_real r hr) h := by simp [of_real, of_ennreal, max, hr]
+| ∞ h := false.elim $ h rfl
+
+lemma forall_ennreal {p : ennreal → Prop} : (∀a, p a) ↔ (∀r (h : 0 ≤ r), p (of_real r)) ∧ p ∞ :=
+⟨assume h, ⟨assume r hr, h _, h _⟩,
+  assume ⟨h₁, h₂⟩, ennreal.rec
+    begin
+      intros r hr,
+      let h₁ := h₁ r hr,
+      simp [of_real, max, hr] at h₁,
+      exact h₁
+    end
+    h₂⟩
+
+end projections
+
+section semiring
+
+instance : has_zero ennreal := ⟨of_real 0⟩
+instance : has_one ennreal := ⟨of_real 1⟩
+instance : inhabited ennreal := ⟨0⟩
+
+@[simp] lemma of_real_zero : of_real 0 = 0 := rfl
+@[simp] lemma of_real_one : of_real 1 = 1 := rfl
+
+@[simp] lemma zero_ne_infty : 0 ≠ ∞ := assume h, ennreal.no_confusion h
+@[simp] lemma infty_ne_zero : ∞ ≠ 0 := assume h, ennreal.no_confusion h
+
+@[simp] lemma of_real_ne_infty : of_real r ≠ ∞ := assume h, ennreal.no_confusion h
+@[simp] lemma infty_ne_of_real : ∞ ≠ of_real r := assume h, ennreal.no_confusion h
+
+@[simp] lemma of_real_eq_of_real_of (hr : 0 ≤ r) (hq : 0 ≤ q) : of_real r = of_real q ↔ r = q :=
+by simp [of_real, max, hr, hq]; exact ⟨ennreal.of_nonneg_real.inj, by simp {contextual := tt}⟩
+
+lemma of_real_ne_of_real_of (hr : 0 ≤ r) (hq : 0 ≤ q) : of_real r ≠ of_real q ↔ r ≠ q :=
+by simp [hr, hq]
+
+instance : zero_ne_one_class ennreal :=
+{ zero := 0, one := 1, zero_ne_one := (of_real_ne_of_real_of (le_refl 0) zero_le_one).mpr zero_ne_one }
+
+@[simp] lemma of_real_eq_zero_iff (hr : 0 ≤ r) : of_real r = 0 ↔ r = 0 :=
+of_real_eq_of_real_of hr (le_refl 0)
+
+@[simp] lemma zero_eq_of_real_iff (hr : 0 ≤ r) : 0 = of_real r ↔ 0 = r :=
+of_real_eq_of_real_of (le_refl 0) hr
+
+@[simp] lemma of_real_eq_one_iff : of_real r = 1 ↔ r = 1 :=
+by_cases (assume : 0 ≤ r, of_real_eq_of_real_of this zero_le_one) $
+  assume : ¬ 0 ≤ r,
+  have r < 0, from lt_of_not_ge this,
+  have of_real r = of_real 0, by simp [of_real, max_eq_left_of_lt ‹r<0›],
+  have r ≠ 1, from assume h, ‹¬ 0 ≤ r› $ h.symm ▸ zero_le_one,
+  by rw [‹of_real r = of_real 0›]; simp [this]
+
+@[simp] lemma one_eq_of_real_iff : 1 = of_real r ↔ 1 = r :=
+by rw [eq_comm, of_real_eq_one_iff, eq_comm]
+
+lemma of_nonneg_real_eq_of_real (hr : 0 ≤ r) : of_nonneg_real r hr = of_real r :=
+by simp [of_real, hr, max]
+
+protected def add : ennreal → ennreal → ennreal
+| (of_nonneg_real a ha) (of_nonneg_real b hb) := of_real (a + b)
+| _ _ := ∞
+
+protected def mul : ennreal → ennreal → ennreal
+| (of_nonneg_real a ha) (of_nonneg_real b hb) := of_real (a * b)
+| ∞ (of_nonneg_real b hb) := if b = 0 then 0 else ∞
+| (of_nonneg_real a ha) ∞ := if a = 0 then 0 else ∞
+| _ _ := ∞
+
+instance : has_add ennreal := ⟨ennreal.add⟩
+instance : has_mul ennreal := ⟨ennreal.mul⟩
+
+@[simp] lemma of_real_add_of_real (hr : 0 ≤ r) (hq : 0 ≤ p) :
+  of_real r + of_real p = of_real (r + p) :=
+by simp [of_real, max, hr, hq]; refl
+
+@[simp] lemma add_infty : a + ∞ = ∞ :=
+by cases a; refl
+
+@[simp] lemma infty_add : ∞ + a = ∞ :=
+by cases a; refl
+
+@[simp] lemma of_real_mul_of_real (hr : 0 ≤ r) (hq : 0 ≤ p) :
+  of_real r * of_real p = of_real (r * p) :=
+by simp [of_real, max, hr, hq]; refl
+
+@[simp] lemma of_real_mul_infty (hr : 0 ≤ r) : of_real r * ∞ = (if r = 0 then 0 else ∞) :=
+by simp [of_real, max, hr]; refl
+
+@[simp] lemma infty_mul_of_real (hr : 0 ≤ r) : ∞ * of_real r = (if r = 0 then 0 else ∞) :=
+by simp [of_real, max, hr]; refl
+
+@[simp] lemma mul_infty : ∀{a}, a * ∞ = (if a = 0 then 0 else ∞) :=
+forall_ennreal.mpr ⟨assume r hr, by simp [hr]; by_cases r = 0; simp [h], by simp; refl⟩
+
+@[simp] lemma infty_mul : ∀{a}, ∞ * a = (if a = 0 then 0 else ∞) :=
+forall_ennreal.mpr ⟨assume r hr, by simp [hr]; by_cases r = 0; simp [h], by simp; refl⟩
+
+instance : add_comm_monoid ennreal :=
+{ add_comm_monoid .
+  zero := 0,
+  add  := (+),
+  add_zero := by simp [forall_ennreal, -of_real_zero, of_real_zero.symm] {contextual:=tt},
+  zero_add := by simp [forall_ennreal, -of_real_zero, of_real_zero.symm] {contextual:=tt},
+  add_comm := by simp [forall_ennreal, le_add_of_le_of_nonneg] {contextual:=tt},
+  add_assoc := by simp [forall_ennreal, le_add_of_le_of_nonneg] {contextual:=tt} }
+
+protected lemma mul_zero : ∀a:ennreal, a * 0 = 0 :=
+by simp [forall_ennreal, -of_real_zero, of_real_zero.symm] {contextual := tt}
+
+protected lemma mul_comm : ∀a b:ennreal, a * b = b * a :=
+by simp [forall_ennreal] {contextual := tt}
+
+protected lemma zero_mul : ∀a:ennreal, 0 * a = 0 :=
+by simp [forall_ennreal, -of_real_zero, of_real_zero.symm] {contextual := tt}
+
+protected lemma mul_assoc : ∀a b c:ennreal, a * b * c = a * (b * c) :=
+begin
+  rw [forall_ennreal], constructor,
+  { intros ra ha,
+    by_cases ra = 0 with ha', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    rw [forall_ennreal], constructor,
+    { intros rb hrb,
+      by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+      rw [forall_ennreal], constructor,
+      { intros rc hrc, simp [*, zero_le_mul] },
+      simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
+    rw [forall_ennreal], constructor,
+      { intros rc hrc,
+        by_cases rc = 0 with hc', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+        simp [*, zero_le_mul] },
+    simp [*] },
+  rw [forall_ennreal], constructor,
+  { intros rb hrb,
+    by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    rw [forall_ennreal], constructor,
+    { intros rc hrc,
+      by_cases rc = 0 with hb';
+        simp [*, zero_le_mul, ennreal.mul_zero, mul_eq_zero_iff_eq_zero_or_eq_zero] },
+    simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
+  intro c, by_cases c = 0; simp [*]
+end
+
+protected lemma left_distrib : ∀a b c:ennreal, a * (b + c) = a * b + a * c :=
+begin
+  rw [forall_ennreal], constructor,
+  { intros ra ha,
+    by_cases ra = 0 with ha', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    rw [forall_ennreal], constructor,
+    { intros rb hrb,
+      by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+      rw [forall_ennreal], constructor,
+      { intros rc hrc, simp [*, zero_le_mul, add_nonneg, left_distrib] },
+      simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
+    rw [forall_ennreal], constructor,
+      { intros rc hrc,
+        by_cases rc = 0 with hc', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+        simp [*, zero_le_mul] },
+    simp [*] },
+  rw [forall_ennreal], constructor,
+  { intros rb hrb,
+    by_cases rb = 0 with hb', simp [*, ennreal.mul_zero, ennreal.zero_mul],
+    rw [forall_ennreal], constructor,
+    { intros rc hrc,
+      by_cases rc = 0 with hb';
+        simp [*, zero_le_mul, ennreal.mul_zero, mul_eq_zero_iff_eq_zero_or_eq_zero, add_nonneg,
+          add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg] },
+    simp [*, zero_le_mul, mul_eq_zero_iff_eq_zero_or_eq_zero] },
+  intro c, by_cases c = 0; simp [*]
+end
+
+instance : comm_semiring ennreal :=
+{ ennreal.add_comm_monoid with
+  one  := 1,
+  mul  := (*),
+  mul_zero := ennreal.mul_zero,
+  zero_mul := ennreal.zero_mul,
+  one_mul := by simp [forall_ennreal, -of_real_one, of_real_one.symm, zero_le_one] {contextual := tt},
+  mul_one := by simp [forall_ennreal, -of_real_one, of_real_one.symm, zero_le_one] {contextual := tt},
+  mul_comm := ennreal.mul_comm,
+  mul_assoc := ennreal.mul_assoc,
+  left_distrib := ennreal.left_distrib,
+  right_distrib := assume a b c, by rw [ennreal.mul_comm, ennreal.left_distrib,
+    ennreal.mul_comm, ennreal.mul_comm b c]; refl }
+
+end semiring
+
+section order
+
+instance : has_le ennreal :=
+⟨λ a b, b = ∞ ∨ (∃r p, 0 ≤ r ∧ r ≤ p ∧ a = of_real r ∧ b = of_real p)⟩
+
+@[simp] lemma infty_le_iff : ∞ ≤ a ↔ a = ∞ :=
+by unfold has_le.le; simp
+
+@[simp] lemma le_infty : a ≤ ∞ :=
+by unfold has_le.le; simp
+
+@[simp] lemma of_real_le_of_real_iff (hr : 0 ≤ r) (hp : 0 ≤ p) :
+  of_real r ≤ of_real p ↔ r ≤ p :=
+show (of_real p = ∞ ∨ _) ↔ _,
+begin
+  simp, constructor,
+  exact assume ⟨r', q', hrq', h₁, h₂, hr'⟩,
+    by simp [hr, hr', le_trans hr' hrq', hp] at h₁ h₂; simp [*],
+  exact assume h, ⟨r, p, h, rfl, rfl, hr⟩
+end
+
+lemma le_of_real_iff (hr : 0 ≤ r) : ∀{a}, a ≤ of_real r ↔ (∃p, 0 ≤ p ∧ p ≤ r ∧ a = of_real p) :=
+have ∀p, 0 ≤ p → (of_real p ≤ of_real r ↔ ∃ (q : ℝ), 0 ≤ q ∧ q ≤ r ∧ of_real p = of_real q),
+  from assume p hp, ⟨assume h, ⟨p, hp, (of_real_le_of_real_iff hp hr).mp h, rfl⟩,
+    assume ⟨q, hq, hqr, heq⟩, calc of_real p = of_real q : heq
+      ... ≤ _ : (of_real_le_of_real_iff hq hr).mpr hqr⟩,
+forall_ennreal.mpr $ ⟨this, by simp⟩
+
+@[simp] protected lemma zero_le : ∀{a:ennreal}, 0 ≤ a :=
+by simp [forall_ennreal, -of_real_zero, of_real_zero.symm] {contextual:=tt}
+
+instance : decidable_linear_order ennreal :=
+{ decidable_linear_order .
+  le := (≤),
+  le_refl := by simp [forall_ennreal, le_refl] {contextual := tt},
+  le_trans := by simp [forall_ennreal] {contextual := tt}; exact assume a ha b hb c hc, le_trans,
+  le_antisymm := by simp [forall_ennreal] {contextual := tt}; exact assume a ha b hb, le_antisymm,
+  le_total := by simp [forall_ennreal] {contextual := tt}; exact assume a ha b hb, le_total _ _,
+  decidable_le := by apply_instance }
+
+@[simp] lemma le_zero_iff_eq : a ≤ 0 ↔ a = 0 :=
+⟨assume h, le_antisymm h ennreal.zero_le, assume h, h ▸ le_refl a⟩
+
+lemma of_real_lt_of_real_iff :
+  0 ≤ r → 0 ≤ p → (of_real r < of_real p ↔ r < p) :=
+by simp [lt_iff_le_not_le] {contextual:=tt}
+
+lemma add_le_add : ∀{b d}, a ≤ b → c ≤ d → a + c ≤ b + d :=
+forall_ennreal.mpr ⟨assume r hr, forall_ennreal.mpr ⟨assume p hp,
+  by simp [le_of_real_iff, *, exists_implies_distrib, and_imp_iff] {contextual:=tt};
+    simp [*, add_nonneg, add_le_add] {contextual := tt}, by simp⟩, by simp⟩
+
+lemma mul_le_mul : ∀{b d}, a ≤ b → c ≤ d → a * c ≤ b * d :=
+forall_ennreal.mpr ⟨assume r hr, forall_ennreal.mpr ⟨assume p hp,
+  by simp [le_of_real_iff, *, exists_implies_distrib, and_imp_iff] {contextual:=tt};
+    simp [*, zero_le_mul, mul_le_mul] {contextual := tt},
+    by by_cases r = 0; simp [*] {contextual:=tt}⟩,
+    assume d, by by_cases d = 0; simp [*] {contextual:=tt}⟩
+
+protected lemma zero_lt_one : 0 < (1 : ennreal) :=
+(of_real_lt_of_real_iff (le_refl 0) zero_le_one).mpr zero_lt_one
+
+end order
+
+section complete_lattice
+
+@[simp] lemma infty_mem_upper_bounds {s : set ennreal} : ∞ ∈ upper_bounds s :=
+assume x hx, le_infty
+
+lemma of_real_mem_upper_bounds {s : set real} (hs : ∀x∈s, (0:real) ≤ x) (hr : 0 ≤ r) :
+  of_real r ∈ upper_bounds (of_real '' s) ↔ r ∈ upper_bounds s :=
+by simp [upper_bounds, bounded_forall_image_iff, *] {contextual := tt}
+
+lemma is_lub_of_real {s : set real} (hs : ∀x∈s, (0:real) ≤ x) (hr : 0 ≤ r) (h : s ≠ ∅) :
+  is_lub (of_real '' s) (of_real r) ↔ is_lub s r :=
+let ⟨x, hx₁⟩ := exists_mem_of_ne_empty h in
+have hx₂ : 0 ≤ x, from hs _ hx₁,
+begin
+  simp [is_lub, is_least, lower_bounds, of_real_mem_upper_bounds, hs, hr, forall_ennreal]
+    {contextual := tt},
+  exact (and_congr_right $ assume hrb,
+    ⟨assume h p hp, h _ (le_trans hx₂ $ hp _ hx₁) hp, assume h p _ hp, h _ hp⟩)
+end
+
+protected lemma exists_is_lub (s : set ennreal) : ∃x, is_lub s x :=
+by_cases (assume h : s = ∅, ⟨0, by simp [h, is_lub, is_least, lower_bounds, upper_bounds]⟩) $
+  assume h : s ≠ ∅,
+  let ⟨x, hx⟩ := exists_mem_of_ne_empty h in
+  by_cases
+    (assume : ∃r, 0 ≤ r ∧ of_real r ∈ upper_bounds s,
+      let ⟨r, hr, hb⟩ := this in
+      let s' := of_real ⁻¹' s ∩ {x | 0 ≤ x} in
+      have s'_nn : ∀x∈s', (0:real) ≤ x, from assume x h, h.right,
+      have s_eq : s = of_real '' s',
+        from set.ext $ assume a, ⟨assume ha,
+          let ⟨q, hq₁, hq₂, hq₃⟩ := (le_of_real_iff hr).mp (hb _ ha) in
+          ⟨q, ⟨show of_real q ∈ s, from hq₃ ▸ ha, hq₁⟩, hq₃ ▸ rfl⟩,
+          assume ⟨r, ⟨hr₁, hr₂⟩, hr₃⟩, hr₃ ▸ hr₁⟩,
+      have x ∈ of_real '' s', from s_eq ▸ hx,
+      let ⟨x', hx', hx'_eq⟩ := this in
+      have ∃x, is_lub s' x, from exists_supremum_real ‹x' ∈ s'› $
+        (of_real_mem_upper_bounds s'_nn hr).mp $ s_eq ▸ hb,
+      let ⟨x, hx⟩ := this in
+      have 0 ≤ x, from le_trans hx'.right $ hx.left _ hx',
+      ⟨of_real x, by rwa [s_eq, is_lub_of_real s'_nn this]; exact ne_empty_of_mem hx'⟩)
+    begin
+      intro h,
+      existsi ∞,
+      simp [is_lub, is_least, lower_bounds, forall_ennreal, not_exists_iff, not_and_iff_imp_not]
+        at h ⊢,
+      assumption
+    end
+
+instance : has_Sup ennreal := ⟨λs, some (ennreal.exists_is_lub s)⟩
+
+protected lemma is_lub_Sup {s : set ennreal} : is_lub s (Sup s) :=
+some_spec _
+
+protected lemma le_Sup {s : set ennreal} : a ∈ s → a ≤ Sup s :=
+ennreal.is_lub_Sup.left a
+
+protected lemma Sup_le {s : set ennreal} : (∀b∈s, b ≤ a) → Sup s ≤ a :=
+ennreal.is_lub_Sup.right _
+
+instance : complete_lattice ennreal :=
+{ ennreal.decidable_linear_order with
+  top := ∞,
+  bot := 0,
+  inf := min,
+  sup := max,
+  Sup := Sup,
+  Inf := λs, Sup {a | ∀b∈s, a ≤ b},
+  le_top       := assume a, le_infty,
+  bot_le       := assume a, ennreal.zero_le,
+  le_sup_left  := le_max_left,
+  le_sup_right := le_max_right,
+  sup_le       := assume a b c, max_le,
+  inf_le_left  := min_le_left,
+  inf_le_right := min_le_right,
+  le_inf       := assume a b c, le_min,
+  le_Sup       := assume s a, ennreal.le_Sup,
+  Sup_le       := assume s a, ennreal.Sup_le,
+  le_Inf       := assume s a h, ennreal.le_Sup h,
+  Inf_le       := assume s a ha, ennreal.Sup_le $ assume b hb, hb _ ha }
+
+end complete_lattice
+
+end ennreal