integrable_withDensity_iff_integrable_smul

English

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

Русский

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

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