Measurability of euclidean space

Stream: Is there code for X?

[Yaël Dillies]

We seem to be be missing measurable_space (euclidean_space . However, we have docs#measurable_space.pi (which should be called pi.measurable_space btw). Is it the correct instance and simply nobody yet took care of copying it to pi_Lp and euclidean_space?

[Heather Macbeth]

@Yaël Dillies It might be preferable to use Haar measure on Euclidean space. I don't think we've made a decision here. @Sebastien Gouezel proved the equivalence, docs#measure_theory.add_haar_measure_eq_volume_pi

However, if you want to use euclidean_space, I'm guessing you want to do geometry, and I believe that basic geometric facts, such as the rotation-invariance of the measure, are not obvious from either definition. You could reduce it to the fact (also missing) that a rotation (use docs#linear_isometry) of Euclidean space has determinant 1, using docs#measure_theory.measure.map_linear_map_add_haar_eq_smul_add_haar .

[David Wärn]

Isn't rotation-invariance of Haar measure easy? A rotation will simply scale Haar measure by some factor, since Haar measure is essentially unique, and since it preserves the unit ball this factor must be 1

[Heather Macbeth]

Maybe this works, indeed ... and it has the advantage of working on an arbitrary finite-dimensional inner product space, not just euclidean_space.

[Sebastien Gouezel]

Yes, from what we already have it is straightforward to show that isometries preserve Lebesgue measure (because they preserve Hausdorff measure by definition, and then any Haar measure is a multiple of Hausdorff measure).

[Sebastien Gouezel]

(And it works for any norm, not only the euclidean one).

[Heather Macbeth]

@Sebastien Gouezel We know that Haar measure is a multiple of $L^\infty$-Hausdorff measure, docs#measure_theory.hausdorff_measure_pi_real, but do we know that it is a multiple of $L^2$-Hausdorff measure?

[Heather Macbeth]

Or rather, I guess we know that $L^2$-Hausdorff measure is left-invariant, but we don't know the normalization factor.

[Yury G. Kudryashov]

Note that the original question was about measurable_space, not measure_space.

[Sebastien Gouezel]

For any norm, the Hausdorff measure is a Haar measure. Any other Haar measure is therefore proportional to it (with unknown constant). Since the Hausdorff measure is invariant under isometries, it follows that this the case for any other Haar measure.

[Heather Macbeth]

I see. But we don't have the normalizations, right? We don't know the volume of the unit hypercube with respect to $L^2$-Hausdorff measure (the result provided for $L^\infty$-Hausdorff measure by docs#measure_theory.hausdorff_measure_pi_real).

[Sebastien Gouezel]

Sure, we don't have the normalizations. But they are irrelevant for most of these questions, in fact!

[Yury G. Kudryashov]

Coming back to the measurable_space instance, I'm going to PR a generalization of docs#topological_space.second_countable_topology_fintype to the case of [encodable ι].

[Yury G. Kudryashov]

As well as docs#pi.borel_space

[Yury G. Kudryashov]

This means that with euclidean_space nat with instance coming from measurable_space.pi will be a borel_space.

[Heather Macbeth]

Will this work? docs#euclidean_space / docs#pi_Lp.inner_product_space require a fintype.

[Eric Wieser]

Just to note that a related discussion happened here