integrable_withDensity_iff_integrable_smul₀

English

For a.a.-measurable f≥0, Integrable g with density μ.withDensity f is equivalent to Integrable (f.toReal • g) μ.

Русский

Для a.e.-измеримой f≥0 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 μ) {g : α → E} :
    Integrable g (μ.withDensity fun x => f x) ↔ Integrable (fun x => f x • g x) μ :=
  integrable_withDensity_iff_integrable_coe_smul₀ hf

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