BalkanMOP2.lean

import data.real.basic
import algebra
import tactic
import algebra.quadratic_discriminant
import algebra.ordered_field
import algebra.ordered_group
import algebra.ordered_ring

open classical
local attribute [instance] prop_decidable


theorem geq_one (a b : ℝ) (ha: 1 ≤ a) (hb: 1 ≤ b): 1 ≤ a * b :=
begin
have ha': 0 ≤ a, {linarith,}, 
calc 1 ≤ a: by exact ha
... ≤ a * b: by exact le_mul_of_one_le_right ha' hb,
end

theorem AMGM (a b : ℝ) (ha: 0 ≤ a) (hb: 0 ≤ b): a + b ≥ 2*real.sqrt(a*b):=
begin
have ineq1: a+b ≥ 0, {linarith,}, 
have eq3: real.sqrt(4)=2,
{
    have obs1: (2:ℝ)^2=(4:ℝ), {ring,}, have obs2: (0:ℝ) ≤ 2, {linarith,}, have obs3: 0 ≤ 4, {linarith,}, rw ← obs1, 
    exact real.sqrt_sqr obs2,
},
have ineq: (a+b)^2 ≥ 4 *(a*b),
{
    have obs1: (a+b)^2-4*a*b=(a-b)^2, {ring,}, have obs2: 0 ≤ (a+b)^2-4*a*b, {rw obs1, exact pow_two_nonneg (a - b),},
    linarith,
},
have ineq2: real.sqrt((a+b)^2) ≥ real.sqrt(4*(a*b)), {exact real.sqrt_le_sqrt ineq,},
rw ((4:ℝ).sqrt_mul' (mul_nonneg ha hb)) at ineq2, rw eq3 at ineq2, have obs: real.sqrt((a+b)^2)=a+b, {exact real.sqrt_sqr ineq1,}, rw obs at ineq2, exact ineq2,
end

theorem mul_mul_div_self' (a b c : ℝ) (hb: b ≠ 0) (hc: c ≠ 0): a/b = (a*c)/(b*c):=
begin
have fact: a/b = a/b*1, {ring,}, rw ← (div_self hc) at fact, rw ← div_mul_div a b c c, exact fact,
end

lemma useful (a : ℝ) (ha: 0 ≤ a ∧ a ≤ 1): (2/(a+1))^2-2*(1-a)*(2/(a+1))-a ≤ 0:=
begin
cases ha with ha1 ha2, have obva: a + 1 > 0, {linarith,},
have rk1: (2/(a+1))^2=(2/(a+1))*(2/(a+1)), {ring,}, have rk2: (2/(a+1))*(2/(a+1)) = (2*2)/((a+1)*(a+1)), {exact div_mul_div 2 (a+1) 2 (a+1)}, 
have rk3: (2:ℝ)*2=4, {linarith,}, have rk4: (a+1)*(a+1)=(a+1)^2, {ring,}, rw rk3 at rk2, rw rk4 at rk2, clear rk3 rk4,
have rk3: 2*(1-a)*(2/(a+1))=(2/(a+1))*(2*(1-a)), {ring,}, have rk4: (2/(a+1))*(2*(1-a)) = (2*(2*(1-a)))/(a+1), {exact div_mul_eq_mul_div (2*(1-a)) 2 (a+1),},
have rk5: 2*(2*(1-a))=4*(1-a), {ring,}, rw rk5 at rk4, 
rw [rk1, rk2, rk3, rk4], clear rk1 rk2 rk3 rk4 rk5, 
have rk2: 4/(a+1)^2 - 4*(1-a)/(a+1)-a = (4/(a+1)^2-4*(1-a)/(a+1))-a, {ring,},  have rks: (a+1)*(a+1)=(a+1)^2, {ring,},
have rk3: (1-a)/(a+1)=(1-a)*(a+1)/(a+1)^2, {rw mul_mul_div_self' (1-a) (a+1) (a+1) (ne_of_gt obva), rw rks, exact (ne_of_gt obva),}, clear rks,
have rk4: 4*(1-a)/(a+1) = 4*((1-a)/(a+1)), {ring,}, rw [rk4, rk3],
have fact: 4/(a+1)^2 - 4*(1-a)*(a+1)/(a+1)^2 = 4*(a^2)/(a+1)^2,
{
rw div_sub_div_same 4 (4*(1-a)*(a+1)) ((a+1)^2), have obs: 4 - 4*(1-a)*(a+1)=4*a^2, {ring,}, rw obs,
}, 
have fact'': 4 / (a+1)^2 - 4 * ((1-a)*(a+1)/(a+1)^2) - a = 4/(a+1)^2 - 4*(1-a)*(a+1)/(a+1)^2-a, {ring,}, rw [fact'', fact],
have obs: a = a / 1 , {ring,}, have obs2: a / 1 = (a * (a+1)^2) / ((a+1)^2), {rw mul_mul_div_self' a 1 ((a+1)^2) _ _, rw one_mul, linarith, linarith [(pow_pos obva 2)],},
rw obs2 at obs, 
rw (congr_arg (has_sub.sub (4 * a ^ 2 / (a + 1) ^ 2)) obs), have obs4: a*(a+1)^2=a^3+2*a^2+a, {ring,}, rw obs4, rw div_sub_div_same (4*a^2) (a^3+2*a^2+a) ((a+1)^2),
have obs5: 4*a^2-(a^3+2*a^2+a)=-a*(a-1)^2, {ring,}, rw obs5, 
exact div_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr ha1) (pow_two_nonneg (a - 1))) (pow_two_nonneg (a + 1)),
end

--Let a, b, c be three real numbers, such that 0 ≤ a ≤ b ≤ c and a+b+c = ab+bc+ca > 0. Prove that √(bc)*(a+1)≥2.

theorem BP2 (a b c : ℝ) (habc1: 0 ≤ a ∧ a ≤ b ∧ b ≤ c) (habc2: a+b+c = a*b + b*c + c*a ∧ 0 < a + b + c):
(real.sqrt(b*c))*(a+1)≥2:=
begin
let t:=real.sqrt(b*c), cases habc1 with ha hbc1, cases hbc1 with hb1 hc1, have obva: a + 1 > 0, {linarith,},
have hb: 0 ≤ b, {linarith,}, have hc: 0 ≤ c, {linarith,}, 
cases (lt_or_ge a 1) with ha1 ha2,
{
have obs: 1 - a > 0, {linarith,}, have obs2: t*t=b*c, {exact real.mul_self_sqrt (mul_nonneg hb hc),}, have obv: t*t=t^2, {ring,}, have ha1': a ≤ 1, {linarith,},
rw obv at obs2, clear obv, cases habc2 with h1 h2, 
have fact: b*c=a+b+c-a*b-c*a, {linarith,}, have fact': a+b+c-a*b-c*a=a+(1-a)*(b+c),{ring,},
have ineq2: a + (1-a)*(b+c) ≥ a + 2*(1-a)*t, {linarith [((mul_le_mul_left obs).mpr (AMGM b c hb hc))],}, rw ← obs2 at fact, rw ← fact at fact', rw ← fact' at ineq2,
have ineq3: t^2-2*(1-a)*t - a ≥ 0, {linarith,},  
have quadratic1: discrim 1 (-(2*(1-a))) (-a) ≥ 0, 
{
rw discrim, have obs: (-(2*(1-a)))^2-4*1*(-a)=4*(a^2-a+1), {ring,}, 
linarith [neg_le_neg ha1', pow_two_nonneg a],
},
let s:= real.sqrt(discrim 1 (-(2*(1-a))) (-a)), 
let x1:= (2*(1-a) + s)/2, let x2:= (2*(1-a)-s)/2, have obv1: x1=(2*(1-a) + s)/2, {refl,}, have obv2: x2=(2*(1-a)-s)/2, {refl,},
have eq2: ∀ t : ℝ, t^2-2*(1-a)*t-a=(t-x1)*(t-x2), 
{
intro t,
have obs: (t-x1)*(t-x2)=t^2-(x1+x2)*t+x1*x2, {ring,}, 
have fact1: x1+x2 = 2*(1-a),{rw [obv1, obv2], rw ← (add_div (2*(1-a)+s) (2*(1-a)-s) 2), linarith,}, rw fact1 at obs,
have fact2: x1*x2=-a, 
{
    rw [obv1, obv2], 
    have rk2: (2*(1-a)+s)*(2*(1-a)-s)=4*(1-a)^2-s*s, {ring,}, rw (real.mul_self_sqrt quadratic1) at rk2, rw discrim at rk2, 
    have obs': (-(2*(1-a)))^2-4*1*(-a)=4*(a^2-a+1), {ring,}, rw obs' at rk2, have obs'': 4*(1-a)^2-4*(a^2-a+1)=-4*a, {ring,}, linarith,
},
rw fact2 at obs, tauto,
}, clear ineq2 fact' fact obs2,
have obs': x2 ≤ 0, 
{
have fact1: (2*(1-a))^2 ≤ s*s,
{
rw (real.mul_self_sqrt quadratic1), have rk: (-(2*(1-a)))^2-4*1*(-a)=4*(a^2-a+1), {ring,}, rw discrim, rw rk, have rk2: (2*(1-a))^2=4*(a^2-2*a+1), {ring,}, linarith,
},
have rk: 0 ≤ 2*(1-a), {linarith,}, 
have factf: real.sqrt((2*(1-a))^2) ≤ real.sqrt(s*s), {exact (real.sqrt_le (pow_nonneg rk 2) (le_trans (pow_nonneg rk 2) fact1)).mpr fact1,},
rw [(real.sqrt_sqr rk), (congr_arg real.sqrt (real.mul_self_sqrt quadratic1))] at factf,
linarith,
},
have obs'': 0 ≤ x1,{linarith [(discrim 1 (-(2 * (1 - a))) (-a)).sqrt_nonneg],},
have quadratic_intervals: ∀ x : ℝ, x^2-2*(1-a)*x-a ≤ 0 → ((x2 ≤ x) ∧ (x ≤ x1)), 
{
intros x hx,
cases (lt_or_ge x x2) with hx1 hx2,
{
have rk1: x < x1, {linarith,}, have rk4: (x-x1)*(x-x2)=(x1-x)*(x2-x), {ring,},
have rk5: 0 < (x1-x)*(x2-x), {exact mul_pos (sub_pos.mpr rk1) (sub_pos.mpr hx1),}, exfalso, rw ← rk4 at rk5, rw ← eq2 x at rk5, linarith, 
},
{
cases (le_or_lt x x1) with hx3 hx4,
{
have rk1: (x - x1) * (x - x2) ≤ 0, {exact mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr hx3) (sub_nonneg.mpr hx2)},
rw ← eq2 x at rk1, exact ⟨hx2, hx3⟩,
},
{
have rk1: x2 < x, {linarith,}, have rk2: 0 < (x-x1)*(x-x2), {exact mul_pos (sub_pos.mpr hx4) (sub_pos.mpr rk1),},
exfalso, rw ← eq2 x at rk2, linarith,
},
},
},   
specialize quadratic_intervals (2/(a+1)) (useful a ⟨ha, ha1'⟩),
have quadratic_open_intervals: ∀ x : ℝ, 0 ≤ x^2-2*(1-a)*x-a → ((x ≤ x2) ∨ (x1 ≤ x)),
{
intros x hx, 
cases (le_or_lt x x2) with hx1 hx2,
{left, exact hx1,},
{
cases (lt_or_ge x x1) with hx3 hx4,
{
have rk1: (x-x1)*(x-x2) < 0,{exact mul_neg_of_neg_of_pos (sub_neg_of_lt hx3) (sub_pos.mpr hx2),}, 
exfalso, rw ← eq2 x at rk1, linarith,
},{right, exact hx4,},
},
},
specialize quadratic_open_intervals t ineq3, 
have fact'': 0 < c, {linarith,},
have fact: 0 < b, 
{
by_contradiction, push_neg at a_1, have obs: b = 0, {linarith,}, have obs': a = 0, {linarith ,}, rw [obs, obs'] at h2,
rw [obs, obs'] at h1, clear ha a_1, rw [zero_mul, zero_mul, mul_zero, zero_add, zero_add, zero_add] at h1, rw h1 at h2, linarith,
},
have factf'': ¬(t ≤ x2), {linarith [real.sqrt_pos.mpr (mul_pos fact fact'')],}, have obsf: x1 ≤ t, {tauto,}, clear fact factf'',
have fact: 2/(a+1) ≤ t, {linarith,}, 
have obv: t = real.sqrt (b*c), {refl,}, rw ← obv, linarith [((div_le_iff' obva).mp fact)],
},
{
have fact0: 2 ≤ a + 1, {linarith,},
have fact': 1 ≤ b, {linarith,}, 
have obs2: (0:ℝ) ≤ (1:ℝ), {linarith,}, 
have obs'': 1 ≤ c, {linarith,},
have obs': real.sqrt(1) ≤ real.sqrt(b*c) ↔ 1 ≤ b*c,{exact real.sqrt_le obs2 (mul_nonneg hb hc),},
have theorem1: real.sqrt(1) ≤ real.sqrt(b*c), {exact (real.sqrt_le obs2 (mul_nonneg hb hc)).mpr (geq_one b c fact' obs'')}, 
rw (real.sqrt_one) at theorem1, have obs0: 0 ≤ a+1, {linarith,},
calc 2 ≤ a + 1 : by exact fact0
...≤ real.sqrt(b*c) * (a + 1): by exact le_mul_of_one_le_left obs0 theorem1,
},
end