integrable_withDensity_iff — Mathlib

English

If f is AA-measurable, Integrable g (μ.withDensity f) is equivalent to Integrable (f.toReal • g) μ.

Русский

Если f-ae измеримо, 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 {f : α → ℝ≥0∞} (hf : Measurable f) (hflt : ∀ᵐ x ∂μ, f x < ∞) {g : α → ℝ} :
    Integrable g (μ.withDensity f) ↔ Integrable (fun x => g x * (f x).toReal) μ :=
  by
  have : (fun x => g x * (f x).toReal) = fun x => (f x).toReal • g x := by simp [mul_comm]
  rw [this]
  exact integrable_withDensity_iff_integrable_smul' hf hflt

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