Measures on Groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We develop some properties of measures on (topological) groups
- We define properties on measures: measures that are left or right invariant w.r.t. multiplication.
- We define the measure
μ.inv : A ↦ μ(A⁻¹)and show that it is right invariant iffμis left invariant. - We define a class
is_haar_measure μ, requiring that the measureμis left-invariant, finite on compact sets, and positive on open sets.
We also give analogues of all these notions in the additive world.
@[class]
structure
measure_theory.measure.is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[has_add G]
(μ : measure_theory.measure G) :
Prop
- map_add_left_eq_self : ∀ (g : G), measure_theory.measure.map (has_add.add g) μ = μ
A measure μ on a measurable additive group is left invariant
if the measure of left translations of a set are equal to the measure of the set itself.
Instances of this typeclass
- measure_theory.measure.is_add_haar_measure.to_is_add_left_invariant
- measure_theory.is_add_left_invariant_smul
- measure_theory.is_add_left_invariant_smul_nnreal
- measure_theory.measure.prod.measure.is_add_left_invariant
- measure_theory.measure.neg.is_add_left_invariant
- measure_theory.measure.pi.is_add_left_invariant
- measure_theory.pi.is_add_left_invariant_volume
- measure_theory.measure.is_add_left_invariant_add_haar_measure
- measure_theory.measure.alternating_map.measure.is_add_left_invariant
- measure_theory.measure.hausdorff_measure.measure.is_add_left_invariant
@[class]
structure
measure_theory.measure.is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[has_mul G]
(μ : measure_theory.measure G) :
Prop
- map_mul_left_eq_self : ∀ (g : G), measure_theory.measure.map (has_mul.mul g) μ = μ
A measure μ on a measurable group is left invariant
if the measure of left translations of a set are equal to the measure of the set itself.
Instances of this typeclass
- measure_theory.measure.is_haar_measure.to_is_mul_left_invariant
- measure_theory.is_mul_left_invariant_smul
- measure_theory.is_mul_left_invariant_smul_nnreal
- measure_theory.measure.prod.measure.is_mul_left_invariant
- measure_theory.measure.inv.is_mul_left_invariant
- measure_theory.measure.pi.is_mul_left_invariant
- measure_theory.pi.is_mul_left_invariant_volume
- measure_theory.measure.is_mul_left_invariant_haar_measure
- measure_theory.measure.hausdorff_measure.measure.is_mul_left_invariant
@[class]
structure
measure_theory.measure.is_add_right_invariant
{G : Type u_2}
[measurable_space G]
[has_add G]
(μ : measure_theory.measure G) :
Prop
- map_add_right_eq_self : ∀ (g : G), measure_theory.measure.map (λ (_x : G), _x + g) μ = μ
A measure μ on a measurable additive group is right invariant
if the measure of right translations of a set are equal to the measure of the set itself.
Instances of this typeclass
- is_add_left_invariant.is_add_right_invariant
- measure_theory.is_add_right_invariant_smul
- measure_theory.is_add_right_invariant_smul_nnreal
- measure_theory.measure.prod.measure.is_add_right_invariant
- measure_theory.measure.neg.is_add_right_invariant
- measure_theory.measure.pi.is_add_right_invariant
- measure_theory.measure.hausdorff_measure.measure.is_add_right_invariant
@[class]
structure
measure_theory.measure.is_mul_right_invariant
{G : Type u_2}
[measurable_space G]
[has_mul G]
(μ : measure_theory.measure G) :
Prop
- map_mul_right_eq_self : ∀ (g : G), measure_theory.measure.map (λ (_x : G), _x * g) μ = μ
A measure μ on a measurable group is right invariant
if the measure of right translations of a set are equal to the measure of the set itself.
Instances of this typeclass
- measure_theory.is_mul_left_invariant.is_mul_right_invariant
- measure_theory.is_mul_right_invariant_smul
- measure_theory.is_mul_right_invariant_smul_nnreal
- measure_theory.measure.prod.measure.is_mul_right_invariant
- measure_theory.measure.inv.is_mul_right_invariant
- measure_theory.measure.pi.is_mul_right_invariant
- measure_theory.measure.hausdorff_measure.measure.is_mul_right_invariant
theorem
measure_theory.map_mul_left_eq_self
{G : Type u_2}
[measurable_space G]
[has_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
(g : G) :
measure_theory.measure.map (has_mul.mul g) μ = μ
theorem
measure_theory.map_add_left_eq_self
{G : Type u_2}
[measurable_space G]
[has_add G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(g : G) :
measure_theory.measure.map (has_add.add g) μ = μ
theorem
measure_theory.map_add_right_eq_self
{G : Type u_2}
[measurable_space G]
[has_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(g : G) :
measure_theory.measure.map (λ (_x : G), _x + g) μ = μ
theorem
measure_theory.map_mul_right_eq_self
{G : Type u_2}
[measurable_space G]
[has_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G) :
measure_theory.measure.map (λ (_x : G), _x * g) μ = μ
@[protected, instance]
def
measure_theory.is_mul_left_invariant_smul
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[μ.is_mul_left_invariant]
(c : ennreal) :
(c • μ).is_mul_left_invariant
@[protected, instance]
def
measure_theory.is_add_left_invariant_smul
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant]
(c : ennreal) :
(c • μ).is_add_left_invariant
@[protected, instance]
def
measure_theory.is_mul_right_invariant_smul
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[μ.is_mul_right_invariant]
(c : ennreal) :
(c • μ).is_mul_right_invariant
@[protected, instance]
def
measure_theory.is_add_right_invariant_smul
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[μ.is_add_right_invariant]
(c : ennreal) :
(c • μ).is_add_right_invariant
@[protected, instance]
def
measure_theory.is_mul_left_invariant_smul_nnreal
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[μ.is_mul_left_invariant]
(c : nnreal) :
(c • μ).is_mul_left_invariant
@[protected, instance]
def
measure_theory.is_add_left_invariant_smul_nnreal
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant]
(c : nnreal) :
(c • μ).is_add_left_invariant
@[protected, instance]
def
measure_theory.is_add_right_invariant_smul_nnreal
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[μ.is_add_right_invariant]
(c : nnreal) :
(c • μ).is_add_right_invariant
@[protected, instance]
def
measure_theory.is_mul_right_invariant_smul_nnreal
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[μ.is_mul_right_invariant]
(c : nnreal) :
(c • μ).is_mul_right_invariant
theorem
measure_theory.measure_preserving_add_left
{G : Type u_2}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(g : G) :
theorem
measure_theory.measure_preserving_mul_left
{G : Type u_2}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
(g : G) :
theorem
measure_theory.measure_preserving.mul_left
{G : Type u_2}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
(g : G)
{X : Type u_1}
[measurable_space X]
{μ' : measure_theory.measure X}
{f : X → G}
(hf : measure_theory.measure_preserving f μ' μ) :
measure_theory.measure_preserving (λ (x : X), g * f x) μ' μ
theorem
measure_theory.measure_preserving.add_left
{G : Type u_2}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(g : G)
{X : Type u_1}
[measurable_space X]
{μ' : measure_theory.measure X}
{f : X → G}
(hf : measure_theory.measure_preserving f μ' μ) :
measure_theory.measure_preserving (λ (x : X), g + f x) μ' μ
theorem
measure_theory.measure_preserving_mul_right
{G : Type u_2}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G) :
measure_theory.measure_preserving (λ (_x : G), _x * g) μ μ
theorem
measure_theory.measure_preserving_add_right
{G : Type u_2}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(g : G) :
measure_theory.measure_preserving (λ (_x : G), _x + g) μ μ
theorem
measure_theory.measure_preserving.add_right
{G : Type u_2}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(g : G)
{X : Type u_1}
[measurable_space X]
{μ' : measure_theory.measure X}
{f : X → G}
(hf : measure_theory.measure_preserving f μ' μ) :
measure_theory.measure_preserving (λ (x : X), f x + g) μ' μ
theorem
measure_theory.measure_preserving.mul_right
{G : Type u_2}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G)
{X : Type u_1}
[measurable_space X]
{μ' : measure_theory.measure X}
{f : X → G}
(hf : measure_theory.measure_preserving f μ' μ) :
measure_theory.measure_preserving (λ (x : X), f x * g) μ' μ
@[protected, instance]
def
measure_theory.is_mul_left_invariant.smul_invariant_measure
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[has_measurable_mul G]
[μ.is_mul_left_invariant] :
@[protected, instance]
def
measure_theory.is_mul_left_invariant.vadd_invariant_measure
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[has_measurable_add G]
[μ.is_add_left_invariant] :
@[protected, instance]
def
measure_theory.is_mul_right_invariant.to_smul_invariant_measure_op
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[has_measurable_mul G]
[μ.is_mul_right_invariant] :
@[protected, instance]
def
measure_theory.is_mul_right_invariant.to_vadd_invariant_measure_op
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[has_measurable_add G]
[μ.is_add_right_invariant] :
@[protected, instance]
def
measure_theory.subgroup.vadd_invariant_measure
{G : Type u_1}
{α : Type u_2}
[add_group G]
[add_action G α]
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure G α μ]
(H : add_subgroup G) :
@[protected, instance]
def
measure_theory.subgroup.smul_invariant_measure
{G : Type u_1}
{α : Type u_2}
[group G]
[mul_action G α]
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure G α μ]
(H : subgroup G) :
theorem
measure_theory.forall_measure_preimage_add_iff
{G : Type u_2}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G) :
An alternative way to prove that μ is left invariant under addition.
theorem
measure_theory.forall_measure_preimage_mul_iff
{G : Type u_2}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G) :
An alternative way to prove that μ is left invariant under multiplication.
theorem
measure_theory.forall_measure_preimage_mul_right_iff
{G : Type u_2}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G) :
An alternative way to prove that μ is right invariant under multiplication.
theorem
measure_theory.forall_measure_preimage_add_right_iff
{G : Type u_2}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G) :
An alternative way to prove that μ is right invariant under addition.
@[protected, instance]
def
measure_theory.measure.prod.measure.is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[has_measurable_add G]
[μ.is_add_left_invariant]
[measure_theory.sigma_finite μ]
{H : Type u_1}
[has_add H]
{mH : measurable_space H}
{ν : measure_theory.measure H}
[has_measurable_add H]
[ν.is_add_left_invariant]
[measure_theory.sigma_finite ν] :
(μ.prod ν).is_add_left_invariant
@[protected, instance]
def
measure_theory.measure.prod.measure.is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[has_measurable_mul G]
[μ.is_mul_left_invariant]
[measure_theory.sigma_finite μ]
{H : Type u_1}
[has_mul H]
{mH : measurable_space H}
{ν : measure_theory.measure H}
[has_measurable_mul H]
[ν.is_mul_left_invariant]
[measure_theory.sigma_finite ν] :
(μ.prod ν).is_mul_left_invariant
@[protected, instance]
def
measure_theory.measure.prod.measure.is_add_right_invariant
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[has_measurable_add G]
[μ.is_add_right_invariant]
[measure_theory.sigma_finite μ]
{H : Type u_1}
[has_add H]
{mH : measurable_space H}
{ν : measure_theory.measure H}
[has_measurable_add H]
[ν.is_add_right_invariant]
[measure_theory.sigma_finite ν] :
(μ.prod ν).is_add_right_invariant
@[protected, instance]
def
measure_theory.measure.prod.measure.is_mul_right_invariant
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[has_measurable_mul G]
[μ.is_mul_right_invariant]
[measure_theory.sigma_finite μ]
{H : Type u_1}
[has_mul H]
{mH : measurable_space H}
{ν : measure_theory.measure H}
[has_measurable_mul H]
[ν.is_mul_right_invariant]
[measure_theory.sigma_finite ν] :
(μ.prod ν).is_mul_right_invariant
theorem
measure_theory.is_mul_left_invariant_map
{G : Type u_2}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[has_measurable_mul G]
{H : Type u_1}
[measurable_space H]
[has_mul H]
[has_measurable_mul H]
[μ.is_mul_left_invariant]
(f : G →ₙ* H)
(hf : measurable ⇑f)
(h_surj : function.surjective ⇑f) :
theorem
measure_theory.is_add_left_invariant_map
{G : Type u_2}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[has_measurable_add G]
{H : Type u_1}
[measurable_space H]
[has_add H]
[has_measurable_add H]
[μ.is_add_left_invariant]
(f : add_hom G H)
(hf : measurable ⇑f)
(h_surj : function.surjective ⇑f) :
theorem
measure_theory.map_sub_right_eq_self
{G : Type u_2}
[measurable_space G]
[sub_neg_monoid G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(g : G) :
measure_theory.measure.map (λ (_x : G), _x - g) μ = μ
theorem
measure_theory.map_div_right_eq_self
{G : Type u_2}
[measurable_space G]
[div_inv_monoid G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G) :
measure_theory.measure.map (λ (_x : G), _x / g) μ = μ
theorem
measure_theory.measure_preserving_div_right
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G) :
measure_theory.measure_preserving (λ (_x : G), _x / g) μ μ
theorem
measure_theory.measure_preserving_sub_right
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(g : G) :
measure_theory.measure_preserving (λ (_x : G), _x - g) μ μ
@[simp]
theorem
measure_theory.measure_preimage_add
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(g : G)
(A : set G) :
We shorten this from measure_preimage_add_left, since left invariant is the
preferred option for measures in this formalization.
@[simp]
theorem
measure_theory.measure_preimage_mul
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
(g : G)
(A : set G) :
We shorten this from measure_preimage_mul_left, since left invariant is the preferred option
for measures in this formalization.
@[simp]
theorem
measure_theory.measure_preimage_add_right
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(g : G)
(A : set G) :
@[simp]
theorem
measure_theory.measure_preimage_mul_right
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G)
(A : set G) :
theorem
measure_theory.map_mul_left_ae
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
(x : G) :
filter.map (λ (h : G), x * h) μ.ae = μ.ae
theorem
measure_theory.map_add_left_ae
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(x : G) :
filter.map (λ (h : G), x + h) μ.ae = μ.ae
theorem
measure_theory.map_mul_right_ae
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(x : G) :
filter.map (λ (h : G), h * x) μ.ae = μ.ae
theorem
measure_theory.map_add_right_ae
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(x : G) :
filter.map (λ (h : G), h + x) μ.ae = μ.ae
theorem
measure_theory.map_sub_right_ae
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(x : G) :
filter.map (λ (t : G), t - x) μ.ae = μ.ae
theorem
measure_theory.map_div_right_ae
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(x : G) :
filter.map (λ (t : G), t / x) μ.ae = μ.ae
theorem
measure_theory.eventually_mul_left_iff
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
(t : G)
{p : G → Prop} :
theorem
measure_theory.eventually_add_left_iff
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(t : G)
{p : G → Prop} :
theorem
measure_theory.eventually_mul_right_iff
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(t : G)
{p : G → Prop} :
theorem
measure_theory.eventually_add_right_iff
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(t : G)
{p : G → Prop} :
theorem
measure_theory.eventually_sub_right_iff
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_right_invariant]
(t : G)
{p : G → Prop} :
theorem
measure_theory.eventually_div_right_iff
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(t : G)
{p : G → Prop} :
@[protected]
noncomputable
def
measure_theory.measure.inv
{G : Type u_2}
[measurable_space G]
[has_inv G]
(μ : measure_theory.measure G) :
The measure A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.
Equations
@[protected]
noncomputable
def
measure_theory.measure.neg
{G : Type u_2}
[measurable_space G]
[has_neg G]
(μ : measure_theory.measure G) :
The measure A ↦ μ (- A), where - A is the pointwise negation of A.
Equations
@[class]
structure
measure_theory.measure.is_neg_invariant
{G : Type u_2}
[measurable_space G]
[has_neg G]
(μ : measure_theory.measure G) :
Prop
A measure is invariant under negation if - μ = μ. Equivalently, this means that for all
measurable A we have μ (- A) = μ A, where - A is the pointwise negation of A.
@[class]
structure
measure_theory.measure.is_inv_invariant
{G : Type u_2}
[measurable_space G]
[has_inv G]
(μ : measure_theory.measure G) :
Prop
A measure is invariant under inversion if μ⁻¹ = μ. Equivalently, this means that for all
measurable A we have μ (A⁻¹) = μ A, where A⁻¹ is the pointwise inverse of A.
@[simp]
theorem
measure_theory.measure.neg_eq_self
{G : Type u_2}
[measurable_space G]
[has_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant] :
@[simp]
theorem
measure_theory.measure.inv_eq_self
{G : Type u_2}
[measurable_space G]
[has_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant] :
@[simp]
theorem
measure_theory.measure.map_inv_eq_self
{G : Type u_2}
[measurable_space G]
[has_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant] :
@[simp]
theorem
measure_theory.measure.map_neg_eq_self
{G : Type u_2}
[measurable_space G]
[has_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant] :
theorem
measure_theory.measure.measure_preserving_inv
{G : Type u_2}
[measurable_space G]
[has_inv G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant] :
theorem
measure_theory.measure.measure_preserving_neg
{G : Type u_2}
[measurable_space G]
[has_neg G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant] :
@[simp]
theorem
measure_theory.measure.neg_apply
{G : Type u_2}
[measurable_space G]
[has_involutive_neg G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
(s : set G) :
@[simp]
theorem
measure_theory.measure.inv_apply
{G : Type u_2}
[measurable_space G]
[has_involutive_inv G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
(s : set G) :
@[protected, simp]
theorem
measure_theory.measure.inv_inv
{G : Type u_2}
[measurable_space G]
[has_involutive_inv G]
[has_measurable_inv G]
(μ : measure_theory.measure G) :
@[protected, simp]
theorem
measure_theory.measure.neg_neg
{G : Type u_2}
[measurable_space G]
[has_involutive_neg G]
[has_measurable_neg G]
(μ : measure_theory.measure G) :
@[simp]
theorem
measure_theory.measure.measure_inv
{G : Type u_2}
[measurable_space G]
[has_involutive_inv G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant]
(A : set G) :
@[simp]
theorem
measure_theory.measure.measure_neg
{G : Type u_2}
[measurable_space G]
[has_involutive_neg G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant]
(A : set G) :
theorem
measure_theory.measure.measure_preimage_neg
{G : Type u_2}
[measurable_space G]
[has_involutive_neg G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant]
(A : set G) :
⇑μ (has_neg.neg ⁻¹' A) = ⇑μ A
theorem
measure_theory.measure.measure_preimage_inv
{G : Type u_2}
[measurable_space G]
[has_involutive_inv G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant]
(A : set G) :
⇑μ (has_inv.inv ⁻¹' A) = ⇑μ A
@[protected, instance]
def
measure_theory.measure.inv.measure_theory.sigma_finite
{G : Type u_2}
[measurable_space G]
[has_involutive_inv G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[measure_theory.sigma_finite μ] :
@[protected, instance]
def
measure_theory.measure.neg.measure_theory.sigma_finite
{G : Type u_2}
[measurable_space G]
[has_involutive_neg G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[measure_theory.sigma_finite μ] :
@[protected, instance]
def
measure_theory.measure.inv.is_mul_right_invariant
{G : Type u_2}
[measurable_space G]
[division_monoid G]
[has_measurable_mul G]
[has_measurable_inv G]
{μ : measure_theory.measure G}
[μ.is_mul_left_invariant] :
@[protected, instance]
def
measure_theory.measure.neg.is_add_right_invariant
{G : Type u_2}
[measurable_space G]
[subtraction_monoid G]
[has_measurable_add G]
[has_measurable_neg G]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant] :
@[protected, instance]
def
measure_theory.measure.inv.is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[division_monoid G]
[has_measurable_mul G]
[has_measurable_inv G]
{μ : measure_theory.measure G}
[μ.is_mul_right_invariant] :
@[protected, instance]
def
measure_theory.measure.neg.is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[subtraction_monoid G]
[has_measurable_add G]
[has_measurable_neg G]
{μ : measure_theory.measure G}
[μ.is_add_right_invariant] :
theorem
measure_theory.measure.measure_preserving_sub_left
{G : Type u_2}
[measurable_space G]
[subtraction_monoid G]
[has_measurable_add G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant]
[μ.is_add_left_invariant]
(g : G) :
measure_theory.measure_preserving (λ (t : G), g - t) μ μ
theorem
measure_theory.measure.measure_preserving_div_left
{G : Type u_2}
[measurable_space G]
[division_monoid G]
[has_measurable_mul G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant]
[μ.is_mul_left_invariant]
(g : G) :
measure_theory.measure_preserving (λ (t : G), g / t) μ μ
theorem
measure_theory.measure.map_div_left_eq_self
{G : Type u_2}
[measurable_space G]
[division_monoid G]
[has_measurable_mul G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant]
[μ.is_mul_left_invariant]
(g : G) :
measure_theory.measure.map (λ (t : G), g / t) μ = μ
theorem
measure_theory.measure.map_sub_left_eq_self
{G : Type u_2}
[measurable_space G]
[subtraction_monoid G]
[has_measurable_add G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant]
[μ.is_add_left_invariant]
(g : G) :
measure_theory.measure.map (λ (t : G), g - t) μ = μ
theorem
measure_theory.measure.measure_preserving_mul_right_inv
{G : Type u_2}
[measurable_space G]
[division_monoid G]
[has_measurable_mul G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant]
[μ.is_mul_left_invariant]
(g : G) :
measure_theory.measure_preserving (λ (t : G), (g * t)⁻¹) μ μ
theorem
measure_theory.measure.measure_preserving_add_right_neg
{G : Type u_2}
[measurable_space G]
[subtraction_monoid G]
[has_measurable_add G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant]
[μ.is_add_left_invariant]
(g : G) :
measure_theory.measure_preserving (λ (t : G), -(g + t)) μ μ
theorem
measure_theory.measure.map_mul_right_inv_eq_self
{G : Type u_2}
[measurable_space G]
[division_monoid G]
[has_measurable_mul G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_inv_invariant]
[μ.is_mul_left_invariant]
(g : G) :
measure_theory.measure.map (λ (t : G), (g * t)⁻¹) μ = μ
theorem
measure_theory.measure.map_add_right_neg_eq_self
{G : Type u_2}
[measurable_space G]
[subtraction_monoid G]
[has_measurable_add G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_neg_invariant]
[μ.is_add_left_invariant]
(g : G) :
measure_theory.measure.map (λ (t : G), -(g + t)) μ = μ
theorem
measure_theory.measure.map_sub_left_ae
{G : Type u_2}
[measurable_space G]
[add_group G]
[has_measurable_add G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
[μ.is_neg_invariant]
(x : G) :
filter.map (λ (t : G), x - t) μ.ae = μ.ae
theorem
measure_theory.measure.map_div_left_ae
{G : Type u_2}
[measurable_space G]
[group G]
[has_measurable_mul G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
[μ.is_inv_invariant]
(x : G) :
filter.map (λ (t : G), x / t) μ.ae = μ.ae
@[protected, instance]
def
measure_theory.measure.regular.neg
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[has_continuous_neg G]
[t2_space G]
[μ.regular] :
@[protected, instance]
def
measure_theory.measure.regular.inv
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[has_continuous_inv G]
[t2_space G]
[μ.regular] :
theorem
measure_theory.regular_inv_iff
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[t2_space G] :
theorem
measure_theory.regular_neg_iff
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[t2_space G] :
theorem
measure_theory.is_open_pos_measure_of_add_left_invariant_of_compact
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[μ.is_add_left_invariant]
(K : set G)
(hK : is_compact K)
(h : ⇑μ K ≠ 0) :
If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to any open set.
theorem
measure_theory.is_open_pos_measure_of_mul_left_invariant_of_compact
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[μ.is_mul_left_invariant]
(K : set G)
(hK : is_compact K)
(h : ⇑μ K ≠ 0) :
If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to any open set.
theorem
measure_theory.is_open_pos_measure_of_add_left_invariant_of_regular
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[μ.is_add_left_invariant]
[μ.regular]
(h₀ : μ ≠ 0) :
A nonzero left-invariant regular measure gives positive mass to any open set.
theorem
measure_theory.is_open_pos_measure_of_mul_left_invariant_of_regular
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[μ.is_mul_left_invariant]
[μ.regular]
(h₀ : μ ≠ 0) :
A nonzero left-invariant regular measure gives positive mass to any open set.
theorem
measure_theory.null_iff_of_is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[μ.is_add_left_invariant]
[μ.regular]
{s : set G}
(hs : is_open s) :
theorem
measure_theory.null_iff_of_is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[μ.is_mul_left_invariant]
[μ.regular]
{s : set G}
(hs : is_open s) :
theorem
measure_theory.measure_ne_zero_iff_nonempty_of_is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[μ.is_mul_left_invariant]
[μ.regular]
(hμ : μ ≠ 0)
{s : set G}
(hs : is_open s) :
theorem
measure_theory.measure_ne_zero_iff_nonempty_of_is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[μ.is_add_left_invariant]
[μ.regular]
(hμ : μ ≠ 0)
{s : set G}
(hs : is_open s) :
theorem
measure_theory.measure_pos_iff_nonempty_of_is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[μ.is_add_left_invariant]
[μ.regular]
(h3μ : μ ≠ 0)
{s : set G}
(hs : is_open s) :
theorem
measure_theory.measure_pos_iff_nonempty_of_is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[μ.is_mul_left_invariant]
[μ.regular]
(h3μ : μ ≠ 0)
{s : set G}
(hs : is_open s) :
theorem
measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[μ.is_mul_left_invariant]
(U : set G)
(hU : is_open U)
(h'U : U.nonempty)
(h : ⇑μ U ≠ ⊤)
{K : set G}
(hK : is_compact K) :
If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass to any compact set.
theorem
measure_theory.measure_lt_top_of_is_compact_of_is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[μ.is_add_left_invariant]
(U : set G)
(hU : is_open U)
(h'U : U.nonempty)
(h : ⇑μ U ≠ ⊤)
{K : set G}
(hK : is_compact K) :
If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass to any compact set.
theorem
measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant'
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[μ.is_mul_left_invariant]
{U : set G}
(hU : (interior U).nonempty)
(h : ⇑μ U ≠ ⊤)
{K : set G}
(hK : is_compact K) :
If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives finite mass to any compact set.
theorem
measure_theory.measure_lt_top_of_is_compact_of_is_add_left_invariant'
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[μ.is_add_left_invariant]
{U : set G}
(hU : (interior U).nonempty)
(h : ⇑μ U ≠ ⊤)
{K : set G}
(hK : is_compact K) :
If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives finite mass to any compact set.
@[simp]
theorem
measure_theory.measure_univ_of_is_mul_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
[group G]
[topological_group G]
[locally_compact_space G]
[noncompact_space G]
(μ : measure_theory.measure G)
[μ.is_open_pos_measure]
[μ.is_mul_left_invariant] :
In a noncompact locally compact group, a left-invariant measure which is positive on open sets has infinite mass.
@[simp]
theorem
measure_theory.measure_univ_of_is_add_left_invariant
{G : Type u_2}
[measurable_space G]
[topological_space G]
[borel_space G]
[add_group G]
[topological_add_group G]
[locally_compact_space G]
[noncompact_space G]
(μ : measure_theory.measure G)
[μ.is_open_pos_measure]
[μ.is_add_left_invariant] :
In a noncompact locally compact additive group, a left-invariant measure which is positive on open sets has infinite mass.
@[protected, instance]
def
is_add_left_invariant.is_add_right_invariant
{G : Type u_2}
[measurable_space G]
[add_comm_semigroup G]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant] :
In an abelian additive
group every left invariant measure is also right-invariant. We don't declare the converse as an
instance, since that would loop type-class inference, and we use is_add_left_invariant as the
default hypothesis in abelian groups.
@[protected, instance]
def
measure_theory.is_mul_left_invariant.is_mul_right_invariant
{G : Type u_2}
[measurable_space G]
[comm_semigroup G]
{μ : measure_theory.measure G}
[μ.is_mul_left_invariant] :
In an abelian group every left invariant measure is also right-invariant.
We don't declare the converse as an instance, since that would loop type-class inference, and
we use is_mul_left_invariant as the default hypothesis in abelian groups.
@[class]
structure
measure_theory.measure.is_add_haar_measure
{G : Type u_4}
[add_group G]
[topological_space G]
[measurable_space G]
(μ : measure_theory.measure G) :
Prop
- to_is_finite_measure_on_compacts : measure_theory.is_finite_measure_on_compacts μ
- to_is_add_left_invariant : μ.is_add_left_invariant
- to_is_open_pos_measure : μ.is_open_pos_measure
A measure on an additive group is an additive Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.
Instances of this typeclass
- measure_theory.measure.prod.is_add_haar_measure
- measure_theory.measure.pi.is_add_haar_measure
- measure_theory.measure.is_add_haar_measure_add_haar_measure
- is_add_haar_measure_basis_add_haar
- measure_theory.is_add_haar_measure_volume_pi
- measure_theory.measure.map_continuous_linear_equiv.is_add_haar_measure
- measure_theory.measure.map_linear_equiv.is_add_haar_measure
- add_circle.measure_theory.measure_space.volume.measure_theory.measure.is_add_haar_measure
- add_circle.haar_add_circle.is_add_haar_measure
@[class]
structure
measure_theory.measure.is_haar_measure
{G : Type u_4}
[group G]
[topological_space G]
[measurable_space G]
(μ : measure_theory.measure G) :
Prop
- to_is_finite_measure_on_compacts : measure_theory.is_finite_measure_on_compacts μ
- to_is_mul_left_invariant : μ.is_mul_left_invariant
- to_is_open_pos_measure : μ.is_open_pos_measure
A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.
@[protected, instance]
def
measure_theory.measure.is_locally_finite_measure_of_is_haar_measure
{G : Type u_1}
[group G]
[measurable_space G]
[topological_space G]
[locally_compact_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure] :
Record that a Haar measure on a locally compact space is locally finite. This is needed as the fact that a measure which is finite on compacts is locally finite is not registered as an instance, to avoid an instance loop.
@[protected, instance]
def
measure_theory.measure.is_locally_finite_measure_of_is_add_haar_measure
{G : Type u_1}
[add_group G]
[measurable_space G]
[topological_space G]
[locally_compact_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure] :
Record that an additive Haar measure on a locally compact space is locally finite. This is needed as the fact that a measure which is finite on compacts is locally finite is not registered as an instance, to avoid an instance loop.
@[simp]
theorem
measure_theory.measure.haar_singleton
{G : Type u_2}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
[topological_group G]
[borel_space G]
(g : G) :
@[simp]
theorem
measure_theory.measure.add_haar_singleton
{G : Type u_2}
[measurable_space G]
[add_group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
[topological_add_group G]
[borel_space G]
(g : G) :
theorem
measure_theory.measure.is_haar_measure.smul
{G : Type u_2}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
{c : ennreal}
(cpos : c ≠ 0)
(ctop : c ≠ ⊤) :
(c • μ).is_haar_measure
theorem
measure_theory.measure.is_add_haar_measure.smul
{G : Type u_2}
[measurable_space G]
[add_group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
{c : ennreal}
(cpos : c ≠ 0)
(ctop : c ≠ ⊤) :
(c • μ).is_add_haar_measure
theorem
measure_theory.measure.is_haar_measure_of_is_compact_nonempty_interior
{G : Type u_2}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
(μ : measure_theory.measure G)
[μ.is_mul_left_invariant]
(K : set G)
(hK : is_compact K)
(h'K : (interior K).nonempty)
(h : ⇑μ K ≠ 0)
(h' : ⇑μ K ≠ ⊤) :
If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is a Haar measure.
theorem
measure_theory.measure.is_add_haar_measure_of_is_compact_nonempty_interior
{G : Type u_2}
[measurable_space G]
[add_group G]
[topological_space G]
[topological_add_group G]
[borel_space G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(K : set G)
(hK : is_compact K)
(h'K : (interior K).nonempty)
(h : ⇑μ K ≠ 0)
(h' : ⇑μ K ≠ ⊤) :
If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is an additive Haar measure.
theorem
measure_theory.measure.is_haar_measure_map
{G : Type u_2}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
[borel_space G]
[topological_group G]
{H : Type u_1}
[group H]
[topological_space H]
[measurable_space H]
[borel_space H]
[t2_space H]
[topological_group H]
(f : G →* H)
(hf : continuous ⇑f)
(h_surj : function.surjective ⇑f)
(h_prop : filter.tendsto ⇑f (filter.cocompact G) (filter.cocompact H)) :
The image of a Haar measure under a continuous surjective proper group homomorphism is again
a Haar measure. See also mul_equiv.is_haar_measure_map.
theorem
measure_theory.measure.is_add_haar_measure_map
{G : Type u_2}
[measurable_space G]
[add_group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
[borel_space G]
[topological_add_group G]
{H : Type u_1}
[add_group H]
[topological_space H]
[measurable_space H]
[borel_space H]
[t2_space H]
[topological_add_group H]
(f : G →+ H)
(hf : continuous ⇑f)
(h_surj : function.surjective ⇑f)
(h_prop : filter.tendsto ⇑f (filter.cocompact G) (filter.cocompact H)) :
The image of an additive Haar measure under a continuous surjective proper additive
group homomorphism is again an additive Haar measure. See also
add_equiv.is_add_haar_measure_map.
theorem
mul_equiv.is_haar_measure_map
{G : Type u_2}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
[borel_space G]
[topological_group G]
{H : Type u_1}
[group H]
[topological_space H]
[measurable_space H]
[borel_space H]
[t2_space H]
[topological_group H]
(e : G ≃* H)
(he : continuous ⇑e)
(hesymm : continuous ⇑(e.symm)) :
A convenience wrapper for measure_theory.measure.is_haar_measure_map.
theorem
add_equiv.is_add_haar_measure_map
{G : Type u_2}
[measurable_space G]
[add_group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
[borel_space G]
[topological_add_group G]
{H : Type u_1}
[add_group H]
[topological_space H]
[measurable_space H]
[borel_space H]
[t2_space H]
[topological_add_group H]
(e : G ≃+ H)
(he : continuous ⇑e)
(hesymm : continuous ⇑(e.symm)) :
A convenience wrapper for measure_theory.measure.is_add_haar_measure_map.
@[protected, instance]
def
measure_theory.measure.is_haar_measure.sigma_finite
{G : Type u_2}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
[sigma_compact_space G] :
A Haar measure on a σ-compact space is σ-finite.
@[protected, instance]
def
measure_theory.measure.is_add_haar_measure.sigma_finite
{G : Type u_2}
[measurable_space G]
[add_group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
[sigma_compact_space G] :
A Haar measure on a σ-compact space is σ-finite.
@[protected, instance]
def
measure_theory.measure.prod.is_haar_measure
{G : Type u_1}
[group G]
[topological_space G]
{mG : measurable_space G}
{H : Type u_2}
[group H]
[topological_space H]
{mH : measurable_space H}
(μ : measure_theory.measure G)
(ν : measure_theory.measure H)
[μ.is_haar_measure]
[ν.is_haar_measure]
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite ν]
[has_measurable_mul G]
[has_measurable_mul H] :
(μ.prod ν).is_haar_measure
@[protected, instance]
def
measure_theory.measure.prod.is_add_haar_measure
{G : Type u_1}
[add_group G]
[topological_space G]
{mG : measurable_space G}
{H : Type u_2}
[add_group H]
[topological_space H]
{mH : measurable_space H}
(μ : measure_theory.measure G)
(ν : measure_theory.measure H)
[μ.is_add_haar_measure]
[ν.is_add_haar_measure]
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite ν]
[has_measurable_add G]
[has_measurable_add H] :
(μ.prod ν).is_add_haar_measure
@[protected, instance]
def
measure_theory.measure.is_haar_measure.has_no_atoms
{G : Type u_2}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
[t1_space G]
[locally_compact_space G]
[(nhds_within 1 {1}ᶜ).ne_bot]
(μ : measure_theory.measure G)
[μ.is_haar_measure] :
If the neutral element of a group is not isolated, then a Haar measure on this group has no atoms.
The additive version of this instance applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.
@[protected, instance]
def
measure_theory.measure.is_add_haar_measure.has_no_atoms
{G : Type u_2}
[measurable_space G]
[add_group G]
[topological_space G]
[topological_add_group G]
[borel_space G]
[t1_space G]
[locally_compact_space G]
[(nhds_within 0 {0}ᶜ).ne_bot]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure] :
If the zero element of an additive group is not isolated, then an additive Haar measure on this group has no atoms.
This applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.