English
A formula for μH[d] s expresses μH[d] s as a supremum over r > 0 and refinements t with diam constraints.
Русский
Формула для μH[d](s) выражает μH[d](s) как супремум по r > 0 и разложениям t с ограничениями по диаметру.
LaTeX
$$$ μH[d] s = \sup_{r>0} \inf_{t} \cdots $$$
Lean4
/-- A formula for `MeasureTheory.Measure.mkMetric`. -/
theorem mkMetric_apply (m : ℝ≥0∞ → ℝ≥0∞) (s : Set X) :
mkMetric m s =
⨆ (r : ℝ≥0∞) (_ : 0 < r),
⨅ (t : ℕ → Set X) (_ : s ⊆ iUnion t) (_ : ∀ n, diam (t n) ≤ r), ∑' n, ⨆ _ : (t n).Nonempty, m (diam (t n)) :=
by
classical
-- We mostly unfold the definitions but we need to switch the order of `∑'` and `⨅`
simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric', OuterMeasure.iSup_apply,
OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
refine
surjective_id.iSup_congr id fun r =>
iSup_congr_Prop Iff.rfl fun _ => surjective_id.iInf_congr _ fun t => iInf_congr_Prop Iff.rfl fun ht => ?_
dsimp
by_cases htr : ∀ n, diam (t n) ≤ r
· rw [iInf_eq_if, if_pos htr]
congr 1 with n : 1
simp only [iInf_eq_if, htr n, if_true]
· rw [iInf_eq_if, if_neg htr]
push_neg at htr; rcases htr with ⟨n, hn⟩
refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
· exact hn.not_ge
rcases diam_pos_iff.1 ((zero_le r).trans_lt hn) with ⟨x, hx, -⟩
exact ⟨x, hx⟩
