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} [MeasurableSpace G] [MeasurableSpace H] [NontriviallyNormedField 𝕜] [TopologicalSpace G] [TopologicalSpace H] [AddCommGroup G] [AddCommGroup H] [TopologicalAddGroup G] [TopologicalAddGroup H] [Module 𝕜 G] [Module 𝕜 H] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [BorelSpace G] [BorelSpace H] [T2Space H] (e : G ≃L[𝕜] H) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (↑e) μ)

Equations

• @MeasureTheory.Measure.MapContinuousLinearEquiv.isAddHaarMeasure = @MeasureTheory.Measure.MapContinuousLinearEquiv.isAddHaarMeasure.proof_1

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] [TopologicalAddGroup G] [TopologicalAddGroup H] [Module 𝕜 G] [Module 𝕜 H] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [BorelSpace G] [BorelSpace H] [T2Space H] [CompleteSpace 𝕜] [T2Space G] [FiniteDimensional 𝕜 G] [ContinuousSMul 𝕜 G] [ContinuousSMul 𝕜 H] (e : G ≃ₗ[𝕜] H) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (↑e) μ)

Equations

• @MeasureTheory.Measure.MapLinearEquiv.isAddHaarMeasure = @MeasureTheory.Measure.MapLinearEquiv.isAddHaarMeasure.proof_1

theorem MeasureTheory.Measure.integral_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) (R : ℝ) : ∫ (x : E), f (R • x) ∂μ = |(R ^ FiniteDimensional.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] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) (R : ℝ) {hR : 0 ≤ R} : ∫ (x : E), f (R • x) ∂μ = (R ^ FiniteDimensional.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] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) (R : ℝ) : ∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ FiniteDimensional.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] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) {R : ℝ} (hR : 0 ≤ R) : ∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ FiniteDimensional.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_mul_left {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace 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] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] (f : E → F) {R : ℝ} (hR : R ≠ 0) : (MeasureTheory.Integrable fun x => f (R • x)) ↔ MeasureTheory.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] {μ : MeasureTheory.Measure E} [MeasureTheory.Measure.IsAddHaarMeasure μ] {f : E → F} (hf : MeasureTheory.Integrable f) {R : ℝ} (hR : R ≠ 0) : MeasureTheory.Integrable fun x => f (R • x)

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

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

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

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

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

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