α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
refine' le_trans le_top (le_of_eq _)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
have hp0_inv_lt : 0 < 1 / p := by simp [hp0_lt]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = ⊤ * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
rw [hf_top, ENNReal.top_rpow_of_pos hp0_inv_lt]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
hp0_inv_lt : 0 < 1 / p
⊢ ⊤ = ⊤ * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
simp [hq0, hg_nonzero]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p q : ℝ
hp0_lt : 0 < p
hq0 : 0 ≤ q
f g : α → ℝ≥0∞
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_nonzero : (∫⁻ (a : α), g a ^ q ∂μ) ≠ 0
⊢ 0 < 1 / p
simp [hp0_lt]