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_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
by_cases hf_zero : (∫⁻ a, f a ^ p ∂μ) = 0
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : (∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
by_cases hg_zero : (∫⁻ a, g a ^ q ∂μ) = 0
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
by_cases hf_top : (∫⁻ a, f a ^ p ∂μ) = ⊤
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : (∫⁻ (a : α), g a ^ q ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ q ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
by_cases hg_top : (∫⁻ a, g a ^ q ∂μ) = ⊤
no goals
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ q ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
exact ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero
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_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) = 0
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_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
refine' Eq.trans_le _ (zero_le _)
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_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) = 0
exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.nonneg hf hf_zero
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : (∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) = 0
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : (∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
refine' Eq.trans_le _ (zero_le _)
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : (∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (g * f) a ∂μ) = 0
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : (∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) = 0
rw [mul_comm]
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : (∫⁻ (a : α), g a ^ q ∂μ) = 0
⊢ (∫⁻ (a : α), (g * f) a ∂μ) = 0
exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.symm.nonneg hg hg_zero
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.pos hpq.symm.nonneg hf_top hg_zero
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : (∫⁻ (a : α), g a ^ q ∂μ) = ⊤
⊢ (∫⁻ (a : α), (g * f) a ∂μ) ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : (∫⁻ (a : α), g a ^ q ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
rw [mul_comm, mul_comm ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p))]
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_zero : ¬(∫⁻ (a : α), f a ^ p ∂μ) = 0
hg_zero : ¬(∫⁻ (a : α), g a ^ q ∂μ) = 0
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : (∫⁻ (a : α), g a ^ q ∂μ) = ⊤
⊢ (∫⁻ (a : α), (g * f) a ∂μ) ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)
exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.symm.pos hpq.nonneg hg_top hf_zero