Basic properties of Haar measures on real vector spaces

instance MeasureTheory.Measure.MapLinearEquiv.isAddHaarMeasure {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} [MeasurableSpace G] [MeasurableSpace H] [NontriviallyNormedField 𝕜] [TopologicalSpace G] [TopologicalSpace H] [AddCommGroup G] [AddCommGroup H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H] [Module 𝕜 G] [Module 𝕜 H] (μ : Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [BorelSpace H] [CompleteSpace 𝕜] [T2Space G] [FiniteDimensional 𝕜 G] [ContinuousSMul 𝕜 G] [ContinuousSMul 𝕜 H] [T2Space H] (e : G ≃ₗ[𝕜] H) : (map (⇑e) μ).IsAddHaarMeasure

theorem MonoidHom.exists_nhds_isBounded {G : Type u_1} {H : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [LocallyCompactSpace G] [MeasurableSpace H] [SeminormedGroup H] [OpensMeasurableSpace H] (f : G →* H) (hf : Measurable ⇑f) (x : G) : ∃ s ∈ nhds x, Bornology.IsBounded (⇑f '' s)

theorem AddMonoidHom.exists_nhds_isBounded {G : Type u_1} {H : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [LocallyCompactSpace G] [MeasurableSpace H] [SeminormedAddGroup H] [OpensMeasurableSpace H] (f : G →+ H) (hf : Measurable ⇑f) (x : G) : ∃ s ∈ nhds x, Bornology.IsBounded (⇑f '' s)

theorem MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable {G : Type u_1} {H : Type u_2} [SeminormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] [SeminormedAddCommGroup H] [MeasurableSpace H] [OpensMeasurableSpace H] [NormedSpace ℝ H] (f : G →+ H) (hf : Measurable ⇑f) : Continuous ⇑f

A Borel-measurable group hom from a locally compact normed group to a real normed space is continuous.

theorem MeasureTheory.Measure.integral_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (R : ℝ) : ∫ (x : E), f (R • x) ∂μ = |(R ^ Module.finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ

The integral of f (R • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

theorem MeasureTheory.Measure.integral_comp_smul_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (R : ℝ) {hR : 0 ≤ R} : ∫ (x : E), f (R • x) ∂μ = (R ^ Module.finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ

The integral of f (R • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

theorem MeasureTheory.Measure.integral_comp_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (R : ℝ) : ∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ Module.finrank ℝ E| • ∫ (x : E), f x ∂μ

The integral of f (R⁻¹ • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

theorem MeasureTheory.Measure.integral_comp_inv_smul_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) {R : ℝ} (hR : 0 ≤ R) : ∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ Module.finrank ℝ E • ∫ (x : E), f x ∂μ

The integral of f (R⁻¹ • x) with respect to an additive Haar measure is a multiple of the integral of f. The formula we give works even when f is not integrable or R = 0 thanks to the convention that a non-integrable function has integral zero.

theorem MeasureTheory.Measure.setIntegral_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) {R : ℝ} (s : Set E) (hR : R ≠ 0) : ∫ (x : E) in s, f (R • x) ∂μ = |(R ^ Module.finrank ℝ E)⁻¹| • ∫ (x : E) in R • s, f x ∂μ

theorem MeasureTheory.Measure.setIntegral_comp_smul_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) {R : ℝ} (s : Set E) (hR : 0 < R) : ∫ (x : E) in s, f (R • x) ∂μ = (R ^ Module.finrank ℝ E)⁻¹ • ∫ (x : E) in R • s, f x ∂μ

theorem MeasureTheory.Measure.integral_comp_mul_left {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g : ℝ → F) (a : ℝ) : ∫ (x : ℝ), g (a * x) = |a⁻¹| • ∫ (y : ℝ), g y

theorem MeasureTheory.Measure.integral_comp_inv_mul_left {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g : ℝ → F) (a : ℝ) : ∫ (x : ℝ), g (a⁻¹ * x) = |a| • ∫ (y : ℝ), g y

theorem MeasureTheory.Measure.integral_comp_mul_right {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g : ℝ → F) (a : ℝ) : ∫ (x : ℝ), g (x * a) = |a⁻¹| • ∫ (y : ℝ), g y

theorem MeasureTheory.Measure.integral_comp_inv_mul_right {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g : ℝ → F) (a : ℝ) : ∫ (x : ℝ), g (x * a⁻¹) = |a| • ∫ (y : ℝ), g y

theorem MeasureTheory.Measure.integral_comp_div {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g : ℝ → F) (a : ℝ) : ∫ (x : ℝ), g (x / a) = |a| • ∫ (y : ℝ), g y

theorem MeasureTheory.integrable_comp_smul_iff {F : Type u_1} [NormedAddCommGroup F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (f : E → F) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : E) => f (R • x)) μ ↔ Integrable f μ

theorem MeasureTheory.Integrable.comp_smul {F : Type u_1} [NormedAddCommGroup F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : Measure E} [μ.IsAddHaarMeasure] {f : E → F} (hf : Integrable f μ) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : E) => f (R • x)) μ

theorem MeasureTheory.integrable_comp_mul_left_iff {F : Type u_1} [NormedAddCommGroup F] (g : ℝ → F) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : ℝ) => g (R * x)) volume ↔ Integrable g volume

theorem MeasureTheory.Integrable.comp_mul_left' {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} (hg : Integrable g volume) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : ℝ) => g (R * x)) volume

theorem MeasureTheory.integrable_comp_mul_right_iff {F : Type u_1} [NormedAddCommGroup F] (g : ℝ → F) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : ℝ) => g (x * R)) volume ↔ Integrable g volume

theorem MeasureTheory.Integrable.comp_mul_right' {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} (hg : Integrable g volume) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : ℝ) => g (x * R)) volume

theorem MeasureTheory.integrable_comp_div_iff {F : Type u_1} [NormedAddCommGroup F] (g : ℝ → F) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : ℝ) => g (x / R)) volume ↔ Integrable g volume

theorem MeasureTheory.Integrable.comp_div {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} (hg : Integrable g volume) {R : ℝ} (hR : R ≠ 0) : Integrable (fun (x : ℝ) => g (x / R)) volume

theorem MeasureTheory.integrable_comp {E' : Type u_2} {F' : Type u_3} {A : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F'] [BorelSpace F'] (f : E' ≃ₗᵢ[ℝ] F') [NormedAddCommGroup A] (g : F' → A) : Integrable (g ∘ ⇑f) volume ↔ Integrable g volume

theorem MeasureTheory.integral_comp {E' : Type u_2} {F' : Type u_3} {A : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F'] [BorelSpace F'] (f : E' ≃ₗᵢ[ℝ] F') [NormedAddCommGroup A] [NormedSpace ℝ A] (g : F' → A) : ∫ (x : E'), g (f x) = ∫ (y : F'), g y