test.lean

import data.real.basic
import data.real.nnreal
import data.rat
open real nnreal

lemma ag4 (a b c d : ℝ) : 4 * (a * b * c * d) ≤ a ^ 4 + b ^ 4 + c ^ 4 + d ^ 4 :=
begin
sorry
end

lemma ag3 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) 
  : 3 * (a * b * c) ≤ a ^ 3 + b ^ 3 + c ^ 3 :=
begin
let m := sqrt (sqrt ((a ^ 3 + b  ^ 3 + c ^ 3) / 3)),
let a1 := sqrt (sqrt (a^3)),
let b1 := sqrt (sqrt (b^3)),
let c1 := sqrt (sqrt (c^3)),
let a3_nonneg : 0 ≤ a ^ 3 := pow_nonneg ha 3,
let b3_nonneg : 0 ≤ b ^ 3  := pow_nonneg hb 3,
let c3_nonneg : 0 ≤ c ^ 3  := pow_nonneg hc 3,
have ha1 : a1 ^ 4 = a ^ 3,
  by rw [(show 4 = 2 * 2, by refl),pow_mul,sqr_sqrt (sqrt_nonneg _),sqr_sqrt a3_nonneg],
have hb1 : b1 ^ 4 = b ^ 3,
  by rw [(show 4 = 2 * 2, by refl),pow_mul,sqr_sqrt (sqrt_nonneg _),sqr_sqrt b3_nonneg],
have hc1 : c1 ^ 4 = c ^ 3,
  by rw [(show 4 = 2 * 2, by refl),pow_mul,sqr_sqrt (sqrt_nonneg _),sqr_sqrt c3_nonneg],
have hm : a ^ 3 + b  ^ 3 + c ^ 3 = 3 * m ^ 4,
  begin
  rw [(show 4 = 2 * 2, by refl),pow_mul,sqr_sqrt (sqrt_nonneg _),sqr_sqrt],
  ring,
  apply div_nonneg_of_nonneg_of_pos _ (show 0 < (3:ℝ), by norm_num),
  exact add_nonneg (add_nonneg a3_nonneg b3_nonneg) c3_nonneg,
  end,
let h := ag4 a1 b1 c1 m,
rw [ha1,hb1,hc1,hm] at h,
rw ← mul_assoc at h,
rw (show 3 * m ^ 4 + m ^ 4 = 4 * (m ^ 3) * m, by ring) at h,
by_cases hmmm : m > 0,
have hh : 4 * (a1 * b1 * c1) ≤ 4 * (m ^ 3) := (mul_le_mul_right hmmm).mp h,
have hhh : a1 * b1 * c1 ≤ m ^ 3 := (mul_le_mul_left (show 0 < (4:ℝ), by norm_num)).mp hh,
have LHS_nonneg : 0 ≤ a1 * b1 * c1,
  begin
    apply mul_nonneg,
    apply mul_nonneg,
    exact sqrt_nonneg _,
    exact sqrt_nonneg _,
    exact sqrt_nonneg _,
  end,
let hhhh := pow_le_pow_of_le_left LHS_nonneg hhh 4,
rw [mul_pow,mul_pow,ha1,hb1,hc1,← mul_pow,← mul_pow] at hhhh,
rw [← pow_mul, (show 3 * 4 = 4 * 3, by exact rfl), pow_mul] at hhhh,
have h0 : a * b * c ≤ m ^ 4,
  begin
    by_contradiction a1,
    simp at a1,
    let a2 := pow_lt_pow_of_lt_left a1 (pow_nonneg (sqrt_nonneg _) 4) (show 0 < 3, by norm_num),
    linarith,
  end,
have h1 : 3 * (a * b * c) ≤ 3 * m ^ 4 
  := (mul_le_mul_left (show 0 < (3:ℝ), by norm_num)).mpr h0,
rwa ← hm at h1,

have m_nonneg : m ≥ 0 := sqrt_nonneg _,
have m0 : m = 0 := by linarith,
rw m0 at hm,
conv_rhs at hm {norm_num},
have a0 : a = 0,
  begin
    by_contradiction,
    have ap : 0 < a := lt_of_le_of_ne ha (ne.symm a_1),
    have a3_pos : 0 < a ^ 3 := pow_pos ap 3, 
    linarith,
  end,
rw a0, norm_num, ring,
exact add_nonneg b3_nonneg c3_nonneg,
end