cauchy schwartz real inner product space

cauchy_schwartz.lean

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.NormedSpace.Basic

variable (F : Type) [LinearOrder F] [NormedAddCommGroup F] [InnerProductSpace ℝ F]

open RealInnerProductSpace

-- https://en.wikipedia.org/wiki/Cauchy%E2%80%93Schwarz_inequality
theorem cauchy_schwarz_inequality (u v : F) :
  |⟪u, v⟫| ^ 2 ≤ ⟪u, u⟫ * ⟪v, v⟫ := by {
    simp

    -- create new variable t, and use it to rewrite hh
    let t := ⟪u, v⟫ / ⟪v, v⟫
    have hh : 0 ≤ ⟪u - t • v, u - t • v⟫ := real_inner_self_nonneg
    rw [
      inner_sub_left, inner_sub_right, inner_smul_right, inner_sub_right,
      inner_smul_right, real_inner_smul_left, real_inner_smul_left, real_inner_comm u v
    ] at hh

    -- reduce hh to 0 ≤ inner u u - inner u v ^ 2 * (inner v v)⁻¹
    ring_nf at hh; simp at hh
    rw [mul_assoc, <- inv_pow, pow_two, pow_two, <- pow_two, mul_comm, <- mul_assoc] at hh
    field_simp at hh; ring_nf at hh

    -- handle the case where v is zero
    by_cases hv_iszero : v = 0
    simp [hv_iszero]
    push_neg at hv_iszero

    -- handle the case where v is negative / positive
    cases' lt_or_gt_of_ne hv_iszero with hv_neg hv_pos

    -- handle the case where v < 0
    have hv_nonneg : 0 ≤ ⟪v, v⟫ := real_inner_self_nonneg
    obtain hv_pos | hv_zero := lt_or_eq_of_le hv_nonneg
    have hhh := mul_le_mul_of_nonneg_left hh (le_of_lt hv_pos)
    simp [mul_sub, mul_comm _ (⟪v, v⟫)⁻¹, mul_inv_cancel_left₀ (ne_of_gt hv_pos), mul_comm] at hhh
    assumption

    -- handle the case where inner v v = 0
    rw [eq_comm, inner_self_eq_zero] at hv_zero
    contradiction

    -- handle the case where v > 0
    have hv_nonneg : 0 ≤ ⟪v, v⟫ := real_inner_self_nonneg
    obtain hv_inner_neg | hv_inner_zero := lt_or_eq_of_le hv_nonneg
    have hhh := mul_le_mul_of_nonneg_left hh (le_of_lt hv_inner_neg)
    simp [mul_sub, mul_comm _ (⟪v, v⟫)⁻¹, mul_inv_cancel_left₀ (ne_of_gt hv_inner_neg), mul_comm] at hhh
    assumption

    -- handle the case where inner v v = 0
    rw [eq_comm, inner_self_eq_zero] at hv_inner_zero
    contradiction
  }