Measures on Groups #
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_1}
[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
- measure_theory.measure.is_add_haar_measure.to_is_add_left_invariant
- measure_theory.has_scalar.smul.measure.is_add_left_invariant
- measure_theory.measure.neg.measure.is_add_left_invariant
- measure_theory.measure.pi.is_add_left_invariant
- measure_theory.pi.is_add_left_invariant_volume
- real.is_add_left_invariant_real_volume
- real.is_add_left_invariant_real_volume_pi
- measure_theory.measure.is_add_left_invariant_add_haar_measure
- measure_theory.is_add_left_invariant_real_volume_pi
@[class]
structure
measure_theory.measure.is_mul_left_invariant
{G : Type u_1}
[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
- measure_theory.measure.is_haar_measure.to_is_mul_left_invariant
- measure_theory.has_scalar.smul.measure.is_mul_left_invariant
- measure_theory.measure.inv.measure.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
@[class]
structure
measure_theory.measure.is_add_right_invariant
{G : Type u_1}
[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.
@[class]
structure
measure_theory.measure.is_mul_right_invariant
{G : Type u_1}
[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.
theorem
measure_theory.map_mul_left_eq_self
{G : Type u_1}
[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_1}
[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_1}
[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_1}
[measurable_space G]
[has_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G) :
⇑(measure_theory.measure.map (λ (_x : G), _x * g)) μ = μ
theorem
measure_theory.forall_measure_preimage_add_iff
{G : Type u_1}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set A → ⇑μ ((λ (h : G), g + h) ⁻¹' A) = ⇑μ A) ↔ μ.is_add_left_invariant
theorem
measure_theory.forall_measure_preimage_mul_iff
{G : Type u_1}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set A → ⇑μ ((λ (h : G), g * h) ⁻¹' A) = ⇑μ A) ↔ μ.is_mul_left_invariant
An alternative way to prove that μ is left invariant under multiplication.
theorem
measure_theory.forall_measure_preimage_mul_right_iff
{G : Type u_1}
[measurable_space G]
[has_mul G]
[has_measurable_mul G]
(μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set A → ⇑μ ((λ (h : G), h * g) ⁻¹' A) = ⇑μ A) ↔ μ.is_mul_right_invariant
An alternative way to prove that μ is left invariant under multiplication.
theorem
measure_theory.forall_measure_preimage_add_right_iff
{G : Type u_1}
[measurable_space G]
[has_add G]
[has_measurable_add G]
(μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set A → ⇑μ ((λ (h : G), h + g) ⁻¹' A) = ⇑μ A) ↔ μ.is_add_right_invariant
@[protected, instance]
def
measure_theory.has_scalar.smul.measure.is_mul_left_invariant
{G : Type u_1}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[μ.is_mul_left_invariant]
(c : ℝ≥0∞) :
(c • μ).is_mul_left_invariant
@[protected, instance]
def
measure_theory.has_scalar.smul.measure.is_add_left_invariant
{G : Type u_1}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant]
(c : ℝ≥0∞) :
(c • μ).is_add_left_invariant
@[protected, instance]
def
measure_theory.has_scalar.smul.measure.is_mul_right_invariant
{G : Type u_1}
[measurable_space G]
[has_mul G]
{μ : measure_theory.measure G}
[μ.is_mul_right_invariant]
(c : ℝ≥0∞) :
(c • μ).is_mul_right_invariant
@[protected, instance]
def
measure_theory.has_scalar.smul.measure.is_add_right_invariant
{G : Type u_1}
[measurable_space G]
[has_add G]
{μ : measure_theory.measure G}
[μ.is_add_right_invariant]
(c : ℝ≥0∞) :
(c • μ).is_add_right_invariant
@[simp]
theorem
measure_theory.measure_preimage_add
{G : Type u_1}
[measurable_space G]
[add_group G]
[has_measurable_add G]
(μ : measure_theory.measure G)
[μ.is_add_left_invariant]
(g : G)
(A : set G) :
@[simp]
theorem
measure_theory.measure_preimage_mul
{G : Type u_1}
[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_1}
[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_1}
[measurable_space G]
[group G]
[has_measurable_mul G]
(μ : measure_theory.measure G)
[μ.is_mul_right_invariant]
(g : G)
(A : set G) :
@[protected]
noncomputable
def
measure_theory.measure.inv
{G : Type u_1}
[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_1}
[measurable_space G]
[has_neg G]
(μ : measure_theory.measure G) :
The measure A ↦ μ (- A), where - A is the pointwise negation of A.
Equations
theorem
measure_theory.measure.neg_apply
{G : Type u_1}
[measurable_space G]
[add_group G]
[has_measurable_neg G]
(μ : measure_theory.measure G)
(s : set G) :
theorem
measure_theory.measure.inv_apply
{G : Type u_1}
[measurable_space G]
[group G]
[has_measurable_inv G]
(μ : measure_theory.measure G)
(s : set G) :
@[protected, simp]
theorem
measure_theory.measure.inv_inv
{G : Type u_1}
[measurable_space G]
[group G]
[has_measurable_inv G]
(μ : measure_theory.measure G) :
@[protected, simp]
theorem
measure_theory.measure.neg_neg
{G : Type u_1}
[measurable_space G]
[add_group G]
[has_measurable_neg G]
(μ : measure_theory.measure G) :
@[protected, instance]
def
measure_theory.measure.inv.measure.is_mul_right_invariant
{G : Type u_1}
[measurable_space G]
[group G]
[has_measurable_mul G]
[has_measurable_inv G]
{μ : measure_theory.measure G}
[μ.is_mul_left_invariant] :
@[protected, instance]
def
measure_theory.measure.neg.measure.is_add_right_invariant
{G : Type u_1}
[measurable_space G]
[add_group G]
[has_measurable_add G]
[has_measurable_neg G]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant] :
@[protected, instance]
def
measure_theory.measure.inv.measure.is_mul_left_invariant
{G : Type u_1}
[measurable_space G]
[group G]
[has_measurable_mul G]
[has_measurable_inv G]
{μ : measure_theory.measure G}
[μ.is_mul_right_invariant] :
@[protected, instance]
def
measure_theory.measure.neg.measure.is_add_left_invariant
{G : Type u_1}
[measurable_space G]
[add_group G]
[has_measurable_add G]
[has_measurable_neg G]
{μ : measure_theory.measure G}
[μ.is_add_right_invariant] :
@[protected, instance]
def
measure_theory.measure.regular.neg
{G : Type u_1}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[add_group G]
[topological_add_group G]
[t2_space G]
[μ.regular] :
@[protected, instance]
def
measure_theory.measure.regular.inv
{G : Type u_1}
[measurable_space G]
[topological_space G]
[borel_space G]
{μ : measure_theory.measure G}
[group G]
[topological_group G]
[t2_space G]
[μ.regular] :
theorem
measure_theory.regular_inv_iff
{G : Type u_1}
[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_1}
[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_1}
[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) :
theorem
measure_theory.is_open_pos_measure_of_mul_left_invariant_of_compact
{G : Type u_1}
[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_1}
[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) :
theorem
measure_theory.is_open_pos_measure_of_mul_left_invariant_of_regular
{G : Type u_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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_1}
[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) :
theorem
measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant'
{G : Type u_1}
[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_1}
[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) :
@[protected, instance]
def
measure_theory.is_mul_left_invariant.is_add_right_invariant
{G : Type u_1}
[measurable_space G]
[add_comm_group G]
{μ : measure_theory.measure G}
[μ.is_add_left_invariant] :
@[protected, instance]
def
measure_theory.is_mul_left_invariant.is_mul_right_invariant
{G : Type u_1}
[measurable_space G]
[comm_group 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 default hypotheses in abelian groups.
@[class]
structure
measure_theory.measure.is_add_haar_measure
{G : Type u_2}
[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.
@[class]
structure
measure_theory.measure.is_haar_measure
{G : Type u_2}
[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.
@[simp]
theorem
measure_theory.measure.haar_singleton
{G : Type u_1}
[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_1}
[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_1}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
{c : ℝ≥0∞}
(cpos : c ≠ 0)
(ctop : c ≠ ⊤) :
(c • μ).is_haar_measure
theorem
measure_theory.measure.is_add_haar_measure.smul
{G : Type u_1}
[measurable_space G]
[add_group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
{c : ℝ≥0∞}
(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_1}
[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_1}
[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 ≠ ⊤) :
theorem
measure_theory.measure.is_haar_measure_map
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
[borel_space G]
[topological_group G]
{H : Type u_2}
[group H]
[topological_space H]
[measurable_space H]
[borel_space H]
[t2_space H]
[topological_group H]
(f : G ≃* H)
(hf : continuous ⇑f)
(hfsymm : continuous ⇑(f.symm)) :
The image of a Haar measure under a group homomorphism which is also a homeomorphism is again a Haar measure.
theorem
measure_theory.measure.is_add_haar_measure_map
{G : Type u_1}
[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_2}
[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)
(hfsymm : continuous ⇑(f.symm)) :
@[protected, instance]
def
measure_theory.measure.is_haar_measure.sigma_finite
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_haar_measure]
[sigma_compact_space G] :
A Haar measure on a sigma-compact space is sigma-finite.
@[protected, instance]
def
measure_theory.measure.is_add_haar_measure.sigma_finite
{G : Type u_1}
[measurable_space G]
[add_group G]
[topological_space G]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure]
[sigma_compact_space G] :
@[protected, instance]
def
measure_theory.measure.is_haar_measure.has_no_atoms
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
[t1_space G]
[locally_compact_space G]
[(𝓝[{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 atom.
This 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_1}
[measurable_space G]
[add_group G]
[topological_space G]
[topological_add_group G]
[borel_space G]
[t1_space G]
[locally_compact_space G]
[(𝓝[{0}ᶜ] 0).ne_bot]
(μ : measure_theory.measure G)
[μ.is_add_haar_measure] :