ICMC_4_2_Problem_3.lean

import algebra 
import tactic
import data.real.basic
import data.real.sqrt
import algebra.quadratic_discriminant

structure inner_product (V : Type) [add_comm_group V] [vector_space ℝ V] := 
(inner : V → V → ℝ)
(inner_add_left: ∀ x y z : V, inner (x+y) z= inner x z + inner y z)
(inner_smul_left: ∀ x y : V, ∀ a : ℝ, inner(a • x) y=a * inner x y)
(inner_add_right: ∀ x y z : V, inner x (y+z) = inner x y + inner x z)
(inner_smul_right: ∀ x y: V, ∀ a : ℝ, inner x (a • y)=a * inner x y)
(inner_positive: ∀ x : V, inner x x ≥ 0)
(inner_zero_iff_zero: ∀ x : V, inner x x=0 ↔ x = (0:V))
(inner_comm: ∀ x y : V, inner x y = inner y x)

variables {V: Type} [add_comm_group V] [vector_space ℝ V] 

variable {f: inner_product V}

instance : has_coe_to_fun (inner_product V) :=
⟨_, λ f, f.inner⟩

@[simp] lemma coe_fn_mk (f : V → V → ℝ) (h₁ h₂ h₃ h₄ h₅ h₆ h₇ ) :
  (inner_product.mk f h₁ h₂ h₃ h₄ h₅ h₆ h₇: V → V → ℝ) = f :=
rfl

@[simp] theorem coe_to_inner: ∀ x y : V, f x y = f.inner x y:=
begin
intros x y,
refl,
end

lemma sqrt_exists (a : ℝ) (ha: 0 ≤ a): ∃ b : ℝ, 0 ≤ b ∧ b * b = a:=
begin
use real.sqrt(a),
split,
{
exact real.sqrt_nonneg a,
},
{
exact real.mul_self_sqrt ha,
},
end

lemma sqrt_of_inner_exists: ∀ x : V, ∃ a : ℝ, 0 ≤ a ∧ a * a = f x x:=
begin
intro x,
exact sqrt_exists (f x x) (f.inner_positive x),
end 

local notation `|` x `|` := real.sqrt (f x x)

lemma norm_square_eq_inner_product: ∀ x : V, |x|*|x| = f x x:=
begin
intro x,
exact real.mul_self_sqrt (f.inner_positive x),
end 

lemma Cauchy_Schwartz: ∀ x y : V, abs(f x y) ≤ |x|*|y|:=
begin
intros x y,
have fact': ∀ a : ℝ, f (x + a • y) (x + a • y) = f x x + 2 * a * f x y + a^2 * f y y,
{    
 intro a,
 calc f (x + a • y) (x + a • y) = f x (x + a • y) + f (a • y) (x + a • y): by exact f.inner_add_left x (a • y) (x + a • y)
 ...= f x (x + a • y) + (a * f y (x + a • y)): congr_arg (has_add.add (f x (x + a • y))) (f.inner_smul_left y (x+ a•y) a)
 ...= (f x x + f x (a • y)) + (a * f y (x + a • y)): congr_fun (congr_arg has_add.add (f.inner_add_right x x (a • y))) (a * f y (x + a • y))
 ...= (f x x + (a * f x y)) + (a * f y (x + a • y)): congr (congr_arg has_add.add (congr_arg (has_add.add (f x x)) (f.inner_smul_right x y a))) rfl
 ...= (f x x + (a * f x y)) + (a * (f y x + f y (a • y))): congr_arg (has_add.add (f x x + a * f x y)) (congr_arg (has_mul.mul a) (f.inner_add_right y x (a • y)))
 ...= (f x x + (a * f x y)) + (a * (f y x + (a * f y y))): congr rfl (congr_arg (has_mul.mul a) (congr_arg (has_add.add (f y x)) (f.inner_smul_right y y a)))
 ...= f x x + a * f x y + a * f y x + a^2 * f y y: by ring
 ...= f x x + a * f x y + a * f x y + a^2 * f y y: congr_arg2 has_add.add (congr_arg (has_add.add (f x x + a * f x y)) (congr_arg (has_mul.mul a) (eq.symm (f.inner_comm x y)))) rfl
 ...= f x x + 2 * a * f x y + a ^ 2 * f y y : by ring,
},
have factfinal: ∀ a : ℝ, 0 ≤ f x x + 2 * a * f x y + a ^ 2 * f y y,
{
 intro a,
 calc 0 ≤ f (x + a • y) (x + a • y): f.inner_positive (x + a • y)
 ...= f x x + 2 * a * f x y + a ^ 2 * f y y : fact' a,
},


have factfinal': ∀ a : ℝ, 0 ≤ f x x + 2 * a * f x y + a * a * f y y,
{
 intro a,
 calc 0 ≤ f x x + 2 * a * f x y + a ^ 2 * f y y : factfinal a
 ...= f x x + 2 * a * f x y + a * a * f y y: congr rfl (congr_fun (congr_arg has_mul.mul (eq.symm (pow_two a).symm)) (f y y)),
},

have  factfinal'': ∀ a : ℝ, 0 ≤ f y y * a * a + 2 * f x y * a + f x x,
{
 intro a,
 calc 0 ≤ f x x + 2 * a * f x y + a * a * f y y: factfinal' a
 ...= f y y * a * a + 2 * f x y * a + f x x : by ring,
},

clear fact' factfinal factfinal',

have discrim_def: ∀ a b c : ℝ, discrim a b c = b ^ 2 - 4 * a * c,
{
 intros a b c,
 rw discrim,
},
have fact: (2 * f x y) ^ 2 - 4 * f y y * f x x ≤ 0,
{
 calc (2 * f x y) ^ 2 - 4 * f y y * f x x = discrim (f y y) (2 * f x y) (f x x): eq.symm (discrim_def (f y y) (2 * f x y) (f x x))
 ...≤ 0: discrim_le_zero factfinal'',
},
ring at fact,
have fact': 4 * ((f x y)^2) ≤ 4 * (f x x * f y y),
{
 calc 4 * ((f x y)^2) = 4 * (f x y)^2: by ring
 ...≤ 4 * f x x * f y y: by exact sub_nonpos.mp fact
 ...= 4 * (f x x * f y y): by ring,
},
have h: real.sqrt(f x x * f y y)=real.sqrt(f x x) * real.sqrt (f y y),
{
 exact real.sqrt_mul (f.inner_positive x) (f y y),
},
have obs: real.sqrt((f x y)^2) ≤ real.sqrt(f x x * f y y),
{
 have obs: (0:ℝ) < 4, {linarith,},
 exact real.sqrt_le_sqrt (le_of_mul_le_mul_left fact' obs),
},
rw (f x y).sqrt_sqr_eq_abs at obs,
rw h at obs,
exact obs,
end 

lemma sq_sqrt_eq_num (a : ℝ) (ha: 0 ≤ a): real.sqrt(a)^2 = a:=
begin
rw pow_two (real.sqrt(a)),
exact real.mul_self_sqrt ha,
end

theorem ICMC_Problem_3 (x y z : V) (hyz: f y z = 0) (hy: 0 ≠ f y y) (hz: 0 ≠ f z z): 
|x|^2 ≥ (f x y)^2 /|y|^2 + (f x z)^2 / |z|^2:=
begin
have obs0: f.inner y z = 0,{exact hyz,},
have obs1: ∀ a : ℝ, a * f x y = f y (z + a • x),
{
 intro a,
 rw [coe_to_inner x y, coe_to_inner y (z + a • x)],
 rw f.inner_add_right,
 rw f.inner_smul_right,
 rw f.inner_comm,
 rw obs0,
 rw zero_add,
},
have obs2: ∀ a : ℝ, abs(a * f x y) ≤ |y| * |z + a • x|,
{
 intro a,
 rw obs1,
 exact Cauchy_Schwartz y (z + a • x),
},
have obs3: ∀ a : ℝ, a^2 * (f x y)^2 ≤ |y|^2 * |z + a • x|^2,
{
 intro a,
 rw (mul_pow a (f x y) 2).symm,
 rw (mul_pow (|y|) (|z + a • x|) 2 ).symm,
 exact sqr_le_sqr (obs2 a),
},
rw pow_two(|y|) at obs3,
rw coe_to_inner y at obs3,
rw real.mul_self_sqrt (f.inner_positive y) at obs3,
rw ←(coe_to_inner y y) at obs3,
have fact1: 0 < f y y, {exact (ne.le_iff_lt hy).mp (f.inner_positive y)},
have obs4: ∀ a : ℝ, a^2 * (f x y)^2 / |y|^2 ≤  |z + a • x|^2,
{
 intro a,
 rw pow_two (|y|),
 rw coe_to_inner y,
 rw real.mul_self_sqrt (f.inner_positive y),
 rw ← coe_to_inner y,
 ring,
 rw mul_assoc,
 rw mul_comm ((f x y)^2) (a^2),
 exact (inv_mul_le_iff fact1).mpr (obs3 a),
},
have fact2: ∀ t : V, real.sqrt(f t t)^2 = f t t,
{
 intro t,
 rw coe_to_inner t,
 rw pow_two(real.sqrt(f.inner t t)),
 exact real.mul_self_sqrt (f.inner_positive t),
},
rw fact2 at obs4,
clear obs3 obs2 obs1,
have fact3: ∀ a : ℝ, real.sqrt(f (z + a • x) (z + a • x))^2 = f z z + 2*a*(f x z) + a^2 * (f x x),
{
 intro a,
 rw sq_sqrt_eq_num (f (z + a • x) (z + a • x)) (f.inner_positive (z + a • x)),
 rw coe_to_inner (z + a • x),
 rw coe_to_inner z,
 rw coe_to_inner x z,
 rw coe_to_inner x x,
 rw f.inner_add_right,
 rw f.inner_add_left,
 rw f.inner_smul_left,
 rw f.inner_smul_right,
 rw f.inner_add_left,
 rw f.inner_smul_left,
 rw f.inner_comm z x,
 ring,
},
have obs4': ∀ a : ℝ, a^2 * (f x y)^2 / |y|^2 ≤ f z z + 2*a*(f x z) + a^2 * (f x x),
{
 intro a,
 rw ← fact3 a,
 rw fact2 y,
 exact obs4 a,
},
clear obs4,
rw fact2 y at obs4',
have obs5: ∀ a : ℝ, 0 ≤ (|x|^2 - (f x y)^2 / |y|^2 )*a*a + 2*(f x z)*a + |z|^2 ,
{
 intro a,
 rw fact2 z,
 rw fact2 x,
 rw fact2 y,
 specialize obs4' a,
 ring,
 ring at obs4',
 linarith,
},
have obs6: discrim (|x|^2 - (f x y)^2 / |y|^2 ) (2 * (f x z)) (|z|^2) ≤ 0,
{
 exact discrim_le_zero obs5,
},
clear obs5 obs4',
rw fact2 x at obs6, rw fact2 y at obs6, rw fact2 z at obs6, rw discrim at obs6,
rw fact2 x, rw fact2 y, rw fact2 z,
rw mul_pow 2 (f x z) 2 at obs6,
have fact4: (2:ℝ)^2=(4:ℝ),{ring,},
rw fact4 at obs6,
clear fact4 fact3 obs0 fact1 fact2,
let b := (f x y)^2 / (f y y),
have hb: (f x y)^2 / (f y y) = b, {refl,},
rw hb at obs6,
have fact1: (4 : ℝ)*(f x z)^2 - (4:ℝ)*(f x x - b) * (f z z) = (4 : ℝ)*((f x z)^2 - (f x x)*(f z z) + b * (f z z)),{ring,},
rw fact1 at obs6,
have fact2: 0 ≤ 4, {linarith,},
have obs1: (f x z)^2 - (f x x)*(f z z) + b * (f z z) ≤ 0, {linarith,},
clear obs6,
have fact3: 0 < f z z, {exact (ne.le_iff_lt hz).mp (f.inner_positive z)},
have obs2: (f x z)^2 + b * (f z z) ≤ (f x x)*(f z z), {linarith,}, clear fact1 fact2 obs1,
rw mul_comm (f x x) (f z z) at obs2,
have obs3: ((f x z)^2 + b * (f z z))/(f z z) ≤ f x x, {exact (div_le_iff' fact3).mpr obs2,}, clear obs2 fact3,
have obs4: ((f x z)^2 + b * (f z z))/(f z z) = (f x z)^2 * (f z z)⁻¹ + b*(f z z)*(f z z)⁻¹, {ring,},
have fact4: b * (f z z) * (f z z)⁻¹ = b,
{
 rw mul_assoc,
 rw mul_inv_cancel hz.symm,
 rw mul_one,
},
rw fact4 at obs4,
rw obs4 at obs3,
clear obs4 fact4,
rw ← hb at obs3,
clear hb b,
ring,
ring at obs3,
linarith,
end