α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (∫⁻ (a : α), f a ^ p ∂μ) = 0
⊢ f =ᵐ[μ] 0
rw [lintegral_eq_zero_iff' (hf.pow_const p)] at hf_zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
x : α
⊢ (fun x => f x ^ p) x = OfNat.ofNat 0 x → f x = OfNat.ofNat 0 x
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0
refine' Filter.Eventually.mp hf_zero (Filter.eventually_of_forall fun x => _)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
x : α
⊢ f x ^ p = OfNat.ofNat 0 x → f x = OfNat.ofNat 0 x
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
x : α
⊢ (fun x => f x ^ p) x = OfNat.ofNat 0 x → f x = OfNat.ofNat 0 x
dsimp only
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
x : α
⊢ ¬f x = 0 → ¬f x ^ p = 0
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
x : α
⊢ f x ^ p = OfNat.ofNat 0 x → f x = OfNat.ofNat 0 x
rw [Pi.zero_apply, ← not_imp_not]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f
hf_zero : (fun x => f x ^ p) =ᵐ[μ] 0
x : α
⊢ ¬f x = 0 → ¬f x ^ p = 0
exact fun hx => (rpow_pos_of_nonneg (pos_iff_ne_zero.2 hx) hp0).ne'