α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ (∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ) = 1
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ (∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ) = 1
simp only [div_eq_mul_inv]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ ((∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ) + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ) = 1

case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ AEMeasurable fun a => f a ^ p * (ENNReal.ofReal p)⁻¹
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ (∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ) = 1
rw [lintegral_add_left']
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ ((∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ) + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ) = 1
rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm, ←
  div_eq_mul_inv, ← div_eq_mul_inv, hpq.inv_add_inv_conj_ennreal]
no goals
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ⊤
simp [hpq.symm.pos]
no goals
case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p q
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_norm : (∫⁻ (a : α), f a ^ p ∂μ) = 1
hg_norm : (∫⁻ (a : α), g a ^ q ∂μ) = 1
⊢ AEMeasurable fun a => f a ^ p * (ENNReal.ofReal p)⁻¹
exact (hf.pow_const _).mul_const _