English
For ENNReal with a sum constraint, rpow_arith_mean ≤ arith_mean_rpow in the stated regime.
Русский
Для ENNReal, где сумма нормирована, выполняется rpow_arith_mean ≤ arith_mean_rpow в указанном режиме.
LaTeX
$$$\text{rpow_arith_mean_le_arith_mean_rpow}(w,z,hw',p)\Rightarrow (\cdot) \le (\cdot)$$$
Lean4
theorem add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0∞) (hp1 : 1 ≤ p) : a ^ p + b ^ p ≤ (a + b) ^ p :=
by
have hp_pos : 0 < p := by positivity
by_cases h_top : a + b = ⊤
· rw [← @ENNReal.rpow_eq_top_iff_of_pos (a + b) p hp_pos] at h_top
rw [h_top]
exact le_top
obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top
lift a to ℝ≥0 using ha_top
lift b to ℝ≥0 using hb_top
simpa [ENNReal.coe_rpow_of_nonneg _ hp_pos.le] using ENNReal.coe_le_coe.2 (NNReal.add_rpow_le_rpow_add a b hp1)
