Dilation scaling of the lower Lebesgue integral

Dilating the variable of a function on a finite-dimensional real normed space E by a nonzero scalar r rescales its integral against an additive Haar measure by |(r ^ n)⁻¹|, where n is the dimension of E. Mathlib records this for the Bochner integral as MeasureTheory.Measure.integral_comp_smul; this file is the lower-Lebesgue-integral counterpart, proved the same way from MeasureTheory.Measure.map_addHaar_smul, and, like the Bochner version, needing no integrability hypothesis.

Main declarations

• TauCeti.lintegral_comp_smul: ∫⁻ x, g (r • x) ∂μ = |(r ^ n)⁻¹| * ∫⁻ x, g x ∂μ.
• TauCeti.lintegral_comp_inv_smul: the same law written for r⁻¹ and 0 < r.
• TauCeti.lintegral_comp_homothety: the same law for the homothety of ratio r about any centre.

theorem TauCeti.lintegral_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (g : E → ENNReal) {r : ℝ} (hr : r ≠ 0) : ∫⁻ (x : E), g (r • x) ∂μ = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| * ∫⁻ (x : E), g x ∂μ

Dilation scaling of the lower Lebesgue integral. This is the counterpart, for ∫⁻, of Mathlib's MeasureTheory.Measure.integral_comp_smul; as there, no integrability of g is needed.

theorem TauCeti.lintegral_comp_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (g : E → ENNReal) {r : ℝ} (hr : 0 < r) : ∫⁻ (x : E), g (r⁻¹ • x) ∂μ = ENNReal.ofReal (r ^ Module.finrank ℝ E) * ∫⁻ (x : E), g x ∂μ

Dilating the variable by r⁻¹, for 0 < r, multiplies a lower Lebesgue integral by r ^ n, where n is the dimension of the ambient space.

theorem TauCeti.lintegral_comp_homothety {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (g : E → ENNReal) (x : E) {r : ℝ} (hr : r ≠ 0) : ∫⁻ (y : E), g ((AffineMap.homothety x r) y) ∂μ = ENNReal.ofReal |(r ^ Module.finrank ℝ E)⁻¹| * ∫⁻ (y : E), g y ∂μ

Homothety scaling of the lower Lebesgue integral. Precomposing with the homothety of ratio r ≠ 0 about any centre x rescales a lower Lebesgue integral against an additive Haar measure by |(r ^ n)⁻¹|, where n is the dimension of the ambient space.