case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (∫⁻ (a : α), (f + g) a ^ 0 ∂μ) ^ (1 / 0) ≤
    2 ^ (1 / 0 - 1) * ((∫⁻ (a : α), f a ^ 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), g a ^ 0 ∂μ) ^ (1 / 0))

case inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
rcases eq_or_lt_of_le hp0 with (rfl | hp)
no goals
case inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
calc
  (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ ((∫⁻ a, f a ^ p ∂μ) + ∫⁻ a, g a ^ p ∂μ) ^ (1 / p) := by
    apply rpow_le_rpow _ (div_nonneg zero_le_one hp0)
    rw [← lintegral_add_left' (hf.pow_const p)]
    exact lintegral_mono fun a => rpow_add_le_add_rpow _ _ hp0 hp1
  _ ≤ (2 : ℝ≥0∞) ^ (1 / p - 1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) :=
    rpow_add_le_mul_rpow_add_rpow _ _ ((one_le_div hp).2 hp1)
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * (1 + 1)
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (∫⁻ (a : α), (f + g) a ^ 0 ∂μ) ^ (1 / 0) ≤
    2 ^ (1 / 0 - 1) * ((∫⁻ (a : α), f a ^ 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), g a ^ 0 ∂μ) ^ (1 / 0))
simp only [Pi.add_apply, rpow_zero, lintegral_one, _root_.div_zero, zero_sub]
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * 2
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * (1 + 1)
norm_num
no goals
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * 2
rw [rpow_neg, rpow_one, ENNReal.inv_mul_cancel two_ne_zero two_ne_top]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) + ∫⁻ (a : α), g a ^ p ∂μ
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ ((∫⁻ (a : α), f a ^ p ∂μ) + ∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
apply rpow_le_rpow _ (div_nonneg zero_le_one hp0)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≤ ∫⁻ (a : α), f a ^ p + g a ^ p ∂μ
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) + ∫⁻ (a : α), g a ^ p ∂μ
rw [← lintegral_add_left' (hf.pow_const p)]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≤ ∫⁻ (a : α), f a ^ p + g a ^ p ∂μ
exact lintegral_mono fun a => rpow_add_le_add_rpow _ _ hp0 hp1