lintegral_withDensity_eq_lintegral_mul_non_measurable₀

English

If f is a.e. measurable with respect to μ and finite μ-a.e., then the density equality holds for all measurable g.

Русский

Пусть f a.e. измерима относительно μ и f<∞ μ-a.e.; тогда равенство плотности выполняется для всех измеримых g.

LaTeX

$$$\int a \, g(a) \ d(\mu.withDensity f) = \int a \, (f(a) \cdot g(a)) \, d\mu$$$

Lean4

theorem lintegral_withDensity_eq_lintegral_mul_non_measurable₀ (μ : Measure α) {f : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (h'f : ∀ᵐ x ∂μ, f x < ∞) (g : α → ℝ≥0∞) : ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, (f * g) a ∂μ :=
  by
  let f' := hf.mk f
  calc
    ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, g a ∂μ.withDensity f' := by rw [withDensity_congr_ae hf.ae_eq_mk]
    _ = ∫⁻ a, (f' * g) a ∂μ :=
      by
      apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]
    _ = ∫⁻ a, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

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