-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_Lp_add_le_of_le_one {p : ℝ} {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hp0 : 0 ≤ p)
    (hp1 : p ≤ 1) :
    (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤
      (2 : ℝ≥0∞) ^ (1 / p - 1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p))

Proof state:
case h₁.hfg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
a : α
⊢ (f + g) a ^ p ≤ f a ^ p + g a ^ p

Tactic:
exact rpow_add_le_add_rpow _ _ hp0 hp1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : 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)

Tactic:
rw [← lintegral_add_left' (hf.pow_const p)]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : 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 + g a ^ p ∂μ) ^ (1 / p)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : 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 + g a ^ p ∂μ) ^ (1 / p)

Tactic:
gcongr with a

Result:
case h₁.hfg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
a : α
⊢ (f + g) a ^ p ≤ f a ^ p + g a ^ p

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : 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))

Tactic:
rcases eq_or_lt_of_le hp0 with (rfl | hp)

Result:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : 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 α
μ : 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))

Proof state:
case inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : 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))

Tactic:
calc
  (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ ((∫⁻ a, f a ^ p ∂μ) + ∫⁻ a, g a ^ p ∂μ) ^ (1 / p) := by
    rw [← lintegral_add_left' (hf.pow_const p)]
    gcongr with a
    exact 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)

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * 2

Tactic:
rw [rpow_neg, rpow_one, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : 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))

Tactic:
simp only [Pi.add_apply, rpow_zero, lintegral_one, _root_.div_zero, zero_sub]

Result:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * (1 + 1)

Proof state:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * (1 + 1)

Tactic:
norm_num

Result:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * 2