Measures invariant under group actions

A measure μ : Measure α is said to be invariant under an action of a group G if scalar multiplication by c : G is a measure preserving map for all c. In this file we define a typeclass for measures invariant under action of an (additive or multiplicative) group and prove some basic properties of such measures.

class MeasureTheory.VAddInvariantMeasure (M : Type u_1) (α : Type u_2) [VAdd M α] : {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure μ : Measure α is invariant under an additive action of M on α if for any measurable set s : Set α and c : M, the measure of its preimage under fun x => c +ᵥ x is equal to the measure of s.

• measure_preimage_vadd : ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

theorem MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd {M : Type u_1} {α : Type u_2} [VAdd M α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.VAddInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

class MeasureTheory.SMulInvariantMeasure (M : Type u_1) (α : Type u_2) [SMul M α] : {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure μ : Measure α is invariant under a multiplicative action of M on α if for any measurable set s : Set α and c : M, the measure of its preimage under fun x => c • x is equal to the measure of s.

• measure_preimage_smul : ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

theorem MeasureTheory.SMulInvariantMeasure.measure_preimage_smul {M : Type u_1} {α : Type u_2} [SMul M α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.SMulInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

instance MeasureTheory.VAddInvariantMeasure.zero {M : Type v} {α : Type w} [MeasurableSpace α] [VAdd M α] : MeasureTheory.VAddInvariantMeasure M α 0

Equations

• ⋯ = ⋯

instance MeasureTheory.SMulInvariantMeasure.zero {M : Type v} {α : Type w} [MeasurableSpace α] [SMul M α] : MeasureTheory.SMulInvariantMeasure M α 0

Equations

• ⋯ = ⋯

instance MeasureTheory.VAddInvariantMeasure.add {M : Type v} {α : Type w} [VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure M α μ] [MeasureTheory.VAddInvariantMeasure M α ν] : MeasureTheory.VAddInvariantMeasure M α (μ + ν)

Equations

• ⋯ = ⋯

instance MeasureTheory.SMulInvariantMeasure.add {M : Type v} {α : Type w} [SMul M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure M α μ] [MeasureTheory.SMulInvariantMeasure M α ν] : MeasureTheory.SMulInvariantMeasure M α (μ + ν)

Equations

• ⋯ = ⋯

instance MeasureTheory.VAddInvariantMeasure.vadd {M : Type v} {α : Type w} [VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure M α μ] (c : ENNReal) : MeasureTheory.VAddInvariantMeasure M α (c • μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.SMulInvariantMeasure.smul {M : Type v} {α : Type w} [SMul M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure M α μ] (c : ENNReal) : MeasureTheory.SMulInvariantMeasure M α (c • μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.VAddInvariantMeasure.vadd_nnreal {M : Type v} {α : Type w} [VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure M α μ] (c : NNReal) : MeasureTheory.VAddInvariantMeasure M α (c • μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.SMulInvariantMeasure.smul_nnreal {M : Type v} {α : Type w} [SMul M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure M α μ] (c : NNReal) : MeasureTheory.SMulInvariantMeasure M α (c • μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.measure_preimage_vadd_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) ≤ μ s

See also measure_preimage_smul_of_nullMeasurableSet and measure_preimage_smul.

theorem MeasureTheory.measure_preimage_smul_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c • x) ⁻¹' s) ≤ μ s

See also measure_preimage_smul_of_nullMeasurableSet and measure_preimage_smul.

theorem MeasureTheory.tendsto_vadd_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) : Filter.Tendsto (fun (x : α) => c +ᵥ x) (MeasureTheory.ae μ) (MeasureTheory.ae μ)

See also vadd_ae.

theorem MeasureTheory.tendsto_smul_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) : Filter.Tendsto (fun (x : α) => c • x) (MeasureTheory.ae μ) (MeasureTheory.ae μ)

See also smul_ae.

theorem MeasureTheory.measure_preimage_vadd_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = 0

theorem MeasureTheory.measure_preimage_smul_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ ((fun (x : α) => c • x) ⁻¹' s) = 0

theorem MeasureTheory.measure_preimage_vadd_of_nullMeasurableSet {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (c : G) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

theorem MeasureTheory.measure_preimage_smul_of_nullMeasurableSet {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (c : G) : μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

@[simp]

theorem MeasureTheory.measure_preimage_vadd {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

@[simp]

theorem MeasureTheory.measure_preimage_smul {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

@[simp]

theorem MeasureTheory.measure_vadd {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s : Set α) : μ (c +ᵥ s) = μ s

@[simp]

theorem MeasureTheory.measure_smul {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s : Set α) : μ (c • s) = μ s

theorem MeasureTheory.measure_vadd_eq_zero_iff {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (c : G) : μ (c +ᵥ s) = 0 ↔ μ s = 0

theorem MeasureTheory.measure_smul_eq_zero_iff {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (c : G) : μ (c • s) = 0 ↔ μ s = 0

theorem MeasureTheory.measure_vadd_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ (c +ᵥ s) = 0

theorem MeasureTheory.measure_smul_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ (c • s) = 0

@[simp]

theorem MeasureTheory.vadd_mem_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α} : c +ᵥ s ∈ MeasureTheory.ae μ ↔ s ∈ MeasureTheory.ae μ

@[simp]

theorem MeasureTheory.smul_mem_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α} : c • s ∈ MeasureTheory.ae μ ↔ s ∈ MeasureTheory.ae μ

@[simp]

theorem MeasureTheory.vadd_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) : c +ᵥ MeasureTheory.ae μ = MeasureTheory.ae μ

@[simp]

theorem MeasureTheory.smul_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) : c • MeasureTheory.ae μ = MeasureTheory.ae μ

@[simp]

theorem MeasureTheory.eventuallyConst_vadd_set_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α} : Filter.EventuallyConst (c +ᵥ s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)

@[simp]

theorem MeasureTheory.eventuallyConst_smul_set_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α} : Filter.EventuallyConst (c • s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)

@[simp]

theorem MeasureTheory.vadd_set_ae_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} : c +ᵥ s ≤ᵐ[μ] c +ᵥ t ↔ s ≤ᵐ[μ] t

@[simp]

theorem MeasureTheory.smul_set_ae_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} : c • s ≤ᵐ[μ] c • t ↔ s ≤ᵐ[μ] t

@[simp]

theorem MeasureTheory.vadd_set_ae_eq {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} : c +ᵥ s =ᵐ[μ] c +ᵥ t ↔ s =ᵐ[μ] t

@[simp]

theorem MeasureTheory.smul_set_ae_eq {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} : c • s =ᵐ[μ] c • t ↔ s =ᵐ[μ] t

@[simp]

theorem MeasureTheory.measurePreserving_vadd {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [VAdd M α] [MeasurableVAdd M α] (c : M) (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] : MeasureTheory.MeasurePreserving (fun (x : α) => c +ᵥ x) μ μ

@[simp]

theorem MeasureTheory.measurePreserving_smul {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [SMul M α] [MeasurableSMul M α] (c : M) (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] : MeasureTheory.MeasurePreserving (fun (x : α) => c • x) μ μ

@[simp]

theorem MeasureTheory.map_vadd {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [VAdd M α] [MeasurableVAdd M α] (c : M) (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] : MeasureTheory.Measure.map (fun (x : α) => c +ᵥ x) μ = μ

@[simp]

theorem MeasureTheory.map_smul {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [SMul M α] [MeasurableSMul M α] (c : M) (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] : MeasureTheory.Measure.map (fun (x : α) => c • x) μ = μ

theorem MeasureTheory.vaddInvariantMeasure_map {M : Type uM} {α : Type uα} {β : Type uβ} [MeasurableSpace M] [MeasurableSpace α] [MeasurableSpace β] [VAdd M α] [VAdd M β] [MeasurableVAdd M β] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] (f : α → β) (hsmul : ∀ (m : M) (a : α), f (m +ᵥ a) = m +ᵥ f a) (hf : Measurable f) : MeasureTheory.VAddInvariantMeasure M β (MeasureTheory.Measure.map f μ)

theorem MeasureTheory.smulInvariantMeasure_map {M : Type uM} {α : Type uα} {β : Type uβ} [MeasurableSpace M] [MeasurableSpace α] [MeasurableSpace β] [SMul M α] [SMul M β] [MeasurableSMul M β] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] (f : α → β) (hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a) (hf : Measurable f) : MeasureTheory.SMulInvariantMeasure M β (MeasureTheory.Measure.map f μ)

instance MeasureTheory.vaddInvariantMeasure_map_vadd {M : Type uM} {N : Type uN} {α : Type uα} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [VAdd M α] [VAdd N α] [VAddCommClass N M α] [MeasurableVAdd M α] [MeasurableVAdd N α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] (n : N) : MeasureTheory.VAddInvariantMeasure M α (MeasureTheory.Measure.map (fun (x : α) => n +ᵥ x) μ)

Equations

• ⋯ = ⋯

instance MeasureTheory.smulInvariantMeasure_map_smul {M : Type uM} {N : Type uN} {α : Type uα} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [SMul M α] [SMul N α] [SMulCommClass N M α] [MeasurableSMul M α] [MeasurableSMul N α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] (n : N) : MeasureTheory.SMulInvariantMeasure M α (MeasureTheory.Measure.map (fun (x : α) => n • x) μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.vaddInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] [MeasurableSpace G] [MeasurableVAdd G α] (μ : MeasureTheory.Measure α) : [MeasureTheory.VAddInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c +ᵥ s) = μ s, ∀ (c : G) (s : Set α), μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c +ᵥ s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun (x : α) => c +ᵥ x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun (x : α) => c +ᵥ x) μ μ].TFAE

Equivalent definitions of a measure invariant under an additive action of a group.

• 0: VAddInvariantMeasure G α μ;

• 1: for every c : G and a measurable set s, the measure of the preimage of s under vector addition (c +ᵥ ·) is equal to the measure of s;

• 2: for every c : G and a measurable set s, the measure of the image c +ᵥ s of s under vector addition (c +ᵥ ·) is equal to the measure of s;

• 3, 4: properties 2, 3 for any set, including non-measurable ones;

• 5: for any c : G, vector addition of c maps μ to μ;

• 6: for any c : G, vector addition of c is a measure preserving map.

theorem MeasureTheory.smulInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSMul G α] (μ : MeasureTheory.Measure α) : [MeasureTheory.SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun (x : α) => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun (x : α) => c • x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun (x : α) => c • x) μ μ].TFAE

Equivalent definitions of a measure invariant under a multiplicative action of a group.

• 0: SMulInvariantMeasure G α μ;

• 1: for every c : G and a measurable set s, the measure of the preimage of s under scalar multiplication by c is equal to the measure of s;

• 2: for every c : G and a measurable set s, the measure of the image c • s of s under scalar multiplication by c is equal to the measure of s;

• 3, 4: properties 2, 3 for any set, including non-measurable ones;

• 5: for any c : G, scalar multiplication by c maps μ to μ;

• 6: for any c : G, scalar multiplication by c is a measure preserving map.

theorem MeasureTheory.NullMeasurableSet.vadd {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] [MeasurableSpace G] [MeasurableVAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (c : G) : MeasureTheory.NullMeasurableSet (c +ᵥ s) μ

theorem MeasureTheory.NullMeasurableSet.smul {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (c : G) : MeasureTheory.NullMeasurableSet (c • s) μ

abbrev MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero.match_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] {K : Set α} {U : Set α} (motive : (∃ (I : Finset G), K ⊆ ⋃ g ∈ I, g +ᵥ U) → Prop) : ∀ (x : ∃ (I : Finset G), K ⊆ ⋃ g ∈ I, g +ᵥ U), (∀ (t : Finset G) (ht : K ⊆ ⋃ g ∈ t, g +ᵥ U), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {K : Set α} {U : Set α} (hK : IsCompact K) (hμK : μ K ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

If measure μ is invariant under an additive group action and is nonzero on a compact set K, then it is positive on any nonempty open set. In case of a regular measure, one can assume μ ≠ 0 instead of μ K ≠ 0, see MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.

theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {K : Set α} {U : Set α} (hK : IsCompact K) (hμK : μ K ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

If measure μ is invariant under a group action and is nonzero on a compact set K, then it is positive on any nonempty open set. In case of a regular measure, one can assume μ ≠ 0 instead of μ K ≠ 0, see MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero.

abbrev MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant.match_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] {U : Set α} (x : α) (motive : (∃ (c : G), c +ᵥ x ∈ U) → Prop) : ∀ (x_1 : ∃ (c : G), c +ᵥ x ∈ U), (∀ (g : G) (hg : g +ᵥ x ∈ U), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} (hU : IsOpen U) (hne : U.Nonempty) (hμU : μ U ≠ ⊤) : MeasureTheory.IsLocallyFiniteMeasure μ

theorem MeasureTheory.isLocallyFiniteMeasure_of_smulInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} (hU : IsOpen U) (hne : U.Nonempty) (hμU : μ U ≠ ⊤) : MeasureTheory.IsLocallyFiniteMeasure μ

theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

abbrev MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.match_1 {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] (motive : (∃ (K : Set α), IsCompact K ∧ μ K ≠ 0) → Prop) : ∀ (x : ∃ (K : Set α), IsCompact K ∧ μ K ≠ 0), (∀ (_K : Set α) (hK : IsCompact _K) (hμK : μ _K ≠ 0), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

theorem MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : 0 < μ U ↔ U.Nonempty

theorem MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : 0 < μ U ↔ U.Nonempty

theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : μ U = 0 ↔ U = ∅

theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : μ U = 0 ↔ U = ∅