α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
refine' le_trans (ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf (hg.pow_const _)) _
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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 α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
by_cases hf_zero_rpow : (∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) = 0
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
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
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
refine' (ENNReal.mul_le_mul_left hf_zero_rpow hf_top_rpow).mpr (le_of_eq _)
case neg.e_a.e_f
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
congr
case neg.e_a.e_f.h
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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
case neg.e_a.e_f
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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
ext1 a
no goals
case neg.e_a.e_f.h
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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
rw [← ENNReal.rpow_mul, hpq.sub_one_mul_conj]
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
rw [hf_zero_rpow, MulZeroClass.zero_mul]
no goals
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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)
exact zero_le _
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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) ≠ ⊤
by_contra h
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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 ∂μ) = ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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
refine' hf_top _
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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 ∂μ) = ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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 ∂μ) = ⊤
have hp_not_neg : ¬p < 0 := by simp [hpq.nonneg]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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 ∂μ) = ⊤
simpa [hpq.pos, hp_not_neg] using h
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hpq : Real.IsConjugateExponent p 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
simp [hpq.nonneg]