HepLean Documentation

Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Basic properties of Haar measures on real vector spaces #

source
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) [μ.IsAddHaarMeasure] [BorelSpace G] [BorelSpace H] [CompleteSpace 𝕜] [T2Space G] [FiniteDimensional 𝕜 G] [ContinuousSMul 𝕜 G] [ContinuousSMul 𝕜 H] [T2Space H] (e : G ≃ₗ[𝕜] H) :
(MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure
Equations
  • ⋯ = ⋯
source
theorem MeasureTheory.Measure.integral_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.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.

source
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) [μ.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.

source
theorem MeasureTheory.Measure.integral_comp_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.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.

source
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) [μ.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.

source
theorem MeasureTheory.Measure.setIntegral_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.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 ∂μ
source
@[deprecated MeasureTheory.Measure.setIntegral_comp_smul]
theorem MeasureTheory.Measure.set_integral_comp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.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 ∂μ

Alias of MeasureTheory.Measure.setIntegral_comp_smul.

source
theorem MeasureTheory.Measure.setIntegral_comp_smul_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.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 ∂μ
source
@[deprecated MeasureTheory.Measure.setIntegral_comp_smul_of_pos]
theorem MeasureTheory.Measure.set_integral_comp_smul_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.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 ∂μ

Alias of MeasureTheory.Measure.setIntegral_comp_smul_of_pos.

source
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
source
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
source
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
source
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
source
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
source
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) [μ.IsAddHaarMeasure] (f : E → F) {R : ℝ} (hR : R ≠ 0) :
MeasureTheory.Integrable (fun (x : E) => f (R • x)) μ ↔ MeasureTheory.Integrable f μ
source
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} [μ.IsAddHaarMeasure] {f : E → F} (hf : MeasureTheory.Integrable f μ) {R : ℝ} (hR : R ≠ 0) :
MeasureTheory.Integrable (fun (x : E) => f (R • x)) μ
source
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.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
source
theorem MeasureTheory.Integrable.comp_mul_left' {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} (hg : MeasureTheory.Integrable g MeasureTheory.volume) {R : ℝ} (hR : R ≠ 0) :
MeasureTheory.Integrable (fun (x : ℝ) => g (R * x)) MeasureTheory.volume
source
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.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
source
theorem MeasureTheory.Integrable.comp_mul_right' {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} (hg : MeasureTheory.Integrable g MeasureTheory.volume) {R : ℝ} (hR : R ≠ 0) :
MeasureTheory.Integrable (fun (x : ℝ) => g (x * R)) MeasureTheory.volume
source
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.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
source
theorem MeasureTheory.Integrable.comp_div {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} (hg : MeasureTheory.Integrable g MeasureTheory.volume) {R : ℝ} (hR : R ≠ 0) :
MeasureTheory.Integrable (fun (x : ℝ) => g (x / R)) MeasureTheory.volume
source
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) :
MeasureTheory.Integrable (g ∘ ⇑f) MeasureTheory.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
source
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