α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∂μ) < ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∂μ) < ⊤
have hp0_lt : 0 < p := lt_of_lt_of_le zero_lt_one hp1
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 + g) a ^ p ∂μ) < ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∂μ) < ⊤
have hp0 : 0 ≤ p := le_of_lt hp0_lt
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∂μ) ≤ ∫⁻ (a : α), 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p ∂μ
refine' lintegral_mono fun a => _
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
dsimp only
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
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]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 * (f a + g a) ^ p ≤ (1 / 2) ^ p * (2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p)

α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ≠ ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
rw [← ENNReal.mul_le_mul_left (ne_of_lt h_zero_lt_half_rpow).symm _]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
rw [← ENNReal.zero_rpow_of_pos hp0_lt]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
exact ENNReal.rpow_lt_rpow (by simp [zero_lt_one]) hp0_lt
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
simp [zero_lt_one]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ (1 / 2) ^ p * 2 ^ (p - 1) = 1 / 2
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]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 * f a + 1 / 2 * g a) ^ p ≤ 1 / 2 * f a ^ p + 1 / 2 * g a ^ p
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 * (f a + g a) ^ p ≤ (1 / 2) ^ p * (2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p)
rw [mul_add, ← mul_assoc, ← mul_assoc, h_rw, ← ENNReal.mul_rpow_of_nonneg _ _ hp0, mul_add]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 * f a + 1 / 2 * g a) ^ p ≤ 1 / 2 * f a ^ p + 1 / 2 * g a ^ p
refine'
  ENNReal.rpow_arith_mean_le_arith_mean2_rpow (1 / 2 : ℝ≥0∞) (1 / 2 : ℝ≥0∞) (f a) (g a) _
    hp1
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
rw [ENNReal.div_add_div_same, one_add_one_eq_two,
  ENNReal.div_self two_ne_zero ENNReal.coe_ne_top]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 < ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ≠ ⊤
rw [← lt_top_iff_ne_top]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ≠ ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 < ⊤
refine' ENNReal.rpow_lt_top_of_nonneg hp0 _
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ 2 ≠ 0
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ≠ ⊤
rw [one_div, ENNReal.inv_ne_top]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ 2 ≠ 0
exact two_ne_zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∂μ) < ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : α), 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p ∂μ) < ⊤
have h_two : (2 : ℝ≥0∞) ^ (p - 1) ≠ ⊤ :=
  ENNReal.rpow_ne_top_of_nonneg (by simp [hp1]) ENNReal.coe_ne_top
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 α
μ : MeasureTheory.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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∂μ) < ⊤
rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
  lintegral_const_mul' _ _ h_two, ENNReal.add_lt_top]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ 0 ≤ p - 1
simp [hp1]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∂μ) < ⊤
exact ⟨ENNReal.mul_lt_top h_two hf_top.ne, ENNReal.mul_lt_top h_two hg_top.ne⟩
no goals
case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
exact (hf.pow_const p).const_mul _