English
The ν-measure of μ.sigmaFiniteSetWRT'(ν) equals the supremum of ν(s) over all measurable s with μ|s sigma-finite.
Русский
Мера ν (μ.sigmaFiniteSetWRT'(ν)) равна верхней границе ν(s) по всем измеримым s, для которых μ|s сигма-финитна.
LaTeX
$$$$\nu\left(\mu\sigmaFiniteSetWRT'(\nu)\right) = \bigvee_{s:\text{MeasurableSet},\ \SigmaFinite(\mu\restriction s)} \nu(s).$$$$
Lean4
/-- `μ.sigmaFiniteSetWRT' ν` has maximal `ν`-measure among all measurable sets `s` with sigma-finite
`μ.restrict s`. -/
theorem measure_sigmaFiniteSetWRT' (μ ν : Measure α) [IsFiniteMeasure ν] :
ν (μ.sigmaFiniteSetWRT' ν) = ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s :=
by
apply le_antisymm
· refine (le_iSup (f := fun _ ↦ _) (sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν)).trans ?_
exact
le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetWRT' ν)
measurableSet_sigmaFiniteSetWRT'
· exact le_of_tendsto' (tendsto_measure_sigmaFiniteSetGE μ ν) (fun _ ↦ measure_mono (Set.subset_iUnion _ _))
