Kazakhstan District 2025 Grade 11 Problem 1

Let $a, b$ be non-negative real numbers such that $a + b = 1$. Show that $$\frac{a ^ 2 + b ^ 2}{2} \le a ^ 3 + b ^ 3 \le a ^ 2 + b ^ 2.$$

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.34.0.

import Mathlib.Data.Real.Basic

theorem solution (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : a + b = 1) :
    (a ^ 2 + b ^ 2) / 2 ≤ a ^ 3 + b ^ 3 ∧ a ^ 3 + b ^ 3 ≤ a ^ 2 + b ^ 2 := sorry

Submit Solution

Login to submit a solution.

Recent Submissions