# Documentation

Mathlib.MeasureTheory.Measure.Haar.NormedSpace

# Basic properties of Haar measures on real vector spaces #

instance MeasureTheory.Measure.MapContinuousLinearEquiv.isAddHaarMeasure {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} [] [] [] [] [] [] [Module 𝕜 G] [Module 𝕜 H] (μ : ) [] [] [] (e : G ≃L[𝕜] H) :
instance MeasureTheory.Measure.MapLinearEquiv.isAddHaarMeasure {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} [] [] [] [] [] [] [Module 𝕜 G] [Module 𝕜 H] (μ : ) [] [] [] [] [] [] [] [] (e : G ≃ₗ[𝕜] H) :
theorem MeasureTheory.Measure.integral_comp_smul {E : Type u_1} [] [] [] [] (μ : ) {F : Type u_2} [] [] (f : EF) (R : ) :
∫ (x : E), f (R x)μ = |()⁻¹| ∫ (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} [] [] [] [] (μ : ) {F : Type u_2} [] [] (f : EF) (R : ) {hR : 0 R} :
∫ (x : E), f (R x)μ = ()⁻¹ ∫ (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} [] [] [] [] (μ : ) {F : Type u_2} [] [] (f : EF) (R : ) :
∫ (x : E), f (R⁻¹ x)μ = || ∫ (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} [] [] [] [] (μ : ) {F : Type u_2} [] [] (f : EF) {R : } (hR : 0 R) :
∫ (x : E), f (R⁻¹ x)μ = ∫ (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_mul_left {F : Type u_2} [] [] (g : F) (a : ) :
∫ (x : ), g (a * x) = |a⁻¹| ∫ (y : ), g y
theorem MeasureTheory.Measure.integral_comp_inv_mul_left {F : Type u_2} [] [] (g : F) (a : ) :
∫ (x : ), g (a⁻¹ * x) = |a| ∫ (y : ), g y
theorem MeasureTheory.Measure.integral_comp_mul_right {F : Type u_2} [] [] (g : F) (a : ) :
∫ (x : ), g (x * a) = |a⁻¹| ∫ (y : ), g y
theorem MeasureTheory.Measure.integral_comp_inv_mul_right {F : Type u_2} [] [] (g : F) (a : ) :
∫ (x : ), g (x * a⁻¹) = |a| ∫ (y : ), g y
theorem MeasureTheory.Measure.integral_comp_div {F : Type u_2} [] [] (g : F) (a : ) :
∫ (x : ), g (x / a) = |a| ∫ (y : ), g y
theorem MeasureTheory.integrable_comp_smul_iff {F : Type u_1} {E : Type u_2} [] [] [] [] (μ : ) (f : EF) {R : } (hR : R 0) :
(MeasureTheory.Integrable fun x => f (R x))
theorem MeasureTheory.Integrable.comp_smul {F : Type u_1} {E : Type u_2} [] [] [] [] {μ : } {f : EF} (hf : ) {R : } (hR : R 0) :
MeasureTheory.Integrable fun x => f (R x)
theorem MeasureTheory.integrable_comp_mul_left_iff {F : Type u_1} (g : F) {R : } (hR : R 0) :
(MeasureTheory.Integrable fun x => g (R * x))
theorem MeasureTheory.Integrable.comp_mul_left' {F : Type u_1} {g : F} (hg : ) {R : } (hR : R 0) :
MeasureTheory.Integrable fun x => g (R * x)
theorem MeasureTheory.integrable_comp_mul_right_iff {F : Type u_1} (g : F) {R : } (hR : R 0) :
(MeasureTheory.Integrable fun x => g (x * R))
theorem MeasureTheory.Integrable.comp_mul_right' {F : Type u_1} {g : F} (hg : ) {R : } (hR : R 0) :
MeasureTheory.Integrable fun x => g (x * R)
theorem MeasureTheory.integrable_comp_div_iff {F : Type u_1} (g : F) {R : } (hR : R 0) :
(MeasureTheory.Integrable fun x => g (x / R))
theorem MeasureTheory.Integrable.comp_div {F : Type u_1} {g : F} (hg : ) {R : } (hR : R 0) :
MeasureTheory.Integrable fun x => g (x / R)