ennrealToMeasure — Mathlib

English

For μ a vector measure taking values in ENNReal, the equivalence holds between the Ennreal-to-measure criterion and absolute continuity: (∀ s, μ.ennrealToMeasure s = 0 → v s = 0) ↔ v ≪ᵥ μ.

Русский

Для μ, принимающей значения в ENNReal, эквивалентность между условием Ennreal-to-measure и абсолютной непрерывностью: (∀ s, μ.ennrealToMeasure s = 0 → v s = 0) ⇔ v ≪ᵥ μ.

LaTeX

$$({μ : VectorMeasure α ENNReal}) : (∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0) ↔ v ≪ᵥ μ$$

Lean4

theorem ennrealToMeasure {μ : VectorMeasure α ℝ≥0∞} : (∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0) ↔ v ≪ᵥ μ :=
  by
  constructor <;> intro h
  · refine mk fun s hmeas hs => h ?_
    rw [← hs, ennrealToMeasure_apply hmeas]
  · intro s hs
    by_cases hmeas : MeasurableSet s
    · rw [ennrealToMeasure_apply hmeas] at hs
      exact h hs
    · exact not_measurable v hmeas

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