Additive Haar measures on Euclidean space and Lebesgue measure on ι → ℝ

Every additive Haar measure μ on EuclideanSpace ℝ ι is a positive finite multiple a • volume of the volume measure, and ofLp carries the volume measure to Lebesgue measure on ι → ℝ. So ofLp carries μ to a • volume, and μ gives the preimage under ofLp of a set S ⊆ ι → ℝ the measure a * volume S. In particular a cube, the preimage of a sup-norm closed ball, can be compared with the concentric Euclidean ball: the cube of half-side r has measure at most √nⁿ times that of the Euclidean ball of radius r, since that ball contains the cube of half-side r / √n.

Main results

• EuclideanSpace.exists_map_toLp_symm_eq_smul: an additive Haar measure is carried by ofLp to a positive finite multiple of Lebesgue measure.
• EuclideanSpace.measure_preimage_ofLp: the measure of a preimage under ofLp.
• EuclideanSpace.measure_preimage_ofLp_closedBall, EuclideanSpace.measure_preimage_ofLp_ball: the measure of a cube.
• EuclideanSpace.measure_preimage_ofLp_closedBall_le: a cube has measure at most √nⁿ times that of the Euclidean ball of the same radius.
• EuclideanSpace.measurePreserving_consEquivL: splitting off the first coordinate identifies the volume of ℝⁿ⁺¹ with the product of the volumes of ℝ and ℝⁿ.

theorem EuclideanSpace.exists_map_toLp_symm_eq_smul {ι : Type u_1} [Fintype ι] (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [μ.IsAddHaarMeasure] : ∃ (a : ENNReal), a ≠ 0 ∧ a ≠ ⊤ ∧ MeasureTheory.Measure.map (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) μ = a • MeasureTheory.volume

An additive Haar measure on EuclideanSpace ℝ ι is carried by ofLp to a positive finite multiple of Lebesgue measure on ι → ℝ.

theorem EuclideanSpace.measure_preimage_ofLp {ι : Type u_1} [Fintype ι] {μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) μ = a • MeasureTheory.volume) (S : Set (ι → ℝ)) : μ (WithLp.ofLp ⁻¹' S) = a * MeasureTheory.volume S

If ofLp carries μ to a • volume, then μ gives the preimage of S the measure a * volume S.

theorem EuclideanSpace.measure_preimage_ofLp_closedBall {ι : Type u_1} [Fintype ι] {μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) μ = a • MeasureTheory.volume) (y : ι → ℝ) {r : ℝ} (hr : 0 ≤ r) : μ (WithLp.ofLp ⁻¹' Metric.closedBall y r) = a * ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

If ofLp carries μ to a • volume, then μ gives the cube of half-side r ≥ 0 the measure a (2r)ⁿ.

theorem EuclideanSpace.measure_preimage_ofLp_ball {ι : Type u_1} [Fintype ι] {μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) μ = a • MeasureTheory.volume) (y : ι → ℝ) {r : ℝ} (hr : 0 < r) : μ (WithLp.ofLp ⁻¹' Metric.ball y r) = a * ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

If ofLp carries μ to a • volume, then μ gives the open cube of half-side r > 0 the measure a (2r)ⁿ.

theorem EuclideanSpace.measure_preimage_ofLp_closedBall_le {ι : Type u_1} [Fintype ι] [Nonempty ι] (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [μ.IsAddHaarMeasure] (x : EuclideanSpace ℝ ι) (r : ℝ) : μ (WithLp.ofLp ⁻¹' Metric.closedBall x.ofLp r) ≤ ENNReal.ofReal (√↑(Fintype.card ι) ^ Fintype.card ι) * μ (Metric.ball x r)

The Euclidean ball B(x, r) lies in the cube of half-side r centred at x, whose measure is at most √nⁿ times that of the ball.

theorem EuclideanSpace.measurePreserving_consEquivL (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(consEquivL ℝ n)) MeasureTheory.volume MeasureTheory.volume

Splitting off the first coordinate carries the product of Lebesgue measure on ℝ and the volume of ℝⁿ to the volume of ℝⁿ⁺¹.

theorem TauCeti.volume_preserving_euclideanSpace_proj {ι : Type u_1} [hι : Fintype ι] [Unique ι] (i : ι) : MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.proj i)) MeasureTheory.volume MeasureTheory.volume

Projection onto the unique coordinate of a Euclidean line preserves actual volume.

theorem TauCeti.measurableEmbedding_euclideanSpace_proj {ι : Type u_1} [Unique ι] (i : ι) : MeasurableEmbedding ⇑(EuclideanSpace.proj i)

The unique-coordinate projection is a measurable embedding, so normalized volume transport also applies to arbitrary restricted integrals.

theorem TauCeti.setIntegral_comp_euclideanSpace_proj_preimage {ι : Type u_1} [Fintype ι] [Unique ι] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (g : ℝ → G) (s : Set ℝ) (i : ι) : ∫ (z : EuclideanSpace ℝ ι) in ⇑(EuclideanSpace.proj i) ⁻¹' s, g (z.ofLp i) = ∫ (t : ℝ) in s, g t

Integrating a function of the unique coordinate of a Euclidean line over the preimage of s is integrating it over s.