Theorems · Definition · measure theory

MeasureTheory.Measure.euclideanHausdorffMeasure

{X : Type u_1} → [inst : EMetricSpace X] → [inst_1 : MeasurableSpace X] → [BorelSpace X] → ℕ → MeasureTheory.Measure X

Euclidean Hausdorff measure μHE[d], defined as μH[d] scaled to agree with Lebesgue measure on a d-dimensional Euclidean space. While this is defined on any (e)metric space, it is intended to be used for affine space associated with an inner product space, where it agrees with the volume measure on the inner product space.

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

21 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpaceMeasurableSpaceBorelSpace