Basic properties of Haar measures on real vector spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
def
measure_theory.measure.map_continuous_linear_equiv.is_add_haar_measure
{𝕜 : Type u_1}
{G : Type u_2}
{H : Type u_3}
[measurable_space G]
[measurable_space H]
[nontrivially_normed_field 𝕜]
[topological_space G]
[topological_space H]
[add_comm_group G]
[add_comm_group H]
[topological_add_group G]
[topological_add_group H]
[module 𝕜 G]
[module 𝕜 H]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
[borel_space G]
[borel_space H]
[t2_space H]
(e : G ≃L[𝕜] H) :
@[protected, instance]
def
measure_theory.measure.map_linear_equiv.is_add_haar_measure
{𝕜 : Type u_1}
{G : Type u_2}
{H : Type u_3}
[measurable_space G]
[measurable_space H]
[nontrivially_normed_field 𝕜]
[topological_space G]
[topological_space H]
[add_comm_group G]
[add_comm_group H]
[topological_add_group G]
[topological_add_group H]
[module 𝕜 G]
[module 𝕜 H]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
[borel_space G]
[borel_space H]
[t2_space H]
[complete_space 𝕜]
[t2_space G]
[finite_dimensional 𝕜 G]
[has_continuous_smul 𝕜 G]
[has_continuous_smul 𝕜 H]
(e : G ≃ₗ[𝕜] H) :
theorem
measure_theory.measure.integral_comp_smul
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
(μ : measure_theory.measure E)
[μ.is_add_haar_measure]
{F : Type u_2}
[normed_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
(f : E → F)
(R : ℝ) :
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
measure_theory.measure.integral_comp_smul_of_nonneg
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
(μ : measure_theory.measure E)
[μ.is_add_haar_measure]
{F : Type u_2}
[normed_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
(f : E → F)
(R : ℝ)
{hR : 0 ≤ R} :
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
measure_theory.measure.integral_comp_inv_smul
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
(μ : measure_theory.measure E)
[μ.is_add_haar_measure]
{F : Type u_2}
[normed_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
(f : E → F)
(R : ℝ) :
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
measure_theory.measure.integral_comp_inv_smul_of_nonneg
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
(μ : measure_theory.measure E)
[μ.is_add_haar_measure]
{F : Type u_2}
[normed_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
(f : E → F)
{R : ℝ}
(hR : 0 ≤ R) :
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
measure_theory.integrable_comp_smul_iff
{F : Type u_1}
[normed_add_comm_group F]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
(μ : measure_theory.measure E)
[μ.is_add_haar_measure]
(f : E → F)
{R : ℝ}
(hR : R ≠ 0) :
measure_theory.integrable (λ (x : E), f (R • x)) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.comp_smul
{F : Type u_1}
[normed_add_comm_group F]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[finite_dimensional ℝ E]
{μ : measure_theory.measure E}
[μ.is_add_haar_measure]
{f : E → F}
(hf : measure_theory.integrable f μ)
{R : ℝ}
(hR : R ≠ 0) :
measure_theory.integrable (λ (x : E), f (R • x)) μ
theorem
measure_theory.integrable_comp_mul_left_iff
{F : Type u_1}
[normed_add_comm_group F]
(g : ℝ → F)
{R : ℝ}
(hR : R ≠ 0) :
theorem
measure_theory.integrable.comp_mul_left'
{F : Type u_1}
[normed_add_comm_group F]
{g : ℝ → F}
(hg : measure_theory.integrable g measure_theory.measure_space.volume)
{R : ℝ}
(hR : R ≠ 0) :
measure_theory.integrable (λ (x : ℝ), g (R * x)) measure_theory.measure_space.volume
theorem
measure_theory.integrable_comp_mul_right_iff
{F : Type u_1}
[normed_add_comm_group F]
(g : ℝ → F)
{R : ℝ}
(hR : R ≠ 0) :
theorem
measure_theory.integrable.comp_mul_right'
{F : Type u_1}
[normed_add_comm_group F]
{g : ℝ → F}
(hg : measure_theory.integrable g measure_theory.measure_space.volume)
{R : ℝ}
(hR : R ≠ 0) :
measure_theory.integrable (λ (x : ℝ), g (x * R)) measure_theory.measure_space.volume
theorem
measure_theory.integrable_comp_div_iff
{F : Type u_1}
[normed_add_comm_group F]
(g : ℝ → F)
{R : ℝ}
(hR : R ≠ 0) :
theorem
measure_theory.integrable.comp_div
{F : Type u_1}
[normed_add_comm_group F]
{g : ℝ → F}
(hg : measure_theory.integrable g measure_theory.measure_space.volume)
{R : ℝ}
(hR : R ≠ 0) :
measure_theory.integrable (λ (x : ℝ), g (x / R)) measure_theory.measure_space.volume