feat (analysis/normed_space): Define real inner product space (#1248)

* Inner product space

* Change the definition of inner_product_space

The original definition introduces an instance loop.

See Zulip talks: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ring.20tactic.20works.20at.20one.20place.2C.20fails.20at.20another

* Orthogonal Projection

Prove the existence of orthogonal projections onto complete subspaces in an inner product space.

* Fix names

* small fixes

src/algebra/ordered_field.lean

@@ -187,6 +187,12 @@ inv_pos $ add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one
 lemma one_div_pos_of_nat {n : ℕ} : 0 < 1 / ((n : α) + 1) :=
 by { rw one_div_eq_inv, exact inv_pos_of_nat }
 
+lemma one_div_le_one_div {n m : ℕ} (h : n ≤ m) : 1 / ((m : α) + 1) ≤ 1 / ((n : α) + 1) :=
+by { refine one_div_le_one_div_of_le _ _, exact nat.cast_add_one_pos _, simpa }
+
+lemma one_div_lt_one_div {n m : ℕ} (h : n < m) : 1 / ((m : α) + 1) < 1 / ((n : α) + 1) :=
+by { refine one_div_lt_one_div_of_lt _ _, exact nat.cast_add_one_pos _, simpa }
+
 end nat
 
 section

src/algebra/ordered_ring.lean

@@ -174,6 +174,13 @@ lemma mul_self_pos {a : α} (ha : a ≠ 0) : 0 < a * a :=
 by rcases lt_trichotomy a 0 with h|h|h;
    [exact mul_pos_of_neg_of_neg h h, exact (ha h).elim, exact mul_pos h h]
 
+lemma mul_self_le_mul_self_of_le_of_neg_le {x y : α} (h₁ : x ≤ y) (h₂ : -x ≤ y) : x * x ≤ y * y :=
+begin
+  cases le_total 0 x,
+  { exact mul_self_le_mul_self h h₁ },
+  { rw ← neg_mul_neg, exact mul_self_le_mul_self (neg_nonneg_of_nonpos h) h₂ }
+end
+
 end linear_ordered_ring
 
 set_option old_structure_cmd true

src/algebra/quadratic_discriminant.lean

@@ -0,0 +1,176 @@
+/-
+  Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
+  Released under Apache 2.0 license as described in the file LICENSE.
+  Authors: Zhouhang Zhou
+  -/
+
+import algebra.ordered_field
+import tactic.linarith tactic.ring
+
+/-!
+  # Quadratic discriminants and roots of a quadratic
+
+  This file defines the discriminant of a quadratic and prove their
+
+  ## Main definition
+
+  The discriminant of a quadratic `a*x*x + b*x + c` is `b*b - 4*a*c`.
+
+  ## Main statements
+  • Roots of a quadratic can be written as `(-b + s) / (2 * a)` or `(-b - s) / (2 * a)`,
+    where `s` is the square root of the discriminant.
+  • If the discriminant has no square root, then the corresponding quadratic has no root.
+  • If a quadratic is always non-negative, then its discriminant is non-positive.
+
+  ## Tags
+
+  polynomial, quadratic, discriminant, root
+  -/
+
+variables {α : Type*}
+
+section lemmas
+
+variables [linear_ordered_field α] {a b c : α}
+
+lemma exists_le_mul : ∀ a : α, ∃ x : α, a ≤ x * x :=
+begin
+  assume a, cases le_total 1 a with ha ha,
+  { use a, exact le_mul_of_ge_one_left (by linarith) ha },
+  { use 1, linarith }
+end
+
+lemma exists_lt_mul : ∀ a : α, ∃ x : α, a < x * x :=
+begin
+  assume a, rcases (exists_le_mul a) with ⟨x, hx⟩,
+  cases le_total 0 x with hx' hx',
+  { use (x + 1),
+    have : (x+1)*(x+1) = x*x + 2*x + 1, ring,
+    exact lt_of_le_of_lt hx (by rw this; linarith) },
+  { use (x - 1),
+    have : (x-1)*(x-1) = x*x - 2*x + 1, ring,
+    exact lt_of_le_of_lt hx (by rw this; linarith) }
+end
+
+end lemmas
+
+variables [linear_ordered_field α] {a b c x : α}
+
+/-- Discriminant of a quadratic -/
+def discrim [ring α] (a b c : α) : α := b^2 - 4 * a * c
+
+/--
+A quadratic has roots if and only if its discriminant equals some square.
+-/
+lemma quadratic_eq_zero_iff_discrim_eq_square (ha : a ≠ 0) :
+  ∀ x : α, a * x * x + b * x + c = 0 ↔  discrim a b c = (2 * a * x + b)^2 :=
+assume x, iff.intro
+  ( assume h, calc
+      discrim a b c = 4*a*(a*x*x + b*x + c) + b*b - 4*a*c : by rw [h, discrim]; ring
+      ... = (2*a*x + b)^2 : by ring )
+  ( assume h,
+    have ha : 2*2*a ≠ 0 := mul_ne_zero (mul_ne_zero two_ne_zero two_ne_zero) ha,
+    eq_of_mul_eq_mul_left_of_ne_zero ha $
+    calc
+      2 * 2 * a * (a * x * x + b * x + c) = (2*a*x + b)^2 - (b^2 - 4*a*c) : by ring
+      ... = 0 : by { rw [← h, discrim], ring }
+      ... = 2*2*a*0 : by ring )
+
+/-- Roots of a quadratic -/
+lemma quadratic_eq_zero_iff (ha : a ≠ 0) {s : α} (h : discrim a b c = s * s) :
+  ∀ x : α, a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) := assume x,
+begin
+  rw [quadratic_eq_zero_iff_discrim_eq_square ha, h, pow_two, mul_self_eq_mul_self_iff],
+  have ne : 2 * a ≠ 0 := mul_ne_zero two_ne_zero ha,
+  have : x = 2 * a * x / (2 * a) := (mul_div_cancel_left x ne).symm,
+  have h₁ : 2 * a * ((-b + s) / (2 * a)) = -b + s := mul_div_cancel' _ ne,
+  have h₂ : 2 * a * ((-b - s) / (2 * a)) = -b - s := mul_div_cancel' _ ne,
+  split,
+  { intro h', rcases h', { left, rw h', simpa }, { right, rw h', simpa } },
+  { intro h', rcases h', { left, rw [h', h₁], ring }, { right, rw [h', h₂], ring } }
+end
+
+/-- A quadratic has roots if its discriminant has square roots -/
+lemma exist_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) :
+  ∃ x, a * x * x + b * x + c = 0 :=
+begin
+  rcases h with ⟨s, hs⟩,
+  use (-b + s) / (2 * a),
+  rw quadratic_eq_zero_iff ha hs,
+  simp
+end
+
+/-- Root of a quadratic when its discriminant equals zero -/
+lemma quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) :
+  ∀ x : α, a * x * x + b * x + c = 0 ↔ x = -b / (2 * a) := assume x,
+begin
+  have : discrim a b c = 0 * 0 := eq.trans h (by ring),
+  rw quadratic_eq_zero_iff ha this,
+  simp
+end
+
+/-- A quadratic has no root if its discriminant has no square root. -/
+lemma quadratic_ne_zero_of_discrim_ne_square (ha : a ≠ 0) (h : ∀ s : α, discrim a b c ≠ s * s) :
+  ∀ (x : α), a * x * x + b * x + c ≠ 0 :=
+begin
+  assume x h',
+  rw [quadratic_eq_zero_iff_discrim_eq_square ha, pow_two] at h',
+  have := h _,
+  contradiction
+end
+
+/-- If a polynomial of degree 2 is always nonnegative, then its dicriminant is nonpositive -/
+lemma discriminant_le_zero {a b c : α} (h : ∀ x : α,  0 ≤ a*x*x + b*x + c) : discrim a b c ≤ 0 :=
+have hc : 0 ≤ c, by { have := h 0, linarith },
+begin
+  rw [discrim, pow_two],
+  cases lt_trichotomy a 0 with ha ha,
+  -- if a < 0
+  cases classical.em (b = 0) with hb hb,
+  { rw hb at *,
+    rcases exists_lt_mul (-c/a) with ⟨x, hx⟩,
+    have := mul_lt_mul_of_neg_left hx ha,
+    rw [mul_div_cancel' _ (ne_of_lt ha), ← mul_assoc] at this,
+    have h₂ := h x, linarith },
+  { cases classical.em (c = 0) with hc' hc',
+    { rw hc' at *,
+      have : -(a*-b*-b + b*-b + 0) = (1-a)*(b*b), ring,
+      have h := h (-b), rw [← neg_nonpos, this] at h,
+      have : b * b ≤ 0, from nonpos_of_mul_nonpos_left h (by linarith),
+      linarith },
+    { have h := h (-c/b),
+      have : a*(-c/b)*(-c/b) + b*(-c/b) + c = a*((c/b)*(c/b)),
+        rw mul_div_cancel' _ hb, ring,
+      rw this at h,
+      have : 0 ≤ a := nonneg_of_mul_nonneg_right h (mul_self_pos $ div_ne_zero hc' hb),
+      linarith [ha] } },
+  cases ha with ha ha,
+  -- if a = 0
+  cases classical.em (b = 0) with hb hb,
+    { rw [ha, hb], linarith },
+    { have := h ((-c-1)/b), rw [ha, mul_div_cancel' _ hb] at this, linarith },
+  -- if a > 0
+  have := calc
+    4*a* (a*(-(b/a)*(1/2))*(-(b/a)*(1/2)) + b*(-(b/a)*(1/2)) + c)
+      = (a*(b/a)) * (a*(b/a)) - 2*(a*(b/a))*b + 4*a*c : by ring
+    ... = -(b*b - 4*a*c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
+  have ha' : 0 ≤ 4*a, linarith,
+  have h := (mul_nonneg ha' (h (-(b/a) * (1/2)))),
+  rw this at h, rwa ← neg_nonneg
+end
+
+/--
+If a polynomial of degree 2 is always positive, then its dicriminant is negtive,
+at least when the coefficient of the quadratic term is nonzero.
+-/
+lemma discriminant_lt_zero {a b c : α} (ha : a ≠ 0) (h : ∀ x : α,  0 < a*x*x + b*x + c) :
+  discrim a b c < 0 :=
+begin
+  have : ∀ x : α,  0 ≤ a*x*x + b*x + c := assume x, le_of_lt (h x),
+  refine lt_of_le_of_ne (discriminant_le_zero this) _,
+  assume h',
+  have := h (-b / (2 * a)),
+  have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0,
+    rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))],
+  linarith
+end

src/analysis/convex.lean

@@ -432,6 +432,17 @@ convex_halfspace_gt _ (is_linear_map.mk complex.add_im complex.smul_im) _
 lemma convex_halfspace_im_lge (r : ℝ) : convex {c : ℂ | r ≤ c.im} :=
 convex_halfspace_ge _ (is_linear_map.mk complex.add_im complex.smul_im) _
 
+section submodule
+
+open submodule
+
+lemma convex_submodule (K : submodule ℝ α) : convex (↑K : set α) :=
+by { repeat {intro}, refine add_mem _ (smul_mem _ _ _) (smul_mem _ _ _); assumption }
+
+lemma convex_subspace (K : subspace ℝ α) : convex (↑K : set α) := convex_submodule K
+
+end submodule
+
 lemma convex_sum {γ : Type*} (hA : convex A) (z : γ → α) (s : finset γ) :
   ∀ a : γ → ℝ, s.sum a = 1 → (∀ i ∈ s, 0 ≤ a i) → (∀ i ∈ s, z i ∈ A) → s.sum (λi, a i • z i) ∈ A :=
 begin