lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero

English

If f is nonnegative and ∫ f^p dμ = 0, then ∫ (f g) dμ = 0 for any a.e. measurable g.

Русский

Если f неотрицательна и ∫ f^p dμ = 0, тогда ∫ (f g) dμ = 0 для любой a.e.-измеримой g.

LaTeX

$$$0 \\le p,\\; f,g:\\alpha\\to\\mathbb{R}_{\\ge 0}^{\\infty},\\; AEMeasurable f\\,μ, AEMeasurable g\\,μ,\\; ∫ f^p dμ = 0 \\Rightarrow ∫ (f g) dμ = 0$$$

Lean4

theorem lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0 : 0 ≤ p) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hf_zero : ∫⁻ a, f a ^ p ∂μ = 0) : (∫⁻ a, (f * g) a ∂μ) = 0 :=
  by
  rw [← @lintegral_zero_fun α _ μ]
  refine lintegral_congr_ae ?_
  suffices h_mul_zero : f * g =ᵐ[μ] 0 * g by rwa [zero_mul] at h_mul_zero
  have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero
  exact hf_eq_zero.mul (ae_eq_refl g)

Похожие утверждения