-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {p q : ℝ}
    (hpq : p.IsConjExponent q) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) :
    (∫⁻ a, f a * g a ^ (p - 1) ∂μ) ≤
      (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ p ∂μ) ^ (1 / q)

Proof state:
case neg.e_a.e_f
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
⊢ (fun a => (g a ^ (p - 1)) ^ q) = fun a => g a ^ p

Tactic:
ext1 a

Result:
case neg.e_a.e_f.h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
a : α
⊢ (g a ^ (p - 1)) ^ q = g a ^ p

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Tactic:
refine (ENNReal.mul_le_mul_left hf_zero_rpow hf_top_rpow).mpr (le_of_eq ?_)

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
⊢ (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) = (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Tactic:
have hf_top_rpow : (∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) ≠ ⊤ := by
  by_contra h
  refine hf_top ?_
  have hp_not_neg : ¬p < 0 := by simp [hpq.nonneg]
  simpa [hpq.pos, hp_not_neg] using h

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
h : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = ⊤
⊢ ∫⁻ (a : α), f a ^ p ∂μ = ⊤

Tactic:
have hp_not_neg : ¬p < 0 := by simp [hpq.nonneg]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
h : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = ⊤
hp_not_neg : ¬p < 0
⊢ ∫⁻ (a : α), f a ^ p ∂μ = ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Tactic:
by_cases hf_zero_rpow : (∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) = 0

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
h : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = ⊤
⊢ False

Tactic:
refine hf_top ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
h : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = ⊤
⊢ ∫⁻ (a : α), f a ^ p ∂μ = ⊤

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
⊢ (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) = (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Tactic:
congr

Result:
case neg.e_a.e_f
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
⊢ (fun a => (g a ^ (p - 1)) ^ q) = fun a => g a ^ p

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
⊢ 0 ≤ 0 * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Tactic:
exact zero_le _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
h : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = ⊤
hp_not_neg : ¬p < 0
⊢ ∫⁻ (a : α), f a ^ p ∂μ = ⊤

Tactic:
simpa [hpq.pos, hp_not_neg] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
h : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = ⊤
⊢ ¬p < 0

Tactic:
simp [hpq.nonneg]

Result:
no goals