English
A measure can be constructed from a sigma-subadditive content on a semiring, and this measure is defined on the corresponding Carathéodory sigma-algebra.
Русский
Можно построить меру из сигма-субаддитивного содержимого на полуребре, и эта мера определена на соответствующей сигма-алгебре Карпатодороя.
LaTeX
$$$\\text{measureCaratheodory}(m,hC,m\\_sigma\\_subadd) : \\text{Measure}_{\\mathrm{caratheodory}(C)}(\\alpha).$$$
Lean4
/-- Construct a measure from a sigma-subadditive content on a semiring. This
measure is defined on the associated Carathéodory sigma-algebra. -/
noncomputable def measureCaratheodory (m : AddContent C) (hC : IsSetSemiring C)
(m_sigma_subadd : m.IsSigmaSubadditive) :
@Measure α (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).caratheodory :=
letI : MeasurableSpace α := (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).caratheodory
{
inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem
addContent_empty with
m_iUnion := fun f hf hd ↦ OuterMeasure.iUnion_eq_of_caratheodory _ hf hd
trim_le := by
apply le_inducedOuterMeasure.mpr fun s hs ↦ ?_
have hs_meas :
MeasurableSet[(inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).caratheodory] s :=
by
change (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s
exact isCaratheodory_inducedOuterMeasure_of_mem hC m hs
rw [OuterMeasure.trim_eq _ hs_meas, m.inducedOuterMeasure_eq hC m_sigma_subadd hs] }
