Additive Haar measures on real normed spaces

A continuous linear equivalence between finite-dimensional real normed spaces is nonsingular for any additive Haar measures chosen on its source and target: null sets correspond to null sets under it, whatever the normalizations. This is uniqueness of additive Haar measure, in the form MeasureTheory.Measure.absolutelyContinuous_isAddHaarMeasure, applied to the pushforward measure, which is again an additive Haar measure.

The real measure of a positive-radius ball is its radius raised to the dimension times the real measure of the unit ball, independently of its centre.

Main results

• ContinuousLinearEquiv.quasiMeasurePreserving_addHaar: a continuous linear equivalence is quasi measure preserving for additive Haar measures on its source and target.
• MeasureTheory.Measure.addHaar_real_ball_of_pos: the real measure of a positive-radius ball.

theorem ContinuousLinearEquiv.quasiMeasurePreserving_addHaar {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (e : E ≃L[ℝ] F) (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e) μ ν

A continuous linear equivalence is nonsingular for any additive Haar measures on its source and target.

theorem MeasureTheory.Measure.addHaar_real_ball_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (mu : Measure E) [mu.IsAddHaarMeasure] (x : E) {r : ℝ} (hr : 0 < r) : mu.real (Metric.ball x r) = r ^ Module.finrank ℝ E * mu.real (Metric.ball 0 1)

The real measure of a ball of positive radius is the corresponding power of the radius times the real measure of the unit ball.