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.
instance
MeasureTheory.SMulInvariantMeasure.zero
{M : Type v}
{α : Type w}
[MeasurableSpace α]
[SMul M α]
:
Equations
- ⋯ = ⋯
instance
MeasureTheory.VAddInvariantMeasure.zero
{M : Type v}
{α : Type w}
[MeasurableSpace α]
[VAdd M α]
:
Equations
- ⋯ = ⋯
instance
MeasureTheory.SMulInvariantMeasure.add
{M : Type v}
{α : Type w}
[SMul M α]
{m : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure M α μ]
[MeasureTheory.SMulInvariantMeasure M α ν]
:
MeasureTheory.SMulInvariantMeasure M α (μ + ν)
Equations
- ⋯ = ⋯
instance
MeasureTheory.VAddInvariantMeasure.add
{M : Type v}
{α : Type w}
[VAdd M α]
{m : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure M α μ]
[MeasureTheory.VAddInvariantMeasure M α ν]
:
MeasureTheory.VAddInvariantMeasure M α (μ + ν)
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
{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_nnreal
{M : Type v}
{α : Type w}
[SMul M α]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure M α μ]
(c : NNReal)
:
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
- ⋯ = ⋯
theorem
MeasureTheory.measure_preimage_smul_le
{G : Type u}
{α : Type w}
{m : MeasurableSpace α}
[SMul G α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.SMulInvariantMeasure G α μ]
(c : G)
(s : Set α)
:
See also measure_preimage_smul_of_nullMeasurableSet and measure_preimage_smul.
theorem
MeasureTheory.measure_preimage_vadd_le
{G : Type u}
{α : Type w}
{m : MeasurableSpace α}
[VAdd G α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.VAddInvariantMeasure G α μ]
(c : G)
(s : Set α)
:
See also measure_preimage_smul_of_nullMeasurableSet and measure_preimage_smul.
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.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.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)
:
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)
:
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)
:
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)
:
@[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 α)
:
@[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 α)
:
@[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 α)
:
@[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 α)
:
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)
:
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)
:
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)
:
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)
:
@[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_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_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.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.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.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.smul_set_ae_le
{G : Type u}
{α : Type w}
{m : MeasurableSpace α}
[Group G]
[MulAction G α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
(c : G)
{s t : Set α}
:
@[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 t : Set α}
:
@[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 t : Set α}
:
@[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 t : Set α}
:
@[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.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.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) μ = μ
@[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) μ = μ
theorem
MeasureTheory.MeasurePreserving.smulInvariantMeasure_iterateMulAct
{α : Type w}
{f : α → α}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.MeasurePreserving f μ μ)
:
theorem
MeasureTheory.MeasurePreserving.vaddInvariantMeasure_iterateAddAct
{α : Type w}
{f : α → α}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.MeasurePreserving f μ μ)
:
theorem
MeasureTheory.smulInvariantMeasure_iterateMulAct
{α : Type w}
{f : α → α}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hf : Measurable f)
:
theorem
MeasureTheory.vaddInvariantMeasure_iterateAddAct
{α : Type w}
{f : α → α}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hf : Measurable 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)
:
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)
:
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
- ⋯ = ⋯
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
- ⋯ = ⋯
theorem
MeasureTheory.smulInvariantMeasure_tfae
(G : Type u)
{α : Type w}
{m : MeasurableSpace α}
[Group G]
[MulAction G α]
(μ : MeasureTheory.Measure α)
[MeasurableSpace G]
[MeasurableSMul G α]
:
[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 : Gand a measurable sets, the measure of the preimage ofsunder scalar multiplication bycis equal to the measure ofs;2: for every
c : Gand a measurable sets, the measure of the imagec • sofsunder scalar multiplication bycis equal to the measure ofs;3, 4: properties 2, 3 for any set, including non-measurable ones;
5: for any
c : G, scalar multiplication bycmapsμtoμ;6: for any
c : G, scalar multiplication bycis a measure preserving map.
theorem
MeasureTheory.vaddInvariantMeasure_tfae
(G : Type u)
{α : Type w}
{m : MeasurableSpace α}
[AddGroup G]
[AddAction G α]
(μ : MeasureTheory.Measure α)
[MeasurableSpace G]
[MeasurableVAdd G α]
:
[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 : Gand a measurable sets, the measure of the preimage ofsunder vector addition(c +ᵥ ·)is equal to the measure ofs;2: for every
c : Gand a measurable sets, the measure of the imagec +ᵥ sofsunder vector addition(c +ᵥ ·)is equal to the measure ofs;3, 4: properties 2, 3 for any set, including non-measurable ones;
5: for any
c : G, vector addition ofcmapsμtoμ;6: for any
c : G, vector addition ofcis a measure preserving map.
theorem
MeasureTheory.NullMeasurableSet.smul
{G : Type u}
{α : Type w}
{m : MeasurableSpace α}
[Group G]
[MulAction G α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
[MeasurableSpace G]
[MeasurableSMul G α]
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(c : G)
:
MeasureTheory.NullMeasurableSet (c • s) μ
theorem
MeasureTheory.NullMeasurableSet.vadd
{G : Type u}
{α : Type w}
{m : MeasurableSpace α}
[AddGroup G]
[AddAction G α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
[MeasurableSpace G]
[MeasurableVAdd G α]
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(c : G)
:
MeasureTheory.NullMeasurableSet (c +ᵥ s) μ
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 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.
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 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.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 ≠ ⊤)
:
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 ≠ ⊤)
:
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_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
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)
:
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)
:
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)
:
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)
: