MeasureTheory.vaddInvariantMeasure_tfae
theorem MeasureTheory.vaddInvariantMeasure_tfae :
∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : 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
This theorem provides equivalent definitions of a measure that is invariant under the action of an additive group. Here, the group `G` acts additively on the set `α`, and `μ` is a measure on `α`. The equivalent definitions are:
- `VAddInvariantMeasure G α μ`: The measure `μ` is invariant under the additive action of `G`.
- For every group element `c : G` and measurable set `s : Set α`, the measure of the preimage of `s` under vector addition `(c +ᵥ ·)` is equal to the measure of `s`.
- For every group element `c : G` and measurable set `s : Set α`, the measure of the image `c +ᵥ s` of `s` under vector addition `(c +ᵥ ·)` is equal to the measure of `s`.
- These properties hold for any set `s : Set α`, even if it's not measurable.
- For any group element `c : G`, the vector addition of `c` maps the measure `μ` to itself.
- For any group element `c : G`, the vector addition of `c` is a measure preserving map. In other words, it doesn't change the measure of any set.
This theorem asserts that these six conditions are equivalent to one another.
More concisely: A measure `μ` on an additive group `(G, +)` is invariant under the group action if and only if for all group elements `c : G` and measurable sets `s : Set α`, the measures of the preimage `c +ᵥ s` and image `c + s` under vector addition are equal.
|
MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero
theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero :
∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : MeasurableSMul G α] {μ : MeasureTheory.Measure α}
[inst_4 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_5 : TopologicalSpace α]
[inst_6 : ContinuousConstSMul G α] [inst : MulAction.IsMinimal G α] {K U : Set α},
IsCompact K → ↑↑μ K ≠ 0 → IsOpen U → U.Nonempty → 0 < ↑↑μ U
This theorem states that for a group `G` acting on a type `α`, if a measure `μ` is invariant under the action of the group and it is nonzero on a compact set `K`, then it is positive on any nonempty open set `U`. In the case of a regular measure, it is sufficient to assume that the measure `μ` is not equal to zero instead of the measure of `K` being nonzero. This is also conditioned on `α` being a topological space and the constant scalar multiplication of `G` and `α` being continuous.
More concisely: If `μ:` `G` -> Filter.Algebras.MeasurableSet `α` -> ℝ is a continuous, invariant, and non-zero measure on the topological space `α` with a continuous action of the group `G`, then `μ(U) > 0` for every nonempty open set `U` in `α`.
|
MeasureTheory.measurePreserving_smul
theorem MeasureTheory.measurePreserving_smul :
∀ {M : Type v} {α : Type w} {m : MeasurableSpace α} [inst : MeasurableSpace M] [inst_1 : SMul M α]
[inst : MeasurableSMul M α] (c : M) (μ : MeasureTheory.Measure α)
[inst : MeasureTheory.SMulInvariantMeasure M α μ], MeasureTheory.MeasurePreserving (fun x => c • x) μ μ
This theorem states that for any type `M` and `α`, and a measure space `α`, if `M` and `α` have a scalar multiplication (`SMul`) operation and `M`, `α` and a measure `μ` satisfy the `SMulInvariantMeasure` property, then the function that maps each element `x` of `α` to the result of the scalar multiplication of `x` by some constant `c` of type `M` preserves the measure `μ`. In other words, scalar multiplication does not change the measure of the space under these conditions.
More concisely: For any measure space `(α, μ)`, type `M` with scalar multiplication `SMul`, and constant `c` in `M`, the measure `μ` is invariant under scalar multiplication, i.e., for all `x` in `α`, `μ(cx) = μ(x)`.
|
MeasureTheory.smulInvariantMeasure_tfae
theorem MeasureTheory.smulInvariantMeasure_tfae :
∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : 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
The theorem `MeasureTheory.smulInvariantMeasure_tfae` establishes the equivalence of several definitions of a measure that is invariant under a multiplicative action of a group. The definitions are:
- `SMulInvariantMeasure G α μ`, which is a measure invariant under the scalar multiplication.
- For every scalar `c` from group `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`.
- Similarly, for every scalar `c` 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`. This is extended to any set, including non-measurable ones.
- For any scalar `c`, scalar multiplication by `c` maps the measure `μ` to itself.
- For any scalar `c`, scalar multiplication by `c` preserves the measure.
This theorem assures that all these definitions are equivalent, and any one of them can be used to determine if a measure is invariant under a multiplicative action of a group.
More concisely: The theorem `MeasureTheory.smulInvariantMeasure_tfae` in Lean 4 establishes the equivalence of a measure being invariant under scalar multiplication by a group element, the preimage and image measures under scalar multiplication being equal, and scalar multiplication preserving the measure.
|
MeasureTheory.NullMeasurableSet.smul
theorem MeasureTheory.NullMeasurableSet.smul :
∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : MeasurableSMul G α] {μ : MeasureTheory.Measure α}
[inst_4 : MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α},
MeasureTheory.NullMeasurableSet s μ → ∀ (c : G), MeasureTheory.NullMeasurableSet (c • s) μ
The theorem `MeasureTheory.NullMeasurableSet.smul` is a statement about measurable sets in measure theory. It states that for any given type `G` which is a group, type `α`, a measurable space `m` over type `α`, and a measure `μ` that is invariant under scaling by elements of `G`, if a set `s` of type `α` is a null measurable set with respect to `μ`, then for any element `c` of the group `G`, the scaled set `c • s` is also a null measurable set with respect to `μ`. In other words, null-measurable sets remain null-measurable even when scaled by any element of a group.
More concisely: If `s` is a null measurable set in the measurable space `(α, m)` with respect to the invariant measure `μ` over the group `G`, then for all `c` in `G`, the scaled set `c • s` is also a null measurable set in `(α, m)` with respect to `μ`.
|
MeasureTheory.measurePreserving_vadd
theorem MeasureTheory.measurePreserving_vadd :
∀ {M : Type v} {α : Type w} {m : MeasurableSpace α} [inst : MeasurableSpace M] [inst_1 : VAdd M α]
[inst : MeasurableVAdd M α] (c : M) (μ : MeasureTheory.Measure α)
[inst : MeasureTheory.VAddInvariantMeasure M α μ], MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ
This theorem states that for any type `M` and `α` with a measurable space `m` and `inst`, if `α` is endowed with the vector addition operation and `M` and `α` have the property of being measurable with respect to vector addition, then the measure `μ` is preserved under the translation operation by a constant `c`. In other words, the addition of a constant to every element in the set does not change the measure of the set, assuming that the measure is invariant under the vector addition operation.
More concisely: Given a measurable space `(M, Σ, m)` and a measurable type `α` with vector addition, if `μ: Σ → ℝ` is a measure invariant under vector addition, then for all `c ∈ α` and `A ∈ Σ`, we have `μ(A) = μ(A + c)`.
|
MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero
theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero :
∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : MeasurableVAdd G α] {μ : MeasureTheory.Measure α}
[inst_4 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_5 : TopologicalSpace α]
[inst_6 : ContinuousConstVAdd G α] [inst : AddAction.IsMinimal G α] {K U : Set α},
IsCompact K → ↑↑μ K ≠ 0 → IsOpen U → U.Nonempty → 0 < ↑↑μ U
The theorem `MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero` states that for any additive group `G` acting on a measurable space `α` with measure `μ`, if the measure `μ` is invariant under the group action and is nonzero on a compact set `K`, then it is positive on any nonempty open set `U`. In case of a regular measure, one can assume `μ ≠ 0` instead of `μ K ≠ 0`. This is crucial in the branch of Measure Theory, particularly when dealing with invariant measures under group actions. The theorem has additional conditions such as the continuity of the action and the minimality of the action, which are typically satisfied in standard settings.
More concisely: If `μ:` MeasurableSpace `α` → ℝ is a nonzero, group-invariant measure on a measurable space `α` with compact set `K,` and the group action on `α` is continuous and minimal, then `μ` is positive on any nonempty open set.
|
MeasureTheory.measure_smul
theorem MeasureTheory.measure_smul :
∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : MeasurableSMul G α] (c : G) (μ : MeasureTheory.Measure α)
[inst_4 : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α), ↑↑μ (c • s) = ↑↑μ s
The theorem `MeasureTheory.measure_smul` states that for any group `G` of type `u`, any type `w` `α`, any measurable space `α` denoted by `m`, given `G` has a group structure and `α` has a `G`-action, and a measurable space structure and the scalar multiplication is measurable, for any element `c` in `G`, any measure `μ` on `α`, and any set `s` in `α`, with the measure `μ` being `G`-smul invariant, the measure of the scalar multiple of the set `s` by `c` is equal to the measure of the set `s`. In mathematical terms, if a group action scales the measure of sets invariantly, then the measure of a set remains unchanged when it is scaled by any element of the group.
More concisely: For any measurable space `(α, m)` with a `G`-action preserving the measure `μ`, the measure of a `G`-invariant set `s` is equal to the measure of its scalar multiplication `cs` by any element `c` in `G`.
|
MeasureTheory.NullMeasurableSet.vadd
theorem MeasureTheory.NullMeasurableSet.vadd :
∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : MeasurableVAdd G α] {μ : MeasureTheory.Measure α}
[inst_4 : MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α},
MeasureTheory.NullMeasurableSet s μ → ∀ (c : G), MeasureTheory.NullMeasurableSet (c +ᵥ s) μ
The theorem `MeasureTheory.NullMeasurableSet.vadd` states that for any type `G` with an addition (`AddGroup`) operation, type `α` with a `MeasurableSpace` and an `AddAction` of `G` on `α`, and a set `s` of type `α`, if `s` is a null measurable set with respect to a measure `μ` which is invariant under the action of `G` (represented by `MeasureTheory.VAddInvariantMeasure`), then for any element `c` of type `G`, the translated set `c +ᵥ s` (representing the addition of `c` to every element of `s`) is also a null measurable set with respect to `μ`. This theorem essentially states that translation by a group element keeps null measurability property intact.
More concisely: If `s` is a null measurable set in the measurable space `(α, Σ, μ)` with respect to the invariant measure `μ` under the additive action of the group `G`, then for all `c` in `G`, the translated set `c + s` is also a null measurable set.
|
MeasureTheory.measure_vadd
theorem MeasureTheory.measure_vadd :
∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
[inst_2 : MeasurableSpace G] [inst_3 : MeasurableVAdd G α] (c : G) (μ : MeasureTheory.Measure α)
[inst_4 : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α), ↑↑μ (c +ᵥ s) = ↑↑μ s
This theorem, `MeasureTheory.measure_vadd`, states that for any given type `G`, type `α`, a measure space `m` of type `α`, an additive group structure on `G`, an action of the group `G` on the set `α`, a measurable space structure on `G`, a `MeasurableVAdd` structure which means that the action of `G` on `α` is measurable, a constant `c` of type `G`, a measure `μ` from the `MeasureTheory`, and the `VAddInvariantMeasure` structure which means that the measure `μ` is invariant under the action of `G`, then for any set `s` of type `α`, the measure of the set obtained by adding `c` to every element in `s` is the same as the measure of the set `s` itself. In the language of mathematics, this can be written as: if $G$ is a group acting on a set $α$ and $μ$ is a $G$-invariant measure on $α$, then for any $c∈G$ and any measurable set $s⊂α$, we have $μ(c + s) = μ(s)$.
More concisely: Given a group action on a measure space with a $G$-invariant measure, for any measurable set and constant in the group, the measure of the set translated by the constant is equal to the measure of the original set.
|