Bochner Integration on Groups #
We develop properties of integrals with a group as domain. This file contains properties about integrability and Bochner integration.
theorem
MeasureTheory.Integrable.comp_neg
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableNeg G]
[μ.IsNegInvariant]
{f : G → F}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (t : G) => f (-t)) μ
theorem
MeasureTheory.Integrable.comp_inv
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableInv G]
[μ.IsInvInvariant]
{f : G → F}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (t : G) => f t⁻¹) μ
theorem
MeasureTheory.integral_neg_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[AddGroup G]
[MeasurableNeg G]
(f : G → E)
(μ : MeasureTheory.Measure G)
[μ.IsNegInvariant]
:
theorem
MeasureTheory.integral_inv_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[Group G]
[MeasurableInv G]
(f : G → E)
(μ : MeasureTheory.Measure G)
[μ.IsInvInvariant]
:
theorem
MeasureTheory.integral_add_left_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
[μ.IsAddLeftInvariant]
(f : G → E)
(g : G)
:
Translating a function by left-addition does not change its integral with respect to a left-invariant measure.
theorem
MeasureTheory.integral_mul_left_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
[μ.IsMulLeftInvariant]
(f : G → E)
(g : G)
:
Translating a function by left-multiplication does not change its integral with respect to a left-invariant measure.
theorem
MeasureTheory.integral_add_right_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
[μ.IsAddRightInvariant]
(f : G → E)
(g : G)
:
Translating a function by right-addition does not change its integral with respect to a right-invariant measure.
theorem
MeasureTheory.integral_mul_right_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
[μ.IsMulRightInvariant]
(f : G → E)
(g : G)
:
Translating a function by right-multiplication does not change its integral with respect to a right-invariant measure.
theorem
MeasureTheory.integral_sub_right_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
[μ.IsAddRightInvariant]
(f : G → E)
(g : G)
:
theorem
MeasureTheory.integral_div_right_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
[μ.IsMulRightInvariant]
(f : G → E)
(g : G)
:
theorem
MeasureTheory.integral_eq_zero_of_add_left_eq_neg
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
{f : G → E}
{g : G}
[AddGroup G]
[MeasurableAdd G]
[μ.IsAddLeftInvariant]
(hf' : ∀ (x : G), f (g + x) = -f x)
:
∫ (x : G), f x ∂μ = 0
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
MeasureTheory.integral_eq_zero_of_mul_left_eq_neg
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
{f : G → E}
{g : G}
[Group G]
[MeasurableMul G]
[μ.IsMulLeftInvariant]
(hf' : ∀ (x : G), f (g * x) = -f x)
:
∫ (x : G), f x ∂μ = 0
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
MeasureTheory.integral_eq_zero_of_add_right_eq_neg
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
{f : G → E}
{g : G}
[AddGroup G]
[MeasurableAdd G]
[μ.IsAddRightInvariant]
(hf' : ∀ (x : G), f (x + g) = -f x)
:
∫ (x : G), f x ∂μ = 0
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
MeasureTheory.integral_eq_zero_of_mul_right_eq_neg
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{μ : MeasureTheory.Measure G}
{f : G → E}
{g : G}
[Group G]
[MeasurableMul G]
[μ.IsMulRightInvariant]
(hf' : ∀ (x : G), f (x * g) = -f x)
:
∫ (x : G), f x ∂μ = 0
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
MeasureTheory.Integrable.comp_add_left
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
{f : G → F}
[μ.IsAddLeftInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (g + t)) μ
theorem
MeasureTheory.Integrable.comp_mul_left
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
{f : G → F}
[μ.IsMulLeftInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (g * t)) μ
theorem
MeasureTheory.Integrable.comp_add_right
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
{f : G → F}
[μ.IsAddRightInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (t + g)) μ
theorem
MeasureTheory.Integrable.comp_mul_right
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
{f : G → F}
[μ.IsMulRightInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (t * g)) μ
theorem
MeasureTheory.Integrable.comp_sub_right
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
{f : G → F}
[μ.IsAddRightInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (t - g)) μ
theorem
MeasureTheory.Integrable.comp_div_right
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
{f : G → F}
[μ.IsMulRightInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (t / g)) μ
theorem
MeasureTheory.Integrable.comp_sub_left
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
[MeasurableNeg G]
{f : G → F}
[μ.IsNegInvariant]
[μ.IsAddLeftInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (g - t)) μ
theorem
MeasureTheory.Integrable.comp_div_left
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
[MeasurableInv G]
{f : G → F}
[μ.IsInvInvariant]
[μ.IsMulLeftInvariant]
(hf : MeasureTheory.Integrable f μ)
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (g / t)) μ
theorem
MeasureTheory.integrable_comp_sub_left
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[AddGroup G]
[MeasurableAdd G]
[MeasurableNeg G]
(f : G → F)
[μ.IsNegInvariant]
[μ.IsAddLeftInvariant]
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (g - t)) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integrable_comp_div_left
{G : Type u_4}
{F : Type u_6}
[MeasurableSpace G]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure G}
[Group G]
[MeasurableMul G]
[MeasurableInv G]
(f : G → F)
[μ.IsInvInvariant]
[μ.IsMulLeftInvariant]
(g : G)
:
MeasureTheory.Integrable (fun (t : G) => f (g / t)) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integral_sub_left_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[AddGroup G]
[MeasurableAdd G]
[MeasurableNeg G]
(f : G → E)
(μ : MeasureTheory.Measure G)
[μ.IsNegInvariant]
[μ.IsAddLeftInvariant]
(x' : G)
:
theorem
MeasureTheory.integral_div_left_eq_self
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[Group G]
[MeasurableMul G]
[MeasurableInv G]
(f : G → E)
(μ : MeasureTheory.Measure G)
[μ.IsInvInvariant]
[μ.IsMulLeftInvariant]
(x' : G)
:
theorem
MeasureTheory.integral_vadd_eq_self
{α : Type u_3}
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[AddGroup G]
[MeasurableSpace α]
[AddAction G α]
[MeasurableVAdd G α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
(f : α → E)
{g : G}
:
theorem
MeasureTheory.integral_smul_eq_self
{α : Type u_3}
{G : Type u_4}
{E : Type u_5}
[MeasurableSpace G]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[Group G]
[MeasurableSpace α]
[MulAction G α]
[MeasurableSMul G α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
(f : α → E)
{g : G}
: