Integration on Groups #
We develop properties of integrals with a group as domain. This file contains properties about integrability, Lebesgue integration and Bochner integration.
theorem
measure_theory.lintegral_mul_left_eq_self
{G : Type u_2}
[measurable_space G]
{μ : measure_theory.measure G}
[group G]
[has_measurable_mul G]
[μ.is_mul_left_invariant]
(f : G → ℝ≥0∞)
(g : G) :
Translating a function by left-multiplication does not change its lintegral with respect to
a left-invariant measure.
theorem
measure_theory.lintegral_add_left_eq_self
{G : Type u_2}
[measurable_space G]
{μ : measure_theory.measure G}
[add_group G]
[has_measurable_add G]
[μ.is_add_left_invariant]
(f : G → ℝ≥0∞)
(g : G) :
theorem
measure_theory.lintegral_add_right_eq_self
{G : Type u_2}
[measurable_space G]
{μ : measure_theory.measure G}
[add_group G]
[has_measurable_add G]
[μ.is_add_right_invariant]
(f : G → ℝ≥0∞)
(g : G) :
theorem
measure_theory.lintegral_mul_right_eq_self
{G : Type u_2}
[measurable_space G]
{μ : measure_theory.measure G}
[group G]
[has_measurable_mul G]
[μ.is_mul_right_invariant]
(f : G → ℝ≥0∞)
(g : G) :
Translating a function by right-multiplication does not change its lintegral with respect to
a right-invariant measure.
theorem
measure_theory.integral_add_left_eq_self
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[add_group G]
[has_measurable_add G]
[μ.is_add_left_invariant]
(f : G → E)
(g : G) :
theorem
measure_theory.integral_mul_left_eq_self
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[group G]
[has_measurable_mul G]
[μ.is_mul_left_invariant]
(f : G → E)
(g : G) :
Translating a function by left-multiplication does not change its integral with respect to a left-invariant measure.
theorem
measure_theory.integral_add_right_eq_self
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[add_group G]
[has_measurable_add G]
[μ.is_add_right_invariant]
(f : G → E)
(g : G) :
theorem
measure_theory.integral_mul_right_eq_self
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[group G]
[has_measurable_mul G]
[μ.is_mul_right_invariant]
(f : G → E)
(g : G) :
Translating a function by right-multiplication does not change its integral with respect to a right-invariant measure.
theorem
measure_theory.integral_zero_of_mul_left_eq_neg
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[group G]
[has_measurable_mul G]
[μ.is_mul_left_invariant]
{f : G → E}
{g : G}
(hf' : ∀ (x : G), f (g * x) = -f x) :
If some left-translate of a function negates it, then the integral of the function with respect to a left-invariant measure is 0.
theorem
measure_theory.integral_zero_of_add_left_eq_neg
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[add_group G]
[has_measurable_add G]
[μ.is_add_left_invariant]
{f : G → E}
{g : G}
(hf' : ∀ (x : G), f (g + x) = -f x) :
theorem
measure_theory.integral_zero_of_add_right_eq_neg
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[add_group G]
[has_measurable_add G]
[μ.is_add_right_invariant]
{f : G → E}
{g : G}
(hf' : ∀ (x : G), f (x + g) = -f x) :
theorem
measure_theory.integral_zero_of_mul_right_eq_neg
{G : Type u_2}
{E : Type u_3}
[measurable_space G]
{μ : measure_theory.measure G}
[normed_group E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[measurable_space E]
[borel_space E]
[group G]
[has_measurable_mul G]
[μ.is_mul_right_invariant]
{f : G → E}
{g : G}
(hf' : ∀ (x : G), f (x * g) = -f x) :
If some right-translate of a function negates it, then the integral of the function with respect to a right-invariant measure is 0.
theorem
measure_theory.lintegral_eq_zero_of_is_add_left_invariant
{G : Type u_2}
[measurable_space G]
{μ : measure_theory.measure G}
[topological_space G]
[add_group G]
[topological_add_group G]
[borel_space G]
[μ.is_add_left_invariant]
[μ.regular]
(hμ : μ ≠ 0)
{f : G → ℝ≥0∞}
(hf : continuous f) :
theorem
measure_theory.lintegral_eq_zero_of_is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
{μ : measure_theory.measure G}
[topological_space G]
[group G]
[topological_group G]
[borel_space G]
[μ.is_mul_left_invariant]
[μ.regular]
(hμ : μ ≠ 0)
{f : G → ℝ≥0∞}
(hf : continuous f) :
For nonzero regular left invariant measures, the integral of a continuous nonnegative function
f is 0 iff f is 0.