English
On measurable sets, the measure constructed by ofMeasurable agrees with the given function m.
Русский
Для измеримых множеств мера, полученная через ofMeasurable, совпадает с заданной функцией m.
LaTeX
$$$\operatorname{ofMeasurable}(m,m0,mU)(s) = m(s) \quad\text{для всех измеримых } s$$
Lean4
/-- Obtain a measure by giving a countably additive function that sends `∅` to `0`. -/
def ofMeasurable (m : ∀ s : Set α, MeasurableSet s → ℝ≥0∞) (m0 : m ∅ MeasurableSet.empty = 0)
(mU :
∀ ⦃f : ℕ → Set α⦄ (h : ∀ i, MeasurableSet (f i)),
Pairwise (Disjoint on f) → m (⋃ i, f i) (MeasurableSet.iUnion h) = ∑' i, m (f i) (h i)) :
Measure α :=
{ toOuterMeasure := inducedOuterMeasure m _ m0
m_iUnion := fun f hf hd =>
show inducedOuterMeasure m _ m0 (iUnion f) = ∑' i, inducedOuterMeasure m _ m0 (f i)
by
rw [inducedOuterMeasure_eq m0 mU (MeasurableSet.iUnion hf), mU hf hd]
congr; funext n; rw [inducedOuterMeasure_eq m0 mU]
trim_le := le_inducedOuterMeasure.2 fun s hs ↦ by rw [OuterMeasure.trim_eq _ hs, inducedOuterMeasure_eq m0 mU hs] }
