Theorem: Imo2001P2.bound (Compfiles/Imo2001P2.lean)

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) ≤ a ^ 3 / √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
Tactic:
rw [div_le_div_iff (by positivity) (by positivity)]
State after:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)
Tactic:
calc a ^ 4 * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)
    = a ^ 3 * (a * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)) := by ring
  _ ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4) := ?_
State after:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 3 * (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 3 * (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)
Tactic:
gcongr
State after:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 4 + b ^ 4 + c ^ 4

State before:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 4 + b ^ 4 + c ^ 4
Tactic:
apply le_of_pow_le_pow_left two_ne_zero (by positivity)
State after:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ^ 2 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2

State before:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ^ 2 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2
Tactic:
rw [mul_pow, sq_sqrt (by positivity), ← sub_nonneg]
State after:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)

State before:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
Tactic:
calc
  (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
    = 2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 +
      (2 * (a ^ 2 * b * c - b ^ 2 * c ^ 2)) ^ 2 := by ring
  _ ≥ 0 := by positivity
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 < a ^ 4 + b ^ 4 + c ^ 4
Tactic:
positivity
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 < √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
Tactic:
positivity
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) = a ^ 3 * (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3))
Tactic:
ring
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ a ^ 4 + b ^ 4 + c ^ 4
Tactic:
positivity
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ (a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3
Tactic:
positivity
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) =
    2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 + (2 * (a ^ 2 * b * c - b ^ 2 * c ^ 2)) ^ 2
Tactic:
ring
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 + (2 * (a ^ 2 * b * c - b ^ 2 * c ^ 2)) ^ 2 ≥ 0
Tactic:
positivity
State after:
no goals