α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) = lintegral μ 0
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) = 0
rw [← @lintegral_zero_fun α _ μ]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (fun a => (f * g) a) =ᵐ[μ] fun a => OfNat.ofNat 0 a
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f * g) a ∂μ) = lintegral μ 0
refine' lintegral_congr_ae _
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
h_mul_zero : f * g =ᵐ[μ] 0 * g
⊢ (fun a => (f * g) a) =ᵐ[μ] fun a => OfNat.ofNat 0 a

case h_mul_zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ f * g =ᵐ[μ] 0 * g
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ (fun a => (f * g) a) =ᵐ[μ] fun a => OfNat.ofNat 0 a
suffices h_mul_zero : f * g =ᵐ[μ] 0 * g
case h_mul_zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
hf_eq_zero : f =ᵐ[μ] 0
⊢ f * g =ᵐ[μ] 0 * g
case h_mul_zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ f * g =ᵐ[μ] 0 * g
have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero
no goals
case h_mul_zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
hf_eq_zero : f =ᵐ[μ] 0
⊢ f * g =ᵐ[μ] 0 * g
exact hf_eq_zero.mul (ae_eq_refl g)
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
h_mul_zero : f * g =ᵐ[μ] 0 * g
⊢ (fun a => (f * g) a) =ᵐ[μ] fun a => OfNat.ofNat 0 a
rwa [MulZeroClass.zero_mul] at h_mul_zero