feat(analysis/mean_inequalities) : Prove AM-GM (#1836)

* feat(analysis/mean_inequalities) : Prove AM-GM

* Update, add more inequalities

* Update src/analysis/convex/specific_functions.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/analysis/mean_inequalities.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/analysis/mean_inequalities.lean

* Small fixes, thanks @sgouezel

* Update src/analysis/mean_inequalities.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 4 people

src/analysis/calculus/deriv.lean

@@ -1217,10 +1217,89 @@ funext $ λ x, deriv_pow
 
 lemma deriv_within_pow (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within (λx, x^n) s x = (n : 𝕜) * x^(n-1) :=
-by rw [differentiable_at_pow.deriv_within hxs, deriv_pow]
+(has_deriv_within_at_pow n x s).deriv_within hxs
+
+lemma iter_deriv_pow' {k : ℕ} :
+  deriv^[k] (λx:𝕜, x^n) = λ x, ((finset.range k).prod (λ i, n - i):ℕ) * x^(n-k) :=
+begin
+  induction k with k ihk,
+  { simp only [one_mul, finset.prod_range_zero, nat.iterate_zero, nat.sub_zero, nat.cast_one] },
+  { simp only [nat.iterate_succ', ihk, finset.prod_range_succ],
+    ext x,
+    rw [((has_deriv_at_pow (n - k) x).const_mul _).deriv, nat.cast_mul, mul_left_comm, mul_assoc,
+      nat.succ_eq_add_one, nat.sub_sub] }
+end
+
+lemma iter_deriv_pow {k : ℕ} :
+  deriv^[k] (λx:𝕜, x^n) x = ((finset.range k).prod (λ i, n - i):ℕ) * x^(n-k) :=
+congr_fun iter_deriv_pow' x
 
 end pow
 
+section fpow
+/-! ### Derivative of `x ↦ x^m` for `m : ℤ` -/
+variables {x : 𝕜} {s : set 𝕜}
+variable {m : ℤ}
+
+lemma has_deriv_at_fpow (m : ℤ) (hx : x ≠ 0) :
+  has_deriv_at (λx, x^m) ((m : 𝕜) * x^(m-1)) x :=
+begin
+  have : ∀ m : ℤ, 0 < m → has_deriv_at (λx, x^m) ((m:𝕜) * x^(m-1)) x,
+  { assume m hm,
+    lift m to ℕ using (le_of_lt hm),
+    simp only [fpow_of_nat, int.cast_coe_nat],
+    convert has_deriv_at_pow _ _ using 2,
+    rw [← int.coe_nat_one, ← int.coe_nat_sub, fpow_of_nat],
+    norm_cast at hm,
+    exact nat.succ_le_of_lt hm },
+  rcases lt_trichotomy m 0 with hm|hm|hm,
+  { have := (has_deriv_at_inv _).comp _ (this (-m) (neg_pos.2 hm));
+      [skip, exact fpow_ne_zero_of_ne_zero hx _],
+    simp only [(∘), fpow_neg, one_div_eq_inv, inv_inv', smul_eq_mul] at this,
+    convert this using 1,
+    rw [pow_two, mul_inv', inv_inv', int.cast_neg, ← neg_mul_eq_neg_mul, neg_mul_neg,
+      ← fpow_add hx, mul_assoc, ← fpow_add hx], congr, abel },
+  { simp only [hm, fpow_zero, int.cast_zero, zero_mul, has_deriv_at_const] },
+  { exact this m hm }
+end
+
+theorem has_deriv_within_at_fpow (m : ℤ) (hx : x ≠ 0) (s : set 𝕜) :
+  has_deriv_within_at (λx, x^m) ((m : 𝕜) * x^(m-1)) s x :=
+(has_deriv_at_fpow m hx).has_deriv_within_at
+
+lemma differentiable_at_fpow (hx : x ≠ 0)  : differentiable_at 𝕜 (λx, x^m) x :=
+(has_deriv_at_fpow m hx).differentiable_at
+
+lemma differentiable_within_at_fpow (hx : x ≠ 0) :
+  differentiable_within_at 𝕜 (λx, x^m) s x :=
+(differentiable_at_fpow hx).differentiable_within_at
+
+lemma differentiable_on_fpow (hs : (0:𝕜) ∉ s) : differentiable_on 𝕜 (λx, x^m) s :=
+λ x hxs, differentiable_within_at_fpow (λ hx, hs $ hx ▸ hxs)
+
+-- TODO : this is true at `x=0` as well
+lemma deriv_fpow (hx : x ≠ 0) : deriv (λx, x^m) x = (m : 𝕜) * x^(m-1) :=
+(has_deriv_at_fpow m hx).deriv
+
+lemma deriv_within_fpow (hxs : unique_diff_within_at 𝕜 s x) (hx : x ≠ 0) :
+  deriv_within (λx, x^m) s x = (m : 𝕜) * x^(m-1) :=
+(has_deriv_within_at_fpow m hx s).deriv_within hxs
+
+lemma iter_deriv_fpow {k : ℕ} (hx : x ≠ 0) :
+  deriv^[k] (λx:𝕜, x^m) x = ((finset.range k).prod (λ i, m - i):ℤ) * x^(m-k) :=
+begin
+  induction k with k ihk generalizing x hx,
+  { simp only [one_mul, finset.prod_range_zero, nat.iterate_zero, int.coe_nat_zero, sub_zero,
+      int.cast_one] },
+  { rw [nat.iterate_succ', finset.prod_range_succ, int.cast_mul, mul_assoc, mul_left_comm, int.coe_nat_succ,
+      ← sub_sub, ← ((has_deriv_at_fpow _ hx).const_mul _).deriv],
+    apply deriv_congr_of_mem_nhds,
+    apply eventually.mono _ @ihk,
+    exact mem_nhds_sets (is_open_neg $ is_closed_eq continuous_id continuous_const) hx }
+end
+
+end fpow
+
 /-! ### Upper estimates on liminf and limsup -/
 
 section real

src/analysis/convex/specific_functions.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import analysis.calculus.mean_value data.nat.parity analysis.complex.exponential
+
+/-!
+# Collection of convex functions
+
+In this file we prove that the following functions are convex:
+
+* `convex_on_exp` : the exponential function is convex on $(-∞, +∞)$;
+* `convex_on_pow_of_even` : given an even natural number $n$, the function $f(x)=x^n$
+  is convex on $(-∞, +∞)$;
+* `convex_on_pow` : for a natural $n$, the function $f(x)=x^n$ is convex on $[0, +∞)$;
+* `convex_on_fpow` : for an integer $m$, the function $f(x)=x^m$ is convex on $(0, +∞)$.
+
+## TODO
+
+* `convex_on_rpow : ∀ r : ℝ, (r ≤ 0 ∨ 1 ≤ r) → convex_on (Ioi 0) (λ x, x ^ r)`
+-/
+
+open real set
+
+/-- `exp` is convex on the whole real line -/
+lemma convex_on_exp : convex_on univ exp :=
+convex_on_univ_of_deriv2_nonneg differentiable_exp
+  (deriv_exp.symm ▸ differentiable_exp)
+  (assume x, (iter_deriv_exp 2).symm ▸ le_of_lt (exp_pos x))
+
+/-- `x^n`, `n : ℕ` is convex on the whole real line whenever `n` is even -/
+lemma convex_on_pow_of_even {n : ℕ} (hn : n.even) : convex_on set.univ (λ x, x^n) :=
+begin
+  apply convex_on_univ_of_deriv2_nonneg differentiable_pow,
+  { simp only [deriv_pow', differentiable.mul, differentiable_const, differentiable_pow] },
+  { intro x,
+    rcases hn.sub (nat.even_bit0 1) with ⟨k, hk⟩,
+    simp only [iter_deriv_pow, finset.prod_range_succ, finset.prod_range_zero, nat.sub_zero,
+      mul_one, hk, pow_mul', pow_two],
+    exact mul_nonneg (nat.cast_nonneg _) (mul_self_nonneg _) }
+end
+
+/-- `x^n`, `n : ℕ` is convex on `[0, +∞)` for all `n` -/
+lemma convex_on_pow (n : ℕ) : convex_on (Ici 0) (λ x, x^n) :=
+begin
+  apply convex_on_of_deriv2_nonneg (convex_Ici _) (continuous_pow n).continuous_on;
+    simp only [interior_Ici, differentiable_on_pow, deriv_pow',
+      differentiable_on_const, differentiable_on.mul, iter_deriv_pow],
+  intros x hx,
+  exact mul_nonneg (nat.cast_nonneg _) (pow_nonneg (le_of_lt hx) _)
+end
+
+lemma finset.prod_nonneg_of_card_nonpos_even
+  {α β : Type*} [decidable_eq α] [linear_ordered_comm_ring β]
+  {f : α → β} [decidable_pred (λ x, f x ≤ 0)]
+  {s : finset α} (h0 : (s.filter (λ x, f x ≤ 0)).card.even) :
+  0 ≤ s.prod f :=
+calc 0 ≤ s.prod (λ x, (if f x ≤ 0 then (-1:β) else 1) * f x) :
+  finset.prod_nonneg (λ x _, by
+    { split_ifs with hx hx, by simp [hx], simp at hx ⊢, exact le_of_lt hx })
+... = _ : by rw [finset.prod_mul_distrib, finset.prod_ite _ _ (λx,x), finset.prod_const_one,
+  mul_one, finset.prod_const, neg_one_pow_eq_pow_mod_two, nat.even_iff.1 h0, pow_zero, one_mul];
+  -- TODO: why Lean fails to find this instance in `prod_ite`?
+  apply_instance
+
+lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : n.even) :
+  0 ≤ (finset.range n).prod (λ k, m - k) :=
+begin
+  cases (le_or_lt ↑n m) with hnm hmn,
+  { exact finset.prod_nonneg (λ k hk, sub_nonneg.2 (le_trans
+      (int.coe_nat_le.2 $ le_of_lt $ finset.mem_range.1 hk) hnm)) },
+  cases le_or_lt 0 m with hm hm,
+  { lift m to ℕ using hm,
+    exact le_of_eq (eq.symm $ finset.prod_eq_zero
+      (finset.mem_range.2 $ int.coe_nat_lt.1 hmn) (sub_self _)) },
+  clear hmn,
+  apply finset.prod_nonneg_of_card_nonpos_even,
+  convert hn,
+  convert finset.card_range n,
+  ext k,
+  simp only [finset.mem_filter, finset.mem_range],
+  refine ⟨and.left, λ hk, ⟨hk, sub_nonpos.2 $ le_trans (le_of_lt hm) _⟩⟩,
+  exact int.coe_nat_nonneg k
+end
+
+/-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m` -/
+lemma convex_on_fpow (m : ℤ) : convex_on (Ioi 0) (λ x, x^m) :=
+begin
+  apply convex_on_of_deriv2_nonneg (convex_Ioi 0); try { rw [interior_Ioi] },
+  { exact (differentiable_on_fpow $ lt_irrefl _).continuous_on },
+  { exact differentiable_on_fpow (lt_irrefl _) },
+  { have : eq_on (deriv (λx:ℝ, x^m)) (λx, ↑m * x^(m-1)) (Ioi 0),
+      from λ x hx, deriv_fpow (ne_of_gt hx),
+    refine (differentiable_on_congr this).2 _,
+    exact (differentiable_on_fpow (lt_irrefl _)).const_mul _ },
+  { intros x hx,
+    simp only [iter_deriv_fpow (ne_of_gt hx)],
+    refine mul_nonneg (int.cast_nonneg.2 _) (fpow_nonneg_of_nonneg (le_of_lt hx) _),
+    exact int_prod_range_nonneg _ _ (nat.even_bit0 1) }
+end

src/analysis/mean_inequalities.lean

@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import analysis.calculus.mean_value data.nat.parity analysis.complex.exponential
+  analysis.convex.specific_functions
+
+/-!
+# Mean value inequalities
+
+In this file we prove various inequalities between mean values:
+arithmetic mean, geometric mean, generalized mean (natural and integer
+cases).
+
+For generalized means we only prove
+$\left( ∑_j w_j z_j \right)^n ≤ ∑_j w_j z_j^n$ because standard versions would
+require $\sqrt[n]{x}$ which is not implemented in `mathlib` yet.
+
+Probably a better approach to the generalized means inequality is to
+prove `convex_on_rpow` in `analysis/convex/specific_functions` first,
+then apply it.
+
+It is not yet clear which versions will be useful in the future, so we
+provide two different forms of most inequalities : for `ℝ` and for
+`ℝ≥0`. For the AM-GM inequality we also prove special cases for `n=2`
+and `n=3`.
+-/
+
+universes u v
+
+open real finset
+open_locale classical nnreal
+
+variables {ι : Type u} (s : finset ι)
+
+/-- Geometric mean is less than or equal to the arithmetic mean, weighted version
+for functions on `finset`s. -/
+theorem real.am_gm_weighted (w z : ι → ℝ)
+  (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : s.sum w = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
+  s.prod (λ i, (z i) ^ (w i)) ≤ s.sum (λ i, w i * z i) :=
+begin
+  let s' := s.filter (λ i, w i ≠ 0),
+  rw [← sum_filter_ne_zero] at hw',
+  suffices : s'.prod (λ i, (z i) ^ (w i)) ≤ s'.sum (λ i, w i * z i),
+  { have A : ∀ i ∈ s, i ∉ s' → w i = 0,
+    { intros i hi hi',
+      simpa only [hi, mem_filter, ne.def, true_and, not_not] using hi' },
+    have B : ∀ i ∈ s, i ∉ s' → (z i) ^ (w i) = 1,
+      from λ i hi hi', by rw [A i hi hi', rpow_zero],
+    have C : ∀ i ∈ s, i ∉ s' → w i * z i = 0,
+      from λ i hi hi', by rw [A i hi hi', zero_mul],
+    rwa [← prod_subset s.filter_subset B, ← sum_subset s.filter_subset C] },
+  have A : ∀ i ∈ s', i ∈ s ∧ w i ≠ 0, from λ i hi, mem_filter.1 hi,
+  replace hz : ∀ i ∈ s', 0 ≤ z i := λ i hi, hz i (A i hi).1,
+  replace hw : ∀ i ∈ s', 0 ≤ w i := λ i hi, hw i (A i hi).1,
+  by_cases B : ∃ i ∈ s', z i = 0,
+  { rcases B with ⟨i, imem, hzi⟩,
+    rw [prod_eq_zero imem],
+    { exact sum_nonneg (λ j hj, mul_nonneg (hw j hj) (hz j hj)) },
+    { rw hzi, exact zero_rpow (A i imem).2 } },
+  { replace hz : ∀ i ∈ s', 0 < z i,
+      from λ i hi, lt_of_le_of_ne (hz _ hi) (λ h, B ⟨i, hi, h.symm⟩),
+    have := convex_on_exp.map_sum_le hw hw' (λ i _, set.mem_univ $ log (z i)),
+    simp only [exp_sum, (∘), smul_eq_mul, mul_comm (w _) (log _)] at this,
+    convert this using 1,
+    { exact prod_congr rfl (λ i hi, rpow_def_of_pos (hz i hi) _) },
+    { exact sum_congr rfl (λ i hi, congr_arg _ (exp_log $ hz i hi).symm) } }
+end
+
+theorem nnreal.am_gm_weighted (w z : ι → ℝ≥0) (hw' : s.sum w = 1) :
+  s.prod (λ i, (z i:ℝ) ^ (w i:ℝ)) ≤ s.sum (λ i, w i * z i) :=
+begin
+  refine real.am_gm_weighted _ _ _ (λ i _, (w i).coe_nonneg) _ (λ i _, (z i).coe_nonneg),
+  assumption_mod_cast
+end
+
+theorem nnreal.am_gm2_weighted (w₁ w₂ p₁ p₂ : ℝ≥0) (hw : w₁ + w₂ = 1) :
+  (p₁:ℝ) ^ (w₁:ℝ) * p₂ ^ (w₂:ℝ) ≤ w₁ * p₁ + w₂ * p₂ :=
+begin
+  have := nnreal.am_gm_weighted (univ : finset (fin 2)) (fin.cons w₁ $ fin.cons w₂ fin_zero_elim)
+    (fin.cons p₁ $ fin.cons p₂ $ fin_zero_elim),
+  simp only [fin.prod_univ_succ, fin.sum_univ_succ, fin.prod_univ_zero, fin.sum_univ_zero,
+    fin.cons_succ, fin.cons_zero, add_zero, mul_one] at this,
+  exact this hw
+end
+
+theorem real.am_gm2_weighted {w₁ w₂ p₁ p₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂)
+  (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hw : w₁ + w₂ = 1) :
+  p₁ ^ w₁ * p₂ ^ w₂ ≤ w₁ * p₁ + w₂ * p₂ :=
+nnreal.am_gm2_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ $ nnreal.coe_eq.1 $ by assumption
+
+theorem nnreal.am_gm3_weighted (w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0) (hw : w₁ + w₂ + w₃ = 1) :
+  (p₁:ℝ) ^ (w₁:ℝ) * p₂ ^ (w₂:ℝ) * p₃ ^ (w₃:ℝ) ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃:=
+begin
+  have := nnreal.am_gm_weighted (univ : finset (fin 3))
+    (fin.cons w₁ $ fin.cons w₂ $ fin.cons w₃ fin_zero_elim)
+    (fin.cons p₁ $ fin.cons p₂ $ fin.cons p₃ fin_zero_elim),
+  simp only [fin.prod_univ_succ, fin.sum_univ_succ, fin.prod_univ_zero, fin.sum_univ_zero,
+    fin.cons_succ, fin.cons_zero, add_zero, mul_one, (add_assoc _ _ _).symm,
+    (mul_assoc _ _ _).symm] at this,
+  exact this hw
+end
+
+/-- Young's inequality, `ℝ≥0` version -/
+theorem nnreal.young_inequality (a b : ℝ≥0) {p q : ℝ≥0} (hp : 1 < p) (hq : 1 < q)
+  (hpq : 1/p + 1/q = 1) :
+  (a * b:ℝ) ≤ (a:ℝ)^(p:ℝ) / p + (b:ℝ)^(q:ℝ) / q :=
+begin
+  have := nnreal.am_gm2_weighted (1/p) (1/q) ⟨(a:ℝ)^(p:ℝ), rpow_nonneg_of_nonneg a.coe_nonneg _⟩
+    ⟨(b:ℝ)^(q:ℝ), rpow_nonneg_of_nonneg b.coe_nonneg _⟩ hpq,
+  simp only [nnreal.coe_mk, nnreal.coe_div, nnreal.coe_one, one_div_eq_inv,
+    (rpow_mul (nnreal.coe_nonneg _) _ _).symm, div_eq_inv_mul.symm] at this,
+  rwa [mul_inv_cancel, mul_inv_cancel, rpow_one, rpow_one] at this;
+    refine ne_of_gt (lt_trans zero_lt_one _); assumption
+end
+
+/-- Young's inequality, `ℝ` version -/
+theorem real.young_inequality {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
+  {p q : ℝ} (hp : 1 < p) (hq : 1 < q) (hpq : 1/p + 1/q = 1) :
+  a * b ≤ a^p / p + b^q / q :=
+@nnreal.young_inequality ⟨a, ha⟩ ⟨b, hb⟩ ⟨p, le_trans zero_le_one (le_of_lt hp)⟩
+  ⟨q, le_trans zero_le_one (le_of_lt hq)⟩ hp hq (nnreal.coe_eq.1 hpq)
+
+theorem real.pow_am_le_am_pow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
+  (hw' : s.sum w = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (n : ℕ) :
+  (s.sum (λ i, w i * z i)) ^ n ≤ s.sum (λ i, w i * z i ^ n) :=
+(convex_on_pow n).map_sum_le hw hw' hz
+
+theorem nnreal.pow_am_le_am_pow (w z : ι → ℝ≥0) (hw' : s.sum w = 1) (n : ℕ) :
+  (s.sum (λ i, w i * z i)) ^ n ≤ s.sum (λ i, w i * z i ^ n) :=
+begin
+  rw [← nnreal.coe_le],
+  push_cast,
+  refine (convex_on_pow n).map_sum_le (λ i _, (w i).coe_nonneg) _ (λ i _, (z i).coe_nonneg),
+  assumption_mod_cast
+end
+
+theorem real.pow_am_le_am_pow_of_even (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
+  (hw' : s.sum w = 1) {n : ℕ} (hn : n.even) :
+  (s.sum (λ i, w i * z i)) ^ n ≤ s.sum (λ i, w i * z i ^ n) :=
+(convex_on_pow_of_even hn).map_sum_le hw hw' (λ _ _, trivial)
+
+theorem real.fpow_am_le_am_fpow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
+  (hw' : s.sum w = 1) (hz : ∀ i ∈ s, 0 < z i) (m : ℤ) :
+  (s.sum (λ i, w i * z i)) ^ m ≤ s.sum (λ i, w i * z i ^ m) :=
+(convex_on_fpow m).map_sum_le hw hw' hz

src/data/nat/parity.lean

@@ -15,6 +15,7 @@ by cases mod_two_eq_zero_or_one n with h h; simp [h]
 @[simp] theorem mod_two_ne_zero {n : nat} : ¬ n % 2 = 0 ↔ n % 2 = 1 :=
 by cases mod_two_eq_zero_or_one n with h h; simp [h]
 
+/-- A natural number `n` is `even` if `2 | n`. -/
 def even (n : nat) : Prop := 2 ∣ n
 
 theorem even_iff {n : nat} : even n ↔ n % 2 = 0 :=
@@ -46,6 +47,9 @@ begin
   exact @modeq.modeq_add _ _ 1 _ 1 h₁ h₂
 end
 
+theorem even.add {m n : ℕ} (hm : m.even) (hn : n.even) : (m + n).even :=
+even_add.2 $ by simp only [*]
+
 @[simp] theorem not_even_bit1 (n : nat) : ¬ even (bit1 n) :=
 by simp [bit1] with parity_simps
 
@@ -55,6 +59,11 @@ begin
   by_cases h : even n; simp [h]
 end
 
+theorem even.sub {m n : ℕ} (hm : m.even) (hn : n.even) : (m - n).even :=
+(le_total n m).elim
+  (λ h, by simp only [even_sub h, *])
+  (λ h, by simp only [sub_eq_zero_of_le h, even_zero])
+
 @[parity_simps] theorem even_succ {n : nat} : even (succ n) ↔ ¬ even n :=
 by rw [succ_eq_add_one, even_add]; simp [not_even_one]
 

src/data/real/nnreal.lean

@@ -38,6 +38,7 @@ lemma le_coe_of_real (r : ℝ) : r ≤ nnreal.of_real r :=
 le_max_left r 0
 
 lemma coe_nonneg (r : nnreal) : (0 : ℝ) ≤ r := r.2
+@[elim_cast, simp] theorem coe_mk (a : ℝ) (ha) : ((⟨a, ha⟩ : ℝ≥0) : ℝ) = a := rfl
 
 instance : has_zero ℝ≥0  := ⟨⟨0, le_refl 0⟩⟩
 instance : has_one ℝ≥0   := ⟨⟨1, zero_le_one⟩⟩

src/data/set/intervals/basic.lean

@@ -318,6 +318,11 @@ end partial_order
 section linear_order
 variables {α : Type u} [linear_order α] {a a₁ a₂ b b₁ b₂ : α}
 
+lemma compl_Iic : -(Iic a) = Ioi a := ext $ λ _, not_le
+lemma compl_Ici : -(Ici a) = Iio a := ext $ λ _, not_le
+lemma compl_Iio : -(Iio a) = Ici a := ext $ λ _, not_lt
+lemma compl_Ioi : -(Ioi a) = Iic a := ext $ λ _, not_lt
+
 lemma Ioo_eq_empty_iff [densely_ordered α] : Ioo a b = ∅ ↔ b ≤ a :=
 ⟨λ eq, le_of_not_lt $ λ h,
   let ⟨x, h₁, h₂⟩ := dense h in