English
There exists a compact closure K provided the complement of K has small measure outside a given set.
Русский
Существует компактное замыкание K, такое что мера дополнения K мала вне заданного множества.
LaTeX
$$$\\exists K:\\ IsCompact(\\overline{K}) \\land μ(K^{c})<ε.$$$
Lean4
theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpace α] [SecondCountableTopology α]
[(uniformity α).IsCountablyGenerated] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] (ε : ℝ≥0∞)
(hε : 0 < ε) : ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε := by
/-
If α is empty, the result is trivial.
Otherwise, fix a dense sequence `seq` and an antitone basis `t` of entourages. We find a sequence
of natural numbers `u n`, such that `interUnionBalls seq u t`, which is the intersection over
`n` of the `t n`-neighborhood of `seq 1, ..., seq (u n)`, covers the space arbitrarily well.
-/
cases isEmpty_or_nonempty α
case inl =>
refine ⟨∅, by simp, ?_⟩
rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]
case inr =>
let seq := TopologicalSpace.denseSeq α
have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
obtain
⟨t : ℕ → Set (α × α), hto : ∀ i, t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ IsSymmetricRel (t i), h_basis :
(uniformity α).HasAntitoneBasis t⟩ :=
(@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (hto n).1
have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε :=
by
refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
· exact (measurable_prodMk_left (IsOpen.measurableSet (hto n).2.1)).compl.nullMeasurableSet
· rw [← compl_iUnion, h_univ, compl_univ]
choose! s' s'bound using h3
rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
classical
let u : ℕ → ℕ := fun n ↦ s' n (δ n)
refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
rw [interUnionBalls, Set.compl_iInter]
refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
have h'' n : Prod.swap ⁻¹' t n = t n := IsSymmetricRel.eq (hto n).2.2
simp only [h'', compl_iUnion, ge_iff_le]
exact (s'bound n (δ n) (hδ1 n)).le
