α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : (∫⁻ (a : α), f a ^ p ∂μ) ≠ 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
⊢ (∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ) = 1
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : (∫⁻ (a : α), f a ^ p ∂μ) ≠ 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
⊢ (∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ) = 1
simp_rw [funMulInvSnorm_rpow hp0_lt]
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : (∫⁻ (a : α), f a ^ p ∂μ) ≠ 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
⊢ (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : (∫⁻ (a : α), f a ^ p ∂μ) ≠ 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
⊢ (∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ) = 1
rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]
no goals
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : (∫⁻ (a : α), f a ^ p ∂μ) ≠ 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
⊢ (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ⊤
rwa [inv_ne_top]