exists_measurable_le_withDensity_eq

English

There exists a measurable density g such that μ.withDensity g = μ.withDensity f and g ≤ f (under SFinite μ).

Русский

Существует измеримая плотность g такая, что μ.withDensity g = μ.withDensity f и g ≤ f (при SFinite μ).

LaTeX

$$$\exists g\, (Measurable g) \land g \le f \land μ.withDensity g = μ.withDensity f$$$

Lean4

theorem exists_measurable_le_withDensity_eq [SFinite μ] (f : α → ℝ≥0∞) :
    ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f :=
  by
  obtain ⟨g, hgm, hgf, hint⟩ := exists_measurable_le_forall_setLIntegral_eq μ f
  use g, hgm, hgf
  ext s hs
  simp only [hint, withDensity_apply _ hs]

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