RellichKondrachov.MeasureTheory.Measure.HausdorffVolume

Relate Hausdorff measure μH[finrank] and Lebesgue measure volume on finite-dimensional real normed vector spaces.

Mathlib provides the exact identification μH[n] = volume on ι → ℝ, and shows that μH[finrank ℝ E] is an additive Haar measure on any finite-dimensional real normed space E. Using uniqueness of Haar measures, we record the resulting proportionality μH[finrank] = c • volume on general E, which is the form needed for transferring L² and compactness statements across equivalent measures.

@[implicit_reducible]

def RellichKondrachov.instMeasurableSpaceHausdorffVolume {E : Type u_1} [NormedAddCommGroup E] : MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

• RellichKondrachov.instMeasurableSpaceHausdorffVolume = borel E

theorem RellichKondrachov.instBorelSpaceHausdorffVolume {E : Type u_1} [NormedAddCommGroup E] : BorelSpace E

theorem RellichKondrachov.hausdorffMeasure_eq_smul_volume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E) = ((MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.closedBall 0 1) / MeasureTheory.volume (Metric.closedBall 0 1)) • MeasureTheory.volume

μH[finrank] is a scalar multiple of volume on a finite-dimensional real normed space.

Inverting the proportionality

theorem RellichKondrachov.volume_eq_smul_hausdorffMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : MeasureTheory.volume = (MeasureTheory.volume (Metric.closedBall 0 1) / (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.closedBall 0 1)) • MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)

volume is a scalar multiple of μH[finrank] on a finite-dimensional real inner product space.