add_rpow_le

Stream: Is there code for X?

[Johan Commelin]

Do we have this concavity result somewhere?

import analysis.special_functions.pow

noncomputable theory

-- move this
lemma real.add_rpow_le (x y r : ℝ)
  (hx : 0 ≤ x) (hy : 0 ≤ y) (h0r : 0 ≤ r) (hr1 : r ≤ 1) :
  (x + y)^r ≤ x^r + y^r :=
sorry

[Kyle Miller]

@Johan Commelin docs#ennreal.rpow_add_le_add_rpow is close (it requires r to be positive)

[Johan Commelin]

Thanks

lemma real.add_rpow_le {x y r : ℝ}
  (hx : 0 ≤ x) (hy : 0 ≤ y) (h0r : 0 ≤ r) (hr1 : r ≤ 1) :
  (x + y)^r ≤ x^r + y^r :=
begin
  by_cases hr : 0 = r,
  { subst r, simp only [zero_le_one, real.rpow_zero, le_add_iff_nonneg_left], },
  let x' : ℝ≥0 := ⟨x, hx⟩,
  let y' : ℝ≥0 := ⟨y, hy⟩,
  have := ennreal.rpow_add_le_add_rpow x' y' (lt_of_le_of_ne h0r hr) hr1,
  exact_mod_cast this,
end