Measure on affine space

Stream: Is there code for X?

[Weiyi Wang]

Let's say I want to state elementary results about area in the Euclidean plane (an affine space, or an AddTorsor), is the following the following the right way to transfer the measure from the vector space? Do we have / plan to have code like this?

import Mathlib

open MeasureTheory
variable {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [MeasurableSpace V]

instance : MeasurableSpace P := MeasurableSpace.comap (· -ᵥ Classical.arbitrary P) inferInstance

instance [MeasurableAdd V] : MeasurableConstVAdd V P := sorry

noncomputable
def MeasureTheory.Measure.onAddTorsor (μ : Measure V) : Measure P := comap (· -ᵥ Classical.arbitrary P) μ

instance (μ : Measure V) [Measure.IsAddLeftInvariant μ] : VAddInvariantMeasure V P (Measure.onAddTorsor μ) := sorry

[Aaron Liu]

Probably your want a different measurable space structure

[Eric Wieser]

Even if you do want the same one; you should instead have something like

class MeasurableTorsor
     (V P) [AddCommGroup V] [AddTorsor V P] [MeasurableSpace V] [MeasurableSpace P] : Prop where
  measurableSpaceEq (p : P) :
    inferInstance = MeasurableSpace.comap (· -ᵥ p) inferInstance

(it's not safe to copy the one on the module as an instance, because if you have P = V you're stuck in a loop)

[Aaron Liu]

one that's not just a copy of the one on the module

[Eric Wieser]

Aaron, do you have an example in mind where having compatible measure spaces is undesirable?

[Aaron Liu]

this reminds me of docs#IsModuleTopology

[Aaron Liu]

Aaron Liu said:

one that's not just a copy of the one on the module

after thinking about it, the only reasonable choice actually is to just copy the one on the addgroup, but only if we also know that the measure on the addgroup behaves well, otherwise there is no reasonable choice

[Eric Wieser]

Copying is not a reasonable choice (since in any concrete setting P may already have a measurablespace instance), but a class that says an ambient space is a copy might be

[Joseph Myers]

As well as a class to say that the measure on a torsor agrees with the (hopefully translation-invariant) measure on the underlying AddGroup (nothing about this should depend on the module structure, just the group), it would be reasonable to have a def to copy the measure (but not an instance that copies the measure, to avoid problems for the group as a torsor for itself, as discussed above).

[Joseph Myers]

But we've also previously discussed that Hausdorff measure might be a better way of talking about areas in a Euclidean context. It's derived from the metric, so doesn't involve any of these issues with instances. And it allows you to talk about areas when the ambient space is more than two-dimensional - which matters for such basic results as "volume of an $n$-simplex = volume of face * height / $n$", which involves both $n$-dimensional and $(n-1)$-dimensional volumes in the same statement and would otherwise require moving to a subspace in order to talk about the volume of a face of the simplex.

[Joseph Myers]

Using Hausdorff measure for this does however require first defining a version with appropriate normalization for Euclidean space (divide the existing $n$-dimensional version in mathlib by the measure it assigns a unit cuboid in $n$-dimensional Euclidean space), because the normalization of the current mathlib version only agrees with $n$-dimensional Lebesgue measure given the sup metric, not given the Euclidean metric.

[Weiyi Wang]

Would one define Hausdorff measure directly on the affine space? I was thinking that it would be defined on the vector space and you still need this transferring to have it on the affine space

[Joseph Myers]

$n$-dimensional Hausdorff measure is defined for any metric space. ($n$ doesn't need to be an integer.)

[Weiyi Wang]

Ah, right

[Weiyi Wang]

How far is mathlib is this area?

[Joseph Myers]

Explicitly determining the scale factor between mathlib's normalization of Hausdorff measure and the Euclidean one, as an expression involving the gamma function, would be a large project (you need the isodiametric inequality; the answer is something like $2^n$ divided by the Lebesgue measure of the Euclidean $n$-ball). But you don't need an explicit expression to define the Euclidean-normalized version - you just divide by the Hausdorff measure of the $n$-dimensional Euclidean cuboid, without calculating what that measure is (just showing it's finite and nonzero).

[Joseph Myers]

Mathlib has Hausdorff measure, and the fact that it's preserved by isometries, and the fact that it agrees with Lebesgue measure if you use the sup metric on the product space rather than the Euclidean one.

[Joseph Myers]

And it has bounds on how Hausdorff measure is transformed by LipschitzWith maps, which will give you bounds on how much it can change between the Euclidean and sup metrics (which is enough to show the unit cuboid gets finite nonzero measure, as needed for the scaling to result in a useful measure; no idea if that's the best way to go for that lemma or if there's something much simpler).

[Joseph Myers]

(OK, we don't seem to have LipschitzWith lemmas for ofLp and toLp, but those will be easy to prove if you need them.)

[Aaron Liu]

Joseph Myers said:

(which is enough to show the unit cuboid gets finite nonzero measure, as needed for the scaling to result in a useful measure; no idea if that's the best way to go for that lemma or if there's something much simpler)

Is it not enough that the cuboid is compact with nonempty interior? To show that its measure is finite nonzero.

[Joseph Myers]

Do we have a suitable lemma saying that $n$-dimensional Hausdorff measure gives finite nonzero measure to a compact set with nonempty interior in $n$-dimensional space when using a metric that's not the sup metric?

[Aaron Liu]

oh the metric

[Aaron Liu]

uhhh

[Aaron Liu]

it's an equivalent norm

[Joseph Myers]

OK, that's the IsAddHaarMeasure measure instance, so yes.

[Aaron Liu]

oh that's great

[Aaron Liu]

the instance is a bit weird I think since you have a Module.finrank ℝ E in there

[Aaron Liu]

so it' won't apply to for example if you have a numeral in there

[Joseph Myers]

Fortunately, defining and using Euclidean-scaled Hausdorff measure should only require that instance to be used somewhere inside the proof of the lemma that the scale factor is finite and nonzero.

[Joseph Myers]

(And the proofs inside that instance are indeed using the fact that the maps between different norms are Lipschitz, we just don't need to do it specifically for the Euclidean case because that instance already exists.)

[Joseph Myers]

Once we have material about the measure of simplices in mathlib, we should move Heron's formula from the mathlib archive into mathlib (the version in the mathlib archive uses 1/2 * a * b * sin C as its definition of area, so first we'll need to show that that does indeed equal the area, defined appropriately using measures).

[Joseph Myers]

Incidental note: it will probably be convenient to have a (Euclidean) definition Affine.Simplex.volume that gives the $n$-dimensional volume of an $n$-dimensional simplex. That should be the measure of the closedInterior, not the interior, so that it gives the right result in the 0-dimensional case (and then we can show that it's equal to the measure of interior as well as that of closedInterior in positive dimensions). The 0-dimensional case matters as the base case for volume in terms of volume of a face.

[Weiyi Wang]

I looked at this because earlier I was looking for the lemma "for triangle, base * height = 2S is the same for 3 points" I soon realized I don't need the actual measure for this, but it still got me thinking the whole thing, and I also had a moment of thought "maybe we should have a definition of volume just as an invariant for all vertices"

[Joseph Myers]

It ought to be possible to get the sort of definitions Eric attempted in #14931 to work to prove such an invariant (in all dimensions) without involving measures - it's similar in spirit to the arguments used to prove that the excenter opposite a vertex of a simplex always exists (which are motivated by an argument in terms of volumes of faces and their projections, reconstructed purely in terms of algebra with heights without mentioning volume at all to avoid needing to involve measures). But it's also clear that any definition of volume ought to be linked to some kind of measure, whether by definition or by API lemma showing it's equal to something defined using measures, to justify that it corresponds to the right thing. And I think we do have enough about Hausdorff measure to use it in setting up such a definition.

[Ruben Van de Velde]

Looks like you've got a nice roadmap here, @Joseph Myers . Do you want to write it up in an issue so it doesn't get lost?

[Weiyi Wang]

I'd like to tackle this if a clear roadmap is written by an expert (or if not I'll create a not-so-great roadmap based on my own understanding...)

[Joseph Myers]

I've never actually used the measure theory part of mathlib, so I'm certainly not an expert here. The outline is:

• Define the scale factor to convert our form of Hausdorff measure to a Euclidean one: (μH[n] (WithLp.toLp 2 '' Set.Icc 0 1 : Set (EuclideanSpace ℝ (Fin n))))⁻¹ (I think).
• Show this is finite and nonzero, using the IsAddHaarMeasure instance to get that from being compact with nonempty interior (or a different argument in the 0-dimensional case when "nonempty interior" isn't true).
• Define Euclidean-scaled Hausdorff measure as our existing Hausdorff measure scaled by this value (this definition works in any metric space, it's just not expected to be interesting except for affine spaces for real inner product spaces). Give it notation, say μHE[n]. Selectively transfer across lemmas we have about Hausdorff measure if it's sufficiently useful to have them available for the new definition without rewriting by the definition.
• In the case of top-dimensional measure in a finite-dimensional real inner product space, show that μHE[n] agrees with volume. (Once you have this, the fact that Hausdorff measure transfers across isometries should allow applying results about volume, where useful, to μHE[n] in any affine space for a real inner product space, including for non-top-dimensional measure.)
• Define Affine.Simplex.volume to be the μHE[n] of the closedInterior. Show this equals volume of base * height / n (not sure if there are existing lemmas to use for this or if you need to do an integral).
• Show that Affine.Simplex.volume also equals the μHE[n] of the interior except in 0 dimensions.
• Use volume of base * height / n to deduce the special case for triangles where "volume of base" is replaced by a distance between two vertices.
• Show also that area of a triangle = a * b * sin C / 2.
• Move Heron's formula from the mathlib archive to mathlib, now expressed in terms of Affine.Simplex.volume.

[Eric Wieser]

Joseph Myers said:

Explicitly determining the scale factor between mathlib's normalization of Hausdorff measure and the Euclidean one, as an expression involving the gamma function, would be a large project (you need the isodiametric inequality; the answer is something like $2^n$ divided by the Lebesgue measure of the Euclidean $n$-ball). But you don't need an explicit expression to define the Euclidean-normalized version - you just divide by the Hausdorff measure of the $n$-dimensional Euclidean cuboid, without calculating what that measure is (just showing it's finite and nonzero).

Could you perhaps make a tracking issue explaining why this is so hard?

[Eric Wieser]

It seems like things would be easier in the long term if we got this out of the way, and so I think we should only detour around it if we're sure it's a nightmare

[Joseph Myers]

I don't know enough about how to prove the isodiametric inequality to give any useful explanation of the difficulties or roadmap for formalization. #maths > Sofa problem may have been solved @ 💬 says it should be done with Brunn-Minkowski which seems to be one of those things with multiple past attempts but no sign of any of them being contributed to mathlib.

An explicit scale factor using the gamma function plus proof it's correct would probably increase the number of (private) imports needed, but that's probably not very significant here.

(We already have the (Lebesgue) volume of a ball in terms of the gamma function.)

[Weiyi Wang]

My prior knowledge of Hausdorff measure was only "it can measure objects of any dimensions" so I just started reading related materials seriously for the first time. Please excuse me if I ask trivial questions.

I started by comparing the definition in mathlib and the one in wikipedia. They seem to agree to each other. However, while mathlib claims it equals to Lebesgue measure, wikipedia claims it needs a scaling factor even for this simple case. Is wikipedia wrong or I am reading it wrong?

[Weiyi Wang]

Oh! it is because ι → ℝ isn't the Euclidean space

[Weiyi Wang]

Since we don't explicitly calculate the factor, how about this definition (the name is temporary)

instance (n : ℕ) : (μH[n] : Measure (EuclideanSpace ℝ (Fin n))).IsAddHaarMeasure = ...
def μHE {X : Type*} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (n : ℕ) : Measure X :=
  addHaarScalarFactor (volume : Measure (EuclideanSpace ℝ (Fin n))) μH[n] • μH[n]

With this I got the following in 40 lines

theorem μHE_eq_volume {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] :
    (μHE (Module.finrank ℝ V) : Measure V) = volume

[Weiyi Wang]

I think I have derived basic properties and I am at base * height / n now. I couldn't find any directly applicable lemma about simplex in vector space, so I think I need to do the integral now... As part of "Is there code for X", please let me know if there are helpful lemma here

[Weiyi Wang]

I have got it through more than half way to the volume formula and the remaining are just some tedious work that I am pretty sure will work out. But I also realized my first attempt has left a stream of lemma too specialized for simplex volume, so I'll need to do redo it before PR the whole thing.

I have opened #34697 for reviewing the basic definition. I'd like to make sure we all agree on the definition

[Joseph Myers]

I hope someone familiar with the measure theory parts of mathlib can review this.

[Weiyi Wang]

While waiting for review, I am looking further into volume measure on curves (e.g. surface area of a sphere). Here is a familiar-looking formula given in Evans, Lawrence C.; Gariepy, Ronald F. (2015), Measure Theory and Fine Properties of Functions (Revised Edition):

Theorem 3.8 (Area formula). Let f : $\mathbb{R}^n \to \mathbb{R}^m$ be Lipschitz continuous, $n \le m$. There for each $\mathcal{L}^n$-measurable subset $A \subset \mathbb{R}^n$
$\int_A Jf dx = \int_{\mathbb{R}^m} \mathcal{H}^0(A \cap f^{-1}\{y\}) d\mathcal{H}^{n}(y)$

where $\mathcal{H}$ is μHE. $Jf$ is the Jacobian, but as the derivative of $f$ is not a square matrix, this is defined via polar decomposition $Df = O \circ S$ and $Jf = |det S|$, where $O$ is an orthogonal $\mathbb{R}^n \to \mathbb{R}^m$, and $S$ is a symmetric $\mathbb{R}^n \to \mathbb{R}^n$

How many of the relevant definitions are in Mathlib? And for those that is not in Mathlib yet, is it the best way to define them as written here?