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 eq_zero_of_le_not_lt {m : ℝ} (m_nonneg : 0 ≤ m) (tt : ¬ 0 < m) : m = 0 := begin
  cases lt_or_eq_of_le m_nonneg,
  exfalso,
  exacts [tt h, eq.symm h],
end

set_option profiler true

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)),
  have a3_nonneg : 0 ≤ a ^ 3 := pow_nonneg ha 3,
  have b3_nonneg : 0 ≤ b ^ 3 := pow_nonneg hb 3,
  have 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],
      {
        conv_rhs 
        {
         rw [← mul_div_assoc, mul_comm, mul_div_assoc],
         rw [div_self ((by linarith : (3 : ℝ) ≠ 0)), mul_one],
        }
      },
      {
          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,
  by_cases hmmm : m > 0,
  have hhhh : (a1 * b1 * c1) ^ 4 ≤ (m ^ 3) ^ 4 :=
  begin
    have 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,
    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,
    exact pow_le_pow_of_le_left LHS_nonneg hhh 4,
  end,
  rw [mul_pow,mul_pow,ha1,hb1,hc1,← mul_pow,← mul_pow] at hhhh,
  rw [← pow_mul, (mul_comm _ _ : 3 * 4 = 4 * 3), pow_mul] at hhhh,
  have h1 : 3 * (a * b * c) ≤ 3 * m ^ 4 :=
  begin
    have h0 : a * b * c ≤ m ^ 4 :=
    begin
      by_contradiction a1,
      rw not_le at a1,
      exact lt_irrefl ((m ^ 4) ^ 3) (lt_of_lt_of_le (pow_lt_pow_of_lt_left a1 (pow_nonneg (sqrt_nonneg _) 4) (show 0 < 3, by norm_num)) hhhh),
    end,
    exact (mul_le_mul_left (by norm_num : 0 < (3:ℝ))).mpr h0,
  end,
  rwa ← hm at h1,
  have m_nonneg : 0 ≤ m := sqrt_nonneg _,
  have m0 : m = 0 := eq_zero_of_le_not_lt m_nonneg hmmm,
  rw m0 at hm,
  simp only [zero_pow, nat.succ_pos', mul_zero] at hm,
  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 only [a3_nonneg, b3_nonneg, c3_nonneg, hm, a3_pos],
    end,
  rw a0,
  simp only [zero_pow, nat.succ_pos', zero_mul, zero_add, mul_zero],
  exact add_nonneg b3_nonneg c3_nonneg,
end

#lint