refactor(data/real): move real.sqrt to data.real.sqrt, more depen…

…dencies (#5359)

* define `nnreal.sqrt`;
* use general theory to prove that the inverse exists, and is an `order_iso`;
* deduce continuity of `sqrt` from continuity of `order_iso`.



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

archive/sensitivity.lean

@@ -10,6 +10,7 @@ import tactic.apply_fun
 import linear_algebra.finite_dimensional
 import linear_algebra.dual
 import analysis.normed_space.basic
+import data.real.sqrt
 
 /-!
 # Huang's sensitivity theorem

src/analysis/special_functions/arsinh.lean

@@ -43,8 +43,7 @@ end
 private lemma b_lt_sqrt_b_one_add_sq (b : ℝ) : b < sqrt (1 + b ^ 2) :=
 calc  b
     ≤ sqrt (b ^ 2)     : le_sqrt_of_sqr_le $ le_refl _
-... < sqrt (1 + b ^ 2) : (sqrt_lt (pow_two_nonneg _) (add_nonneg zero_le_one (pow_two_nonneg _))).2
-  (lt_one_add _)
+... < sqrt (1 + b ^ 2) : (sqrt_lt (pow_two_nonneg _)).2 (lt_one_add _)
 
 private lemma add_sqrt_one_add_pow_two_pos (b : ℝ) : 0 < b + sqrt (1 + b ^ 2) :=
 by { rw [← neg_neg b, ← sub_eq_neg_add, sub_pos, pow_two, neg_mul_neg, ← pow_two],

src/analysis/special_functions/pow.lean

@@ -595,9 +595,6 @@ begin
     rw [sqrt_eq_zero_of_nonpos (le_of_lt h), rpow_def_of_neg h, this, cos_pi_div_two, mul_zero] }
 end
 
-lemma continuous_sqrt : continuous sqrt :=
-by rw sqrt_eq_rpow; exact continuous_rpow_of_pos (λa, by norm_num) continuous_id continuous_const
-
 end sqrt
 
 end real

src/analysis/special_functions/trigonometric.lean

@@ -1214,7 +1214,7 @@ variable (x : ℝ)
 /-- the series `sqrt_two_add_series x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots,
   starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2`
 -/
-@[simp] noncomputable def sqrt_two_add_series (x : ℝ) : ℕ → ℝ
+@[simp, pp_nodot] noncomputable def sqrt_two_add_series (x : ℝ) : ℕ → ℝ
 | 0     := x
 | (n+1) := sqrt (2 + sqrt_two_add_series n)
 
@@ -1235,10 +1235,9 @@ lemma sqrt_two_add_series_lt_two : ∀(n : ℕ), sqrt_two_add_series 0 n < 2
 | (n+1) :=
   begin
     refine lt_of_lt_of_le _ (le_of_eq $ sqrt_sqr $ le_of_lt zero_lt_two),
-    rw [sqrt_two_add_series, sqrt_lt],
-    apply add_lt_of_lt_sub_left,
-    apply lt_of_lt_of_le (sqrt_two_add_series_lt_two n),
-    norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num
+    rw [sqrt_two_add_series, sqrt_lt, ← lt_sub_iff_add_lt'],
+    { refine (sqrt_two_add_series_lt_two n).trans_le _, norm_num },
+    { exact add_nonneg zero_le_two (sqrt_two_add_series_zero_nonneg n) }
   end
 
 lemma sqrt_two_add_series_succ (x : ℝ) :
@@ -1252,7 +1251,7 @@ lemma sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) :
 | (n+1) :=
   begin
     rw [sqrt_two_add_series, sqrt_two_add_series],
-    apply sqrt_le_sqrt, apply add_le_add_left, apply sqrt_two_add_series_monotone_left
+    exact sqrt_le_sqrt (add_le_add_left (sqrt_two_add_series_monotone_left _) _)
   end
 
 @[simp] lemma cos_pi_over_two_pow : ∀(n : ℕ), cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2

src/data/complex/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Mario Carneiro
 -/
-import data.real.basic
+import data.real.sqrt
 
 open_locale big_operators
 

src/data/real/basic.lean

@@ -415,216 +415,6 @@ end
 
 noncomputable instance : cau_seq.is_complete ℝ abs := ⟨cau_seq_converges⟩
 
-theorem sqrt_exists : ∀ {x : ℝ}, 0 ≤ x → ∃ y, 0 ≤ y ∧ y * y = x :=
-suffices H : ∀ {x : ℝ}, 0 < x → x ≤ 1 → ∃ y, 0 < y ∧ y * y = x, begin
-  intros x x0, cases x0,
-  cases le_total x 1 with x1 x1,
-  { rcases H x0 x1 with ⟨y, y0, hy⟩,
-    exact ⟨y, le_of_lt y0, hy⟩ },
-  { have := (inv_le_inv x0 zero_lt_one).2 x1,
-    rw inv_one at this,
-    rcases H (inv_pos.2 x0) this with ⟨y, y0, hy⟩,
-    refine ⟨y⁻¹, le_of_lt (inv_pos.2 y0), _⟩, rw [← mul_inv', hy, inv_inv'] },
-  { exact ⟨0, by simp [x0.symm]⟩ }
-end,
-λ x x0 x1, begin
-  let S := {y | 0 < y ∧ y * y ≤ x},
-  have lb : x ∈ S := ⟨x0, by simpa using (mul_le_mul_right x0).2 x1⟩,
-  have ub : ∀ y ∈ S, (y:ℝ) ≤ 1,
-  { intros y yS, cases yS with y0 yx,
-    refine (mul_self_le_mul_self_iff (le_of_lt y0) zero_le_one).2 _,
-    simpa using le_trans yx x1 },
-  have S0 : 0 < Sup S := lt_of_lt_of_le x0 (le_Sup _ ⟨_, ub⟩ lb),
-  refine ⟨Sup S, S0, le_antisymm (not_lt.1 $ λ h, _) (not_lt.1 $ λ h, _)⟩,
-  { rw [← div_lt_iff S0, lt_Sup S ⟨_, lb⟩ ⟨_, ub⟩] at h,
-    rcases h with ⟨y, ⟨y0, yx⟩, hy⟩,
-    rw [div_lt_iff S0, ← div_lt_iff' y0, lt_Sup S ⟨_, lb⟩ ⟨_, ub⟩] at hy,
-    rcases hy with ⟨z, ⟨z0, zx⟩, hz⟩,
-    rw [div_lt_iff y0] at hz,
-    exact not_lt_of_lt
-      ((mul_lt_mul_right y0).1 (lt_of_le_of_lt yx hz))
-      ((mul_lt_mul_left z0).1 (lt_of_le_of_lt zx hz)) },
-  { let s := Sup S, let y := s + (x - s * s) / 3,
-    replace h : 0 < x - s * s := sub_pos.2 h,
-    have _30 := bit1_pos zero_le_one,
-    have : s < y := (lt_add_iff_pos_right _).2 (div_pos h _30),
-    refine not_le_of_lt this (le_Sup S ⟨_, ub⟩ ⟨lt_trans S0 this, _⟩),
-    rw [add_mul_self_eq, add_assoc, ← le_sub_iff_add_le', ← add_mul,
-      ← le_div_iff (div_pos h _30), div_div_cancel' (ne_of_gt h)],
-    apply add_le_add,
-    { simpa using (mul_le_mul_left (@zero_lt_two ℝ _ _)).2 (Sup_le_ub _ ⟨_, lb⟩ ub) },
-    { rw [div_le_one _30],
-      refine le_trans (sub_le_self _ (mul_self_nonneg _)) (le_trans x1 _),
-      exact (le_add_iff_nonneg_left _).2 (le_of_lt zero_lt_two) },
-    apply_instance, }
-end
-
-def sqrt_aux (f : cau_seq ℚ abs) : ℕ → ℚ
-| 0       := rat.mk_nat (f 0).num.to_nat.sqrt (f 0).denom.sqrt
-| (n + 1) := let s := sqrt_aux n in max 0 $ (s + f (n+1) / s) / 2
-
-theorem sqrt_aux_nonneg (f : cau_seq ℚ abs) : ∀ i : ℕ, 0 ≤ sqrt_aux f i
-| 0       := by rw [sqrt_aux, mk_nat_eq, mk_eq_div];
-  apply div_nonneg; exact int.cast_nonneg.2 (int.of_nat_nonneg _)
-| (n + 1) := le_max_left _ _
-
-/- TODO(Mario): finish the proof
-theorem sqrt_aux_converges (f : cau_seq ℚ abs) : ∃ h x, 0 ≤ x ∧ x * x = max 0 (mk f) ∧
-  mk ⟨sqrt_aux f, h⟩ = x :=
-begin
-  rcases sqrt_exists (le_max_left 0 (mk f)) with ⟨x, x0, hx⟩,
-  suffices : ∃ h, mk ⟨sqrt_aux f, h⟩ = x,
-  { exact this.imp (λ h e, ⟨x, x0, hx, e⟩) },
-  apply of_near,
-
-  suffices : ∃ δ > 0, ∀ i, abs (↑(sqrt_aux f i) - x) < δ / 2 ^ i,
-  { rcases this with ⟨δ, δ0, hδ⟩,
-    intros,
-     }
-end -/
-
-/-- The square root of a real number. This returns 0 for negative inputs. -/
-@[pp_nodot] noncomputable def sqrt (x : ℝ) : ℝ :=
-classical.some (sqrt_exists (le_max_left 0 x))
-/-quotient.lift_on x
-  (λ f, mk ⟨sqrt_aux f, (sqrt_aux_converges f).fst⟩)
-  (λ f g e, begin
-    rcases sqrt_aux_converges f with ⟨hf, x, x0, xf, xs⟩,
-    rcases sqrt_aux_converges g with ⟨hg, y, y0, yg, ys⟩,
-    refine xs.trans (eq.trans _ ys.symm),
-    rw [← @mul_self_inj_of_nonneg ℝ _ x y x0 y0, xf, yg],
-    congr' 1, exact quotient.sound e
-  end)-/
-
-theorem sqrt_prop (x : ℝ) : 0 ≤ sqrt x ∧ sqrt x * sqrt x = max 0 x :=
-classical.some_spec (sqrt_exists (le_max_left 0 x))
-/-quotient.induction_on x $ λ f,
-by rcases sqrt_aux_converges f with ⟨hf, _, x0, xf, rfl⟩; exact ⟨x0, xf⟩-/
-
-theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 :=
-eq_zero_of_mul_self_eq_zero $ (sqrt_prop x).2.trans $ max_eq_left h
-
-theorem sqrt_nonneg (x : ℝ) : 0 ≤ sqrt x := (sqrt_prop x).1
-
-@[simp] theorem mul_self_sqrt (h : 0 ≤ x) : sqrt x * sqrt x = x :=
-(sqrt_prop x).2.trans (max_eq_right h)
-
-@[simp] theorem sqrt_mul_self (h : 0 ≤ x) : sqrt (x * x) = x :=
-(mul_self_inj_of_nonneg (sqrt_nonneg _) h).1 (mul_self_sqrt (mul_self_nonneg _))
-
-theorem sqrt_eq_iff_mul_self_eq (hx : 0 ≤ x) (hy : 0 ≤ y) :
-  sqrt x = y ↔ y * y = x :=
-⟨λ h, by rw [← h, mul_self_sqrt hx],
- λ h, by rw [← h, sqrt_mul_self hy]⟩
-
-@[simp] theorem sqr_sqrt (h : 0 ≤ x) : sqrt x ^ 2 = x :=
-by rw [pow_two, mul_self_sqrt h]
-
-@[simp] theorem sqrt_sqr (h : 0 ≤ x) : sqrt (x ^ 2) = x :=
-by rw [pow_two, sqrt_mul_self h]
-
-theorem sqrt_eq_iff_sqr_eq (hx : 0 ≤ x) (hy : 0 ≤ y) :
-  sqrt x = y ↔ y ^ 2 = x :=
-by rw [pow_two, sqrt_eq_iff_mul_self_eq hx hy]
-
-theorem sqrt_mul_self_eq_abs (x : ℝ) : sqrt (x * x) = abs x :=
-(le_total 0 x).elim
-  (λ h, (sqrt_mul_self h).trans (abs_of_nonneg h).symm)
-  (λ h, by rw [← neg_mul_neg,
-    sqrt_mul_self (neg_nonneg.2 h), abs_of_nonpos h])
-
-theorem sqrt_sqr_eq_abs (x : ℝ) : sqrt (x ^ 2) = abs x :=
-by rw [pow_two, sqrt_mul_self_eq_abs]
-
-@[simp] theorem sqrt_zero : sqrt 0 = 0 :=
-by simpa using sqrt_mul_self (le_refl _)
-
-@[simp] theorem sqrt_one : sqrt 1 = 1 :=
-by simpa using sqrt_mul_self zero_le_one
-
-@[simp] theorem sqrt_le (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x ≤ sqrt y ↔ x ≤ y :=
-by rw [mul_self_le_mul_self_iff (sqrt_nonneg _) (sqrt_nonneg _),
-       mul_self_sqrt hx, mul_self_sqrt hy]
-
-@[simp] theorem sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x < sqrt y ↔ x < y :=
-lt_iff_lt_of_le_iff_le (sqrt_le hy hx)
-
-lemma sqrt_le_sqrt (h : x ≤ y) : sqrt x ≤ sqrt y :=
-begin
-  rw [mul_self_le_mul_self_iff (sqrt_nonneg _) (sqrt_nonneg _), (sqrt_prop _).2, (sqrt_prop _).2],
-  exact max_le_max (le_refl _) h
-end
-
-lemma sqrt_le_left (hy : 0 ≤ y) : sqrt x ≤ y ↔ x ≤ y ^ 2 :=
-begin
-  rw [mul_self_le_mul_self_iff (sqrt_nonneg _) hy, pow_two],
-  cases le_total 0 x with hx hx,
-  { rw [mul_self_sqrt hx] },
-  { have h1 : 0 ≤ y * y := mul_nonneg hy hy,
-    have h2 : x ≤ y * y := le_trans hx h1,
-    simp [sqrt_eq_zero_of_nonpos, hx, h1, h2] }
-end
-
-/- note: if you want to conclude `x ≤ sqrt y`, then use `le_sqrt_of_sqr_le`.
-   if you have `x > 0`, consider using `le_sqrt'` -/
-lemma le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
-by rw [mul_self_le_mul_self_iff hx (sqrt_nonneg _), pow_two, mul_self_sqrt hy]
-
-lemma le_sqrt' (hx : 0 < x) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
-begin
-  rw [mul_self_le_mul_self_iff (le_of_lt hx) (sqrt_nonneg _), pow_two],
-  cases le_total 0 y with hy hy,
-  { rw [mul_self_sqrt hy] },
-  { have h1 : 0 < x * x := mul_pos hx hx,
-    have h2 : ¬x * x ≤ y := not_le_of_lt (lt_of_le_of_lt hy h1),
-    simp [sqrt_eq_zero_of_nonpos, hy, h1, h2] }
-end
-
-lemma le_sqrt_of_sqr_le (h : x ^ 2 ≤ y) : x ≤ sqrt y :=
-begin
-  cases lt_or_ge 0 x with hx hx,
-  { rwa [le_sqrt' hx] },
-  { exact le_trans hx (sqrt_nonneg y) }
-end
-
-@[simp] theorem sqrt_inj (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x = sqrt y ↔ x = y :=
-by simp [le_antisymm_iff, hx, hy]
-
-@[simp] theorem sqrt_eq_zero (h : 0 ≤ x) : sqrt x = 0 ↔ x = 0 :=
-by simpa using sqrt_inj h (le_refl _)
-
-theorem sqrt_eq_zero' : sqrt x = 0 ↔ x ≤ 0 :=
-(le_total x 0).elim
-  (λ h, by simp [h, sqrt_eq_zero_of_nonpos])
-  (λ h, by simp [h]; simp [le_antisymm_iff, h])
-
-@[simp] theorem sqrt_pos : 0 < sqrt x ↔ 0 < x :=
-lt_iff_lt_of_le_iff_le (iff.trans
-  (by simp [le_antisymm_iff, sqrt_nonneg]) sqrt_eq_zero')
-
-@[simp] theorem sqrt_mul' (x) {y : ℝ} (hy : 0 ≤ y) : sqrt (x * y) = sqrt x * sqrt y :=
-begin
-  cases le_total 0 x with hx hx,
-  { refine iff.mp (mul_self_inj_of_nonneg _ (mul_nonneg _ _)) _; try {apply sqrt_nonneg},
-    rw [mul_self_sqrt (mul_nonneg hx hy), mul_assoc,
-        mul_left_comm (sqrt y), mul_self_sqrt hy, ← mul_assoc, mul_self_sqrt hx] },
-  { rw [sqrt_eq_zero'.2 (mul_nonpos_of_nonpos_of_nonneg hx hy),
-        sqrt_eq_zero'.2 hx, zero_mul] }
-end
-
-@[simp] theorem sqrt_mul (hx : 0 ≤ x) (y : ℝ) : sqrt (x * y) = sqrt x * sqrt y :=
-by rw [mul_comm, sqrt_mul' _ hx, mul_comm]
-
-@[simp] theorem sqrt_inv (x : ℝ) : sqrt x⁻¹ = (sqrt x)⁻¹ :=
-(le_or_lt x 0).elim
-  (λ h, by simp [sqrt_eq_zero'.2, inv_nonpos, h])
-  (λ h, by rw [
-    ← mul_self_inj_of_nonneg (sqrt_nonneg _) (le_of_lt $ inv_pos.2 $ sqrt_pos.2 h),
-    mul_self_sqrt (le_of_lt $ inv_pos.2 h), ← mul_inv', mul_self_sqrt (le_of_lt h)])
-
-@[simp] theorem sqrt_div (hx : 0 ≤ x) (y : ℝ) : sqrt (x / y) = sqrt x / sqrt y :=
-by rw [division_def, sqrt_mul hx, sqrt_inv]; refl
-
 attribute [irreducible] real.le
 
 end real

src/data/real/irrational.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Yury Kudryashov.
 -/
-import data.real.basic
+import data.real.sqrt
 import data.rat.sqrt
 import ring_theory.int.basic
 import data.polynomial.eval

src/data/real/nnreal.lean

@@ -395,6 +395,10 @@ nnreal.gi.gc r p
 lemma le_of_real_iff_coe_le {r : ℝ≥0} {p : ℝ} (hp : 0 ≤ p) : r ≤ nnreal.of_real p ↔ ↑r ≤ p :=
 by rw [← nnreal.coe_le_coe, nnreal.coe_of_real p hp]
 
+lemma le_of_real_iff_coe_le' {r : ℝ≥0} {p : ℝ} (hr : 0 < r) : r ≤ nnreal.of_real p ↔ ↑r ≤ p :=
+(le_or_lt 0 p).elim le_of_real_iff_coe_le $ λ hp,
+  by simp only [(hp.trans_le r.coe_nonneg).not_le, of_real_eq_zero.2 hp.le, hr.not_le]
+
 lemma of_real_lt_iff_lt_coe {r : ℝ} {p : ℝ≥0} (ha : 0 ≤ r) : nnreal.of_real r < p ↔ r < ↑p :=
 by rw [← nnreal.coe_lt_coe, nnreal.coe_of_real r ha]