mathlib documentation

measure_theory.group

Measures on Groups #

We develop some properties of measures on (topological) groups

source
def measure_theory.is_mul_left_invariant {G : Type u_1} [measurable_space G] [has_mul G] (μ : set G → ℝ≥0∞) :
Prop

A measure μ on a topological group is left invariant if the measure of left translations of a set are equal to the measure of the set itself. To left translate sets we use preimage under left multiplication, since preimages are nicer to work with than images.

Equations
source
def measure_theory.is_add_left_invariant {G : Type u_1} [measurable_space G] [has_add G] (μ : set G → ℝ≥0∞) :
Prop

A measure on a topological group is left invariant if the measure of left translations of a set are equal to the measure of the set itself. To left translate sets we use preimage under left addition, since preimages are nicer to work with than images.

source
def measure_theory.is_add_right_invariant {G : Type u_1} [measurable_space G] [has_add G] (μ : set G → ℝ≥0∞) :
Prop

A measure on a topological group is right invariant if the measure of right translations of a set are equal to the measure of the set itself. To right translate sets we use preimage under right addition, since preimages are nicer to work with than images.

source
def measure_theory.is_mul_right_invariant {G : Type u_1} [measurable_space G] [has_mul G] (μ : set G → ℝ≥0∞) :
Prop

A measure μ on a topological group is right invariant if the measure of right translations of a set are equal to the measure of the set itself. To right translate sets we use preimage under right multiplication, since preimages are nicer to work with than images.

Equations
source
theorem measure_theory.measure.map_add_left_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [has_add G] [has_continuous_add G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), ⇑(measure_theory.measure.map (has_add.add g)) μ = μ) ↔ measure_theory.is_add_left_invariant ⇑μ
source
theorem measure_theory.measure.map_mul_left_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [has_mul G] [has_continuous_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), ⇑(measure_theory.measure.map (has_mul.mul g)) μ = μ) ↔ measure_theory.is_mul_left_invariant ⇑μ
source
theorem measure_theory.measure.map_add_right_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [has_add G] [has_continuous_add G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), ⇑(measure_theory.measure.map (λ (h : G), h + g)) μ = μ) ↔ measure_theory.is_add_right_invariant ⇑μ
source
theorem measure_theory.measure.map_mul_right_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [has_mul G] [has_continuous_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), ⇑(measure_theory.measure.map (λ (h : G), h * g)) μ = μ) ↔ measure_theory.is_mul_right_invariant ⇑μ
source
@[protected]
def measure_theory.measure.inv {G : Type u_1} [measurable_space G] [has_inv G] (μ : measure_theory.measure G) :
measure_theory.measure G

The measure A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.

Equations
source
@[protected]
def measure_theory.measure.neg {G : Type u_1} [measurable_space G] [has_neg G] (μ : measure_theory.measure G) :
measure_theory.measure G

The measure A ↦ μ (- A), where - A is the pointwise negation of A.

source
theorem measure_theory.measure.neg_apply {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] (μ : measure_theory.measure G) {s : set G} (hs : measurable_set s) :
⇑(μ.neg) s = ⇑μ (-s)
source
theorem measure_theory.measure.inv_apply {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] (μ : measure_theory.measure G) {s : set G} (hs : measurable_set s) :
⇑(μ.inv) s = ⇑μ s⁻¹
source
@[protected, simp]
theorem measure_theory.measure.inv_inv {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] (μ : measure_theory.measure G) :
μ.inv.inv = μ
source
@[protected, simp]
theorem measure_theory.measure.neg_neg {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] (μ : measure_theory.measure G) :
μ.neg.neg = μ
source
theorem measure_theory.measure.regular.neg {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} [t2_space G] (hμ : μ.regular) :
μ.neg.regular
source
theorem measure_theory.measure.regular.inv {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} [t2_space G] (hμ : μ.regular) :
μ.inv.regular
source
@[simp]
theorem measure_theory.regular_inv_iff {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} [t2_space G] :
μ.inv.regular ↔ μ.regular
source
@[simp]
theorem measure_theory.regular_neg_iff {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} [t2_space G] :
μ.neg.regular ↔ μ.regular
source
theorem measure_theory.is_add_left_invariant.neg {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} (h : measure_theory.is_add_left_invariant ⇑μ) :
measure_theory.is_add_right_invariant ⇑(μ.neg)
source
theorem measure_theory.is_mul_left_invariant.inv {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} (h : measure_theory.is_mul_left_invariant ⇑μ) :
measure_theory.is_mul_right_invariant ⇑(μ.inv)
source
theorem measure_theory.is_add_right_invariant.neg {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} (h : measure_theory.is_add_right_invariant ⇑μ) :
measure_theory.is_add_left_invariant ⇑(μ.neg)
source
theorem measure_theory.is_mul_right_invariant.inv {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} (h : measure_theory.is_mul_right_invariant ⇑μ) :
measure_theory.is_mul_left_invariant ⇑(μ.inv)
source
@[simp]
theorem measure_theory.is_mul_right_invariant_inv {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} :
measure_theory.is_mul_right_invariant ⇑(μ.inv) ↔ measure_theory.is_mul_left_invariant ⇑μ
source
@[simp]
theorem measure_theory.is_add_right_invariant_neg {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} :
measure_theory.is_add_right_invariant ⇑(μ.neg) ↔ measure_theory.is_add_left_invariant ⇑μ
source
@[simp]
theorem measure_theory.is_add_left_invariant_neg {G : Type u_1} [measurable_space G] [add_group G] [topological_space G] [topological_add_group G] [borel_space G] {μ : measure_theory.measure G} :
measure_theory.is_add_left_invariant ⇑(μ.neg) ↔ measure_theory.is_add_right_invariant ⇑μ
source
@[simp]
theorem measure_theory.is_mul_left_invariant_inv {G : Type u_1} [measurable_space G] [group G] [topological_space G] [topological_group G] [borel_space G] {μ : measure_theory.measure G} :
measure_theory.is_mul_left_invariant ⇑(μ.inv) ↔ measure_theory.is_mul_right_invariant ⇑μ

Properties of regular left invariant measures

source
theorem measure_theory.is_mul_left_invariant.null_iff_empty {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [group G] [topological_group G] (hμ : μ.regular) (h2μ : measure_theory.is_mul_left_invariant ⇑μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) :
⇑μ s = 0 ↔ s = ∅
source
theorem measure_theory.measure.is_add_left_invariant.null_iff_empty {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [add_group G] [topological_add_group G] (hμ : μ.regular) (h2μ : measure_theory.is_add_left_invariant ⇑μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) :
⇑μ s = 0 ↔ s = ∅
source
theorem measure_theory.is_mul_left_invariant.null_iff {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [group G] [topological_group G] (hμ : μ.regular) (h2μ : measure_theory.is_mul_left_invariant ⇑μ) {s : set G} (hs : is_open s) :
⇑μ s = 0 ↔ s = ∅ ∨ μ = 0
source
theorem measure_theory.measure.is_add_left_invariant.null_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] (hμ : μ.regular) (h2μ : measure_theory.is_add_left_invariant ⇑μ) {s : set G} (hs : is_open s) :
⇑μ s = 0 ↔ s = ∅ ∨ μ = 0
source
theorem measure_theory.measure.is_add_left_invariant.measure_ne_zero_iff_nonempty {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [add_group G] [topological_add_group G] (hμ : μ.regular) (h2μ : measure_theory.is_add_left_invariant ⇑μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) :
⇑μ s ≠ 0 ↔ s.nonempty
source
theorem measure_theory.is_mul_left_invariant.measure_ne_zero_iff_nonempty {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [group G] [topological_group G] (hμ : μ.regular) (h2μ : measure_theory.is_mul_left_invariant ⇑μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) :
⇑μ s ≠ 0 ↔ s.nonempty
source
theorem measure_theory.lintegral_eq_zero_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] (hμ : μ.regular) (h2μ : measure_theory.is_mul_left_invariant ⇑μ) (h3μ : μ ≠ 0) {f : G → ℝ≥0∞} (hf : continuous f) :
∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0

For nonzero regular left invariant measures, the integral of a continuous nonnegative function f is 0 iff f is 0.

source
theorem measure_theory.lintegral_mul_left_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [group G] [has_continuous_mul G] (hμ : measure_theory.is_mul_left_invariant ⇑μ) (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ

Translating a function by left-multiplication does not change its lintegral with respect to a left-invariant measure.

source
theorem measure_theory.lintegral_add_left_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [add_group G] [has_continuous_add G] (hμ : measure_theory.is_add_left_invariant ⇑μ) (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (g + x) ∂μ = ∫⁻ (x : G), f x ∂μ
source
theorem measure_theory.lintegral_add_right_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [add_group G] [has_continuous_add G] (hμ : measure_theory.is_add_right_invariant ⇑μ) (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (x + g) ∂μ = ∫⁻ (x : G), f x ∂μ
source
theorem measure_theory.lintegral_mul_right_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [group G] [has_continuous_mul G] (hμ : measure_theory.is_mul_right_invariant ⇑μ) (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ

Translating a function by right-multiplication does not change its lintegral with respect to a right-invariant measure.