integrable_withDensity_iff_integrable_smul'

English

If f is NNReal-measurable, then Integrable g with density μ.withDensity f is equivalent to Integrable (f.toReal • g) μ.

Русский

Если f измеримо в NNReal, то Integrable g с density μ.withDensity f эквивалентно Integrable (f.toReal • g) μ.

LaTeX

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

Lean4

theorem integrable_withDensity_iff_integrable_smul' {f : α → ℝ≥0∞} (hf : Measurable 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_smul]
  · simp_rw [NNReal.smul_def, ENNReal.toReal]
  · exact hf.ennreal_toNNReal

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