hausdorffMeasure

Mathlib.MeasureTheory.Measure.Hausdorff

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.hausdorffMeasure

English

Define the Hausdorff measure μH[d] on X by μH[d] s = mkMetric (diam^d) (s) in a suitable construction.

Русский

Определим Хаусдорфову меру μH[d] на X через mkMetric с дименом d.

LaTeX

$$$ μH[d] = mkMetric (\lambda r. r^{d}) $$$

Lean4

/-- Hausdorff measure on an (e)metric space. -/
def hausdorffMeasure (d : ℝ) : Measure X :=
  mkMetric fun r => r ^ d

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru