integrable_withDensity_iff_integrable_smul₀'

English

If f is a.e.-measurable and nonnegative, Integrable g with μ.withDensity f is equivalent to Integrable (f.toReal • g) μ.

Русский

Если f измеримо по почти всей мере и неотрицательно, Integrable g с μ.withDensity f эквивалентно Integrable (f.toReal • g) μ.

LaTeX

$$Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ$$

Lean4

theorem integrable_withDensity_iff_integrable_smul₀' {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hflt : ∀ᵐ x ∂μ, f x < ∞)
    {g : α → E} : Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ :=
  by
  rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt), integrable_withDensity_iff_integrable_coe_smul₀]
  · congr!
  · exact hf.ennreal_toNNReal

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