noncomputable def Real.am (xs : List ℝ) : ℝ

Equations

• Real.am xs = xs.sum / ↑xs.length

noncomputable def Real.gm (xs : List ℝ) : ℝ

Equations

• Real.gm xs = xs.prod ^ (↑xs.length)⁻¹

noncomputable def Real.mk! (f : ℕ → ℚ) : ℝ

Equations

• Real.mk! f = if h : IsCauSeq abs f then Real.mk ⟨f, h⟩ else 0

theorem Real.add_inv {a b : ℝ} (h : b ≠ 0) : a + b⁻¹ = (a * b + 1) / b

theorem Real.pow_lt_iff {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ b < c ↔ a < c ^ (1 / b)

theorem Real.add_inv_pow_lt_exp_one_of {a : ℝ} (h : 0 ≤ a) : (1 + a⁻¹) ^ a < exp 1

theorem Real.ofNat_eq {n : ℕ} : OfNat.ofNat n = ↑n

theorem Real.list_sum_map_mul_left {xs : List ℝ} {w : ℝ} : (List.map (fun (x : ℝ) => w * x) xs).sum = w * xs.sum

theorem Real.list_sum_map_mul_right {xs : List ℝ} {w : ℝ} : (List.map (fun (x : ℝ) => x * w) xs).sum = xs.sum * w

theorem Real.gm_le_am (xs : List ℝ) (h₁ : xs ≠ []) (h₂ : ∀ x ∈ xs, 0 ≤ x) : gm xs ≤ am xs

theorem Real.gm_le_am_2 (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : √(a * b) ≤ (a + b) / 2

theorem Real.gm_le_am_3 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : (a * b * c) ^ 3⁻¹ ≤ (a + b + c) / 3

theorem Real.log_eq_logb {a : ℝ} : log a = logb (exp 1) a

theorem Real.eq_of_log_eq_log {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (h : log a = log b) : a = b

theorem Real.log_eq_log_iff {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : log a = log b ↔ a = b

theorem Real.rpow_eq_exp {a b : ℝ} (ha : 0 < a) : a ^ b = exp (b * log a)

theorem Real.exi_mk_cauchy {x : ℝ} : ∃ (a : ℕ → ℚ) (ha : IsCauSeq abs a), x = mk ⟨a, ha⟩

theorem IsCauSeq.sub {a b : ℕ → ℚ} (ha : IsCauSeq abs a) (hb : IsCauSeq abs b) : IsCauSeq abs (a - b)

theorem Real.mk_sub_mk {a b : ℕ → ℚ} {ha : IsCauSeq abs a} {hb : IsCauSeq abs b} : mk ⟨a, ha⟩ - mk ⟨b, hb⟩ = mk ⟨a - b, ⋯⟩

theorem IsCauSeq.abs' {a : ℕ → ℚ} (ha : IsCauSeq abs a) : IsCauSeq abs |a|

theorem Real.neg_mk {a : ℕ → ℚ} {ha : IsCauSeq abs a} : -mk ⟨a, ha⟩ = mk ⟨-a, ⋯⟩

theorem Real.abs_mk {a : ℕ → ℚ} {ha : IsCauSeq abs a} : |mk ⟨a, ha⟩| = mk ⟨|a|, ⋯⟩

theorem Real.inv_lt_self_of_one_lt {x : ℝ} (h : 1 < x) : x⁻¹ < x

theorem Real.inv_le_self_of_one_le {x : ℝ} (h : 1 ≤ x) : x⁻¹ ≤ x

theorem Real.lt_inv_self_of {x : ℝ} (h₁ : 0 < x) (h₂ : x < 1) : x < x⁻¹

theorem Real.le_inv_self_of {x : ℝ} (h₁ : 0 < x) (h₂ : x ≤ 1) : x ≤ x⁻¹

theorem Real.sqrt_add_one_sub_lt_one {x : ℝ} (hx : 0 < x) : √(x + 1) - √x < 1

@[simp]

theorem Real.abs_sqrt {x : ℝ} : |√x| = √x

theorem Real.abs_sub_lt_of_lt_lt_half {a b c d : ℝ} (h₁ : |a - c| < d / 2) (h₂ : |b - c| < d / 2) : |a - b| < d

theorem Real.abs_sub_lt_of_le_lt_half {a b c d : ℝ} (h₁ : |a - c| ≤ d / 2) (h₂ : |b - c| < d / 2) : |a - b| < d

theorem Real.abs_sub_lt_of_lt_le_half {a b c d : ℝ} (h₁ : |a - c| < d / 2) (h₂ : |b - c| ≤ d / 2) : |a - b| < d

theorem Real.abs_sub_le_of_le_le_half {a b c d : ℝ} (h₁ : |a - c| ≤ d / 2) (h₂ : |b - c| ≤ d / 2) : |a - b| ≤ d

theorem Real.sqrt_add {a b : ℝ} (h₁ : 0 ≤ b) (h₂ : b ≤ a) : √(a + b) = √((a + √(a ^ 2 - b ^ 2)) / 2) + √((a - √(a ^ 2 - b ^ 2)) / 2)

theorem Real.sqrt_sub {a b : ℝ} (h₁ : 0 ≤ b) (h₂ : b ≤ a) : √(a - b) = √((a + √(a ^ 2 - b ^ 2)) / 2) - √((a - √(a ^ 2 - b ^ 2)) / 2)

theorem Real.sqrt_add_sqrt {a b : ℝ} (h₁ : 0 ≤ b) (h₂ : √b ≤ a) : √(a + √b) = √((a + √(a ^ 2 - b)) / 2) + √((a - √(a ^ 2 - b)) / 2)

theorem Real.sqrt_sub_sqrt {a b : ℝ} (h₁ : 0 ≤ b) (h₂ : √b ≤ a) : √(a - √b) = √((a + √(a ^ 2 - b)) / 2) - √((a - √(a ^ 2 - b)) / 2)

@[simp]

theorem Real.sq_sqrt_nat {n : ℕ} : √(OfNat.ofNat n) ^ 2 = OfNat.ofNat n

@[simp]

theorem Real.sqrt_sq_nat {n : ℕ} : √(OfNat.ofNat n ^ 2) = OfNat.ofNat n

theorem Real.sqrt_eq_of_neg {a : ℝ} (h : a < 0) : √a = 0

theorem Real.sqrt_eq_of_nonpos {a : ℝ} (h : a ≤ 0) : √a = 0

@[simp]

theorem Real.le_sq_self_iff {a : ℝ} : a ≤ a ^ 2 ↔ a ≤ 0 ∨ 1 ≤ a

@[simp]

theorem Real.lt_sq_self_iff {a : ℝ} : a < a ^ 2 ↔ a < 0 ∨ 1 < a

theorem Real.pow_rpow_inv {a : ℝ} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) : (a ^ OfNat.ofNat n) ^ (OfNat.ofNat n)⁻¹ = a

theorem Real.rpow_inv_pow {a : ℝ} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) : (a ^ (OfNat.ofNat n)⁻¹) ^ OfNat.ofNat n = a