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

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
⊢ (f a + g a) ^ p ≤ 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p

Tactic:
have h_zero_lt_half_rpow : (0 : ℝ≥0∞) < (1 / 2 : ℝ≥0∞) ^ p := by
  rw [← ENNReal.zero_rpow_of_pos hp0_lt]
  exact ENNReal.rpow_lt_rpow (by simp [zero_lt_one]) hp0_lt

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
h_zero_lt_half_rpow : 0 < (1 / 2) ^ p
⊢ (f a + g a) ^ p ≤ 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
⊢ 0 < (1 / 2) ^ p

Tactic:
rw [← ENNReal.zero_rpow_of_pos hp0_lt]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
⊢ 0 ^ p < (1 / 2) ^ p

Proof state:
case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
h_two : 2 ^ (p - 1) ≠ ⊤
⊢ AEMeasurable (fun a => 2 ^ (p - 1) * f a ^ p) μ

Tactic:
exact (hf.pow_const p).const_mul _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
h_two : 2 ^ (p - 1) ≠ ⊤
⊢ ∫⁻ (a : α), 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p ∂μ < ⊤

Tactic:
rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
  lintegral_const_mul' _ _ h_two, ENNReal.add_lt_top]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
h_two : 2 ^ (p - 1) ≠ ⊤
⊢ 2 ^ (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ⊤ ∧ 2 ^ (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ⊤

case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
h_two : 2 ^ (p - 1) ≠ ⊤
⊢ AEMeasurable (fun a => 2 ^ (p - 1) * f a ^ p) μ

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
h_two : 2 ^ (p - 1) ≠ ⊤
⊢ 2 ^ (p - 1) * ∫⁻ (a : α), f a ^ p ∂μ < ⊤ ∧ 2 ^ (p - 1) * ∫⁻ (a : α), g a ^ p ∂μ < ⊤

Tactic:
exact ⟨ENNReal.mul_lt_top h_two.lt_top hf_top, ENNReal.mul_lt_top h_two.lt_top hg_top⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
h_zero_lt_half_rpow : 0 < (1 / 2) ^ p
h_rw : (1 / 2) ^ p * 2 ^ (p - 1) = 1 / 2
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
rw [ENNReal.div_add_div_same, one_add_one_eq_two,
  ENNReal.div_self two_ne_zero ENNReal.coe_ne_top]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
⊢ 0 ^ p < (1 / 2) ^ p

Tactic:
exact ENNReal.rpow_lt_rpow (by simp [zero_lt_one]) hp0_lt

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
⊢ ∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤

Tactic:
have hp0_lt : 0 < p := lt_of_lt_of_le zero_lt_one hp1

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
⊢ ∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
h_zero_lt_half_rpow : 0 < (1 / 2) ^ p
⊢ (f a + g a) ^ p ≤ 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p

Tactic:
have h_rw : (1 / 2 : ℝ≥0∞) ^ p * (2 : ℝ≥0∞) ^ (p - 1) = 1 / 2 := by
  rw [sub_eq_add_neg, ENNReal.rpow_add _ _ two_ne_zero ENNReal.coe_ne_top, ← mul_assoc, ←
    ENNReal.mul_rpow_of_nonneg _ _ hp0, one_div,
    ENNReal.inv_mul_cancel two_ne_zero ENNReal.coe_ne_top, ENNReal.one_rpow, one_mul,
    ENNReal.rpow_neg_one]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
h_zero_lt_half_rpow : 0 < (1 / 2) ^ p
h_rw : (1 / 2) ^ p * 2 ^ (p - 1) = 1 / 2
⊢ (f a + g a) ^ p ≤ 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
h_zero_lt_half_rpow : 0 < (1 / 2) ^ p
h_rw : (1 / 2) ^ p * 2 ^ (p - 1) = 1 / 2
⊢ (1 / 2) ^ p ≠ ⊤

Tactic:
rw [← lt_top_iff_ne_top]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
h_zero_lt_half_rpow : 0 < (1 / 2) ^ p
h_rw : (1 / 2) ^ p * 2 ^ (p - 1) = 1 / 2
⊢ (1 / 2) ^ p < ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
hp1 : 1 ≤ p
hp0_lt : 0 < p
hp0 : 0 ≤ p
a : α
⊢ 0 < 1 / 2

Tactic:
simp [zero_lt_one]

Result:
no goals