English
There exists a measurable set t such that μ|t is sigma-finite and ν(t) is large enough in relation to the supremum of ν over sigma-finite restrictions.
Русский
Существует измеримое множество t так, что μ|t сигма-конечно и ν(t) достигает достаточной величины по отношению к супремуму ν над сигма-конечными ограничениями.
LaTeX
$$$\exists t\; MeasurableSet(t) \wedge SigmaFinite(μ.restrict t) \wedge (⨆ s (MeasurableSet s) (SigmaFinite (μ.restrict s)), ν s) - 1/n ≤ ν t$$$
Lean4
/-- Let `C` be the supremum of `ν s` over all measurable sets `s` such that `μ.restrict s` is
sigma-finite. `C` is finite since `ν` is a finite measure. Then there exists a measurable set `t`
with `μ.restrict t` sigma-finite such that `ν t ≥ C - 1/n`. -/
theorem exists_isSigmaFiniteSet_measure_ge (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) :
∃ t,
MeasurableSet t ∧
SigmaFinite (μ.restrict t) ∧
(⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / n ≤ ν t :=
by
by_cases hC_lt : 1 / n < ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s
· have h_lt_top : ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s < ∞ :=
by
refine
(?_ : ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν Set.univ).trans_lt
(measure_lt_top _ _)
refine iSup_le (fun s ↦ ?_)
exact iSup_le (fun _ ↦ iSup_le (fun _ ↦ measure_mono (Set.subset_univ s)))
obtain ⟨t, ht⟩ :=
exists_lt_of_lt_ciSup
(ENNReal.sub_lt_self h_lt_top.ne (ne_zero_of_lt hC_lt) (by simp) :
(⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / n <
⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s)
have ht_meas : MeasurableSet t := by
by_contra h_notMem
simp only [h_notMem] at ht
simp at ht
have ht_mem : SigmaFinite (μ.restrict t) := by
by_contra h_notMem
simp only [h_notMem] at ht
simp at ht
refine ⟨t, ht_meas, ht_mem, ?_⟩
simp only [ht_meas, ht_mem, iSup_true] at ht
exact ht.le
· refine ⟨∅, MeasurableSet.empty, by rw [Measure.restrict_empty]; infer_instance, ?_⟩
rw [tsub_eq_zero_of_le (not_lt.mp hC_lt)]
exact zero_le'
