English
Under the stated covering assumptions, mkMetric m s ≤ liminf (∑' i, m (diam (t n i))) l.
Русский
При заданных предположениях покрытий, mkMetric m s ≤ liminf (∑' i, m (diam (t n i))) l.
LaTeX
$$$ mkMetric m s \le \liminf_{n} \sum_i m(\operatorname{diam}(t_n i)) $$$
Lean4
/-- To bound the Hausdorff measure (or, more generally, for a measure defined using
`MeasureTheory.Measure.mkMetric`) of a set, one may use coverings with maximum diameter tending to
`0`, indexed by any sequence of countable types. -/
theorem mkMetric_le_liminf_tsum {β : Type*} {ι : β → Type*} [∀ n, Countable (ι n)] (s : Set X) {l : Filter β}
(r : β → ℝ≥0∞) (hr : Tendsto r l (𝓝 0)) (t : ∀ n : β, ι n → Set X) (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n)
(hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i) (m : ℝ≥0∞ → ℝ≥0∞) : mkMetric m s ≤ liminf (fun n => ∑' i, m (diam (t n i))) l :=
by
haveI : ∀ n, Encodable (ι n) := fun n => Encodable.ofCountable _
simp only [mkMetric_apply]
refine iSup₂_le fun ε hε => ?_
refine le_of_forall_gt_imp_ge_of_dense fun c hc => ?_
rcases
((frequently_lt_of_liminf_lt (by isBoundedDefault) hc).and_eventually
((hr.eventually (gt_mem_nhds hε)).and (ht.and hst))).exists with
⟨n, hn, hrn, htn, hstn⟩
set u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b
refine iInf₂_le_of_le u (by rwa [iUnion_decode₂]) ?_
refine iInf_le_of_le (fun j => ?_) ?_
· rw [EMetric.diam_iUnion_mem_option]
exact iSup₂_le fun _ _ => (htn _).trans hrn.le
·
calc
(∑' j : ℕ, ⨆ _ : (u j).Nonempty, m (diam (u j))) = _ :=
tsum_iUnion_decode₂ (fun t : Set X => ⨆ _ : t.Nonempty, m (diam t)) (by simp) _
_ ≤ ∑' i : ι n, m (diam (t n i)) := (ENNReal.tsum_le_tsum fun b => iSup_le fun _ => le_rfl)
_ ≤ c := hn.le
