Hausdorff measure normalisation

Stream: mathlib4

[Oliver Nash]

I was recently wondering about our normalisation of Hausdorff measure. I believe it is such that the following is true:

import Mathlib.MeasureTheory.Group.Measure
import Mathlib.MeasureTheory.Measure.Hausdorff

open FiniteDimensional MeasureTheory Measure Metric

variable {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]

lemma hausdorffMeasure_ball_zero_one :
    μH[finrank ℝ E] (ball (0 : E) 1) = 2 ^ finrank ℝ E := by
  sorry

[Oliver Nash]

Furthermore, given this (or otherwise) it looks like the following should be easy:

instance isAddHaarMeasure_hausdorffMeasure [Nontrivial E] :
    IsAddHaarMeasure (G := E) μH[finrank ℝ E] :=
  sorry

[Oliver Nash]

I might add these results if I have time in the coming week but I thought I'd see if anyone had remarks to make before I embark. Maybe @Yury G. Kudryashov ?

[Yury G. Kudryashov]

I don't think that hausdorffMeasure_ball_zero_one is true.

[Yury G. Kudryashov]

I think that in an inner product space it is equal to volume.

[Yury G. Kudryashov]

IsAddHaarMeasure ... should be true.

[Yury G. Kudryashov]

We have MeasureTheory.instIsAddLeftInvariantHausdorffMeasureOfIsometricVAdd, so you only need to prove that it's positive on balls and is finite on compacts. Both easily follow from its properties on ι → Real and a linear equivalence with this space.

[Oliver Nash]

I'll have to look into the normalisation question when I have more time but in the meantime I added the easy (given what we have) bit: #16524

[Joseph Myers]

It would be good to have lemmas giving the normalisation not just for top-dimensional Hausdorff measure, but for m-dimensional Hausdorff measure in an n-dimensional affine space, applied to a set lying in an m-dimensional affine subspace thereof. (See the PutnamBench discussion of how to refer to the area of a triangle in 3-dimensional space, for example - to talk about 2-dimensional areas in higher-dimensional spaces we need to know how to correctly normalise 2-dimensional Hausdorff measure in a space of any dimension with the Euclidean metric.)

[Yury G. Kudryashov]

This can by done by some map/comap tricks.

[Joseph Myers]

OK, that's something we do already have the lemmas for (docs#Isometry.hausdorffMeasure_image etc.), unlike the normalisation where we only have a lemma giving equality to volume in the ι → ℝ (sup metric) case, not anything for the Euclidean metric.

[Yury G. Kudryashov]

Yury G. Kudryashov said:

I think that in an inner product space it is equal to volume.

No longer sure about that.

[Yury G. Kudryashov]

For the plane, the answer seems to be π/4 due to the isodiametric inequality.

[Yury G. Kudryashov]

@Joseph Myers I think that you should generalize MeasureSpace on InnerProductSpace to a NormedAddTorsor (if it isn't done yet), then you'll have measure on an affine subspace of a Euclidean space.

[Oliver Nash]

I think I should have time to add a proof of my original claim in the next day or so.

[Oliver Nash]

I had a look this morning and I think the non-trivial direction follows from docs#Besicovitch.exists_closedBall_covering_tsum_measure_le (though perhaps this is too much of a sledgehammer).

[Oliver Nash]

Really though, we should just use the volume for docs#EuclideanSpace and not the Hausdorff measure.

[Joseph Myers]

Yury G. Kudryashov said:

Joseph Myers I think that you should generalize MeasureSpace on InnerProductSpace to a NormedAddTorsor (if it isn't done yet), then you'll have measure on an affine subspace of a Euclidean space.

Any translation-invariant measure on an additive group gives one for an AddTorsor in the obvious way, but this probably needs to be a def and not an instance to avoid diamonds for the measure on the group, which can also be considered as a torsor for itself, as while the measures would be equal I expect they wouldn't be defeq. (Then I suppose you'd need a Prop typeclass asserting that the measure on a torsor is the one given by that on the underlying group, with associated instances both for the group as a torsor for itself and for the measure given by the above def.)

[Joseph Myers]

Oliver Nash said:

Really though, we should just use the volume for docs#EuclideanSpace and not the Hausdorff measure.

We need some standard way to talk about n-dimensional volume of a set in a space that might be of more than n dimensions, whether that's volume combined with moving to a subspace or whether that's Hausdorff measure (and then we need lemmas relating all the plausible ways of talking about this to whatever the main version we choose is). Even a statement as basic as "volume of an n-dimensional simplex = volume of base * height / n" involves measures of both n-dimensional and (n-1)-dimensional sets simultaneously (in a space that might be more than n-dimensional). (No doubt we do then also want a version of that specialized to triangles, where 1-dimensional volume of the base is replaced by distance between two points.)

[Yury G. Kudryashov]

Joseph Myers said:

Yury G. Kudryashov said:

Joseph Myers I think that you should generalize MeasureSpace on InnerProductSpace to a NormedAddTorsor (if it isn't done yet), then you'll have measure on an affine subspace of a Euclidean space.

Any translation-invariant measure on an additive group gives one for an AddTorsor in the obvious way, but this probably needs to be a def and not an instance to avoid diamonds for the measure on the group, which can also be considered as a torsor for itself, as while the measures would be equal I expect they wouldn't be defeq. (Then I suppose you'd need a Prop typeclass asserting that the measure on a torsor is the one given by that on the underlying group, with associated instances both for the group as a torsor for itself and for the measure given by the above def.)

If you replace the instance measureSpaceOfInnerProductSpace with a new instance that works for torsors, then you get no diamonds.

[Eric Wieser]

I think I argued in the past that that instance is probably not a good one in the long run, as it will surely lead to diamonds

[Yury G. Kudryashov]

How?

[Oliver Nash]

Joseph Myers said:

Oliver Nash said:

Really though, we should just use the volume for docs#EuclideanSpace and not the Hausdorff measure.

We need some standard way to talk about n-dimensional volume of a set in a space that might be of more than n dimensions, whether that's volume combined with moving to a subspace or whether that's Hausdorff measure [...]

Agreed of course. What I had in mind though is that Hausdorff measure is still not the right thing (not even up to an overall scale) if you just pass to a subset which is not an affine subspace.

For example if we take the 2-sphere inside Euclidean 3-space, then Mathlib gives it the subset metric rather than the geodesic metric. So the corresponding 2-dim Hausdorff measure (or equivalently the restriction of the 2-dim Hausdorff measure on Euclidean 3-space) will not be the right measure because the diameter of a ball will be off by the cosine of an angle.

So what's really missing is geodesic distance. The setting in which I understand this well is when you have an infinitesimal metric, i.e., a Riemannian manifold and then the tangent space is an inner product space so you might as well just use inner product space volume there and (assuming orientability) integrate this up to a measure. (Of course, this will actually agree with the Hausdorff measure, with the geodesic metric, up to scale.)

[Eric Wieser]

Yury G. Kudryashov said:

How?

Eric Wieser said:

I'm pretty sure that measure_space_of_inner_product_space is going to give us a diamond problem eventually, because it breaks the "don't construct data from data" rule; what's the measure on ulift complex? Is it just the measure on complex passed through equiv.ulift? Or is it the measure derived from inner passed through equiv.ulift? They're certainly not defeq, because everything goes through a classical.some.

[Sébastien Gouëzel]

Oliver Nash said:

For example if we take the 2-sphere inside Euclidean 3-space, then Mathlib gives it the subset metric rather than the geodesic metric. So the corresponding 2-dim Hausdorff measure (or equivalently the restriction of the 2-dim Hausdorff measure on Euclidean 3-space) will not be the right measure because the diameter of a ball will be off by the cosine of an angle.

I'm not sure I understand the issue here. When you zoom in enough, since you're talking of a submanifold, the geodesic distance and the subset distance become essentially the same (within a multiplicative factor of $1+\epsilon$). As Hausdorff measure is precisely defined by zooming in arbitrarily, doesn't it imply that the Hausdorff measure for the geodesic distance and the subset distance coincide?

Of course, this wouldn't be the case for arbitrary sets, but in fractal sets where the difference becomes relevant I don't think you can even talk of a geodesic distance.

[Oliver Nash]

Oh you're absolutely right. What I wrote is clearly ridiculous.

What I had in mind was that the area of a circle on the sphere will be off by a factor involving the cosine so how could things line up but of course radius^2 will be off by an exactly compensating factor, so indeed it is possible for there to be agreement up to an overall scale; and moreover there is! (In my defense I was writing this in my rapidly shortening moments over lunch --- indeed I'd better resume work now.)

[Oliver Nash]

OK I now agree that the HM is a very convenient shortcut around the missing differential geometry. (Indeed one wonders if Euclid made an error declaring the unit square to have area 1; and should instead have given the unit circle this honour.)

[Yury G. Kudryashov]

Thanks Eric, ULift is a good example. Should we make it a non-instance and add a typeclass saying that the volume (or even a measure?) is equal to the one given by the inner product? @Sébastien Gouëzel , what do you think?

[Eric Wieser]

The argument in the past (which I think is reasonable) was "we don't actually care about ULift, let's wait until we have a situation we do care about"

[Sébastien Gouëzel]

I think we care a lot about the standard measure on inner product spaces (for example when doing Fourier transform) and not so much about ULifting measures, so I'd rather keep the current instance. Of course, I'm ready to change my mind the day it creates real problems!

[Yury G. Kudryashov]

Then we should add this information to the docstring of the instance.

[Yury G. Kudryashov]

Opened #17270, feel free to push improvements there.