MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac
theorem MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α},
MeasureTheory.IsFundamentalDomain G s μ →
ν.AbsolutelyContinuous μ → (MeasureTheory.Measure.sum fun g => ν.restrict (g • s)) = ν
This theorem, "MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac", states that for any Group `G`, any type `α` under the action of `G`, any measurable space `α`, any set `s` of elements of type `α`, any measure `μ` on `α`, assuming `G` is a measurable space and has a measurable scalar multiplication with `α`, `μ` is a scalar multiplication invariant measure, and `G` is countable, then for any measure `ν` on `α`, if `s` is a fundamental domain of `μ` under the action of `G` and `ν` is absolutely continuous with respect to `μ`, then the sum of the measures `ν` restricted to the orbit of `s` under the action of `G` is equal to `ν`.
In simpler terms, if you have a measure that is absolutely continuous with respect to a measure that is invariant under a certain group action, then when you sum over the measures of the group-translated copies of a fundamental domain, you get back the original measure.
More concisely: If `G` is a countable measurable group acting on a measurable space `(α, μ)` with invariant measure `μ`, `s` is a fundamental domain, and `ν` is an absolutely continuous measure with respect to `μ`, then the sum of `ν` over the orbit of `s` under `G` equals `ν`.
|
MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum
theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), ↑↑μ t = ∑' (g : G), ↑↑μ ((g +ᵥ t) ∩ s)
This theorem, named `MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum`, asserts the following: for any additively group-structured type `G` and any type `α`, given that `G` is an additive action on `α`, `α` is a measurable space, `s` is a set in `α`, `μ` is a measure on `α`, `G` is a measurable space, `G` is measurably v-additive in `α`, `μ` is v-add invariant measure in `G` and `α`, and `G` is countable, if `s` is an additive fundamental domain of `G` with respect to `μ`, then for any set `t` in `α`, the measure of `t` is equal to the sum of the measures of the sets obtained by translating `t` by each element of `G` and taking the intersection with `s`. The theorem uses summation symbol ∑' to represent the summation over the countable set `G`.
More concisely: If `G` is a countable, measurably additive group acting on the measurable space `(α, μ)`, `s` is an additive fundamental domain of `G`, then for any set `t` in `α`, the measure of `t` equals the sum of the measures of `t ∩ s` for all translations `g ∈ G`.
|
MeasureTheory.IsFundamentalDomain.measure_eq
theorem MeasureTheory.IsFundamentalDomain.measure_eq :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → ↑↑μ s = ↑↑μ t
The theorem states that if `s` and `t` are two fundamental domains of the same action by a group `G` on a set `α`, then, under certain conditions, the measures of `s` and `t` are equal. These conditions include `G` being a group, `α` being a set equipped with a measurable space structure and a `G`-action, the measure `μ` of `α` being `smul` invariant, and `G` being countable. A fundamental domain here refers to a subset of `α` that contains exactly one representative for each orbit of the `G`-action.
More concisely: If `G` is a countable group acting on a measurable set `α` with a `μ`-finite, `smul` invariant measure `μ`, then any two fundamental domains `s` and `t` of this action have equal measures.
|
MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict
theorem MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsAddFundamentalDomain G s μ →
∀ {f : α → ENNReal}, (∀ (γ : G) (x : α), f (γ +ᵥ x) = f x) → essSup f (μ.restrict s) = essSup f μ
The theorem `MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict` states that, if a function `f` is invariant under the action of a countable additive group `G`, and `μ` is a `G`-invariant measure with a fundamental domain `s`, then the essential supremum of `f` when restricted to `s` is the same as that of `f` over its entire domain. In other words, the greatest value of `f` that occurs "almost everywhere" in `s` is the same as the greatest value of `f` that occurs "almost everywhere" in the whole domain. This fact holds true for all functions that are invariant under the action of a countable additive group, and for all `G`-invariant measures that have a fundamental domain.
More concisely: For a countable additive group-invariant function `f` and a `G`-invariant measure `μ` with fundamental domain `s`, the essential supremum of `f` over `s` equals the essential supremum of `f` over its entire domain.
|
MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac
theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α},
MeasureTheory.IsFundamentalDomain G s μ →
ν.AbsolutelyContinuous μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν
This theorem, `MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac`, states that for any types `G` and `α` where `G` is a group and `α` is a mul-action of `G`, and for any sets `s` of `α`, `μ` as a measure on `α`, and `ν` as another measure on `α`, if `s` is a fundamental domain of `G` with respect to `μ`, and `ν` is absolutely continuous with respect to `μ`, then for any function `f` from `α` to extended nonnegative real numbers, the integral of `f` with respect to `ν` is equal to the sum over all elements `g` in `G` of the integral of `f` over the set `g • s` with respect to `ν`. In the context of measure theory, this theorem establishes a relationship between an integral over a measure space and a sum over a group action, under certain conditions.
More concisely: If `G` is a group acting on a set `α` with measure `μ`, `ν` is an absolutely continuous measure on `α` with respect to `μ`, and `s` is a fundamental domain of `G` with respect to `μ`, then for any integrable function `f` on `α` with respect to `ν`, the integral of `f` with respect to `ν` is equal to the sum over all elements `g` in `G` of the integral of `f` over `g•s` with respect to `ν`.
|
MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd
theorem MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ],
MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.NullMeasurableSet (g +ᵥ s) μ
The theorem `MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd` states that for any type `G` (which forms an additive group) and any type `α` (which has a measurable space structure and on which `G` acts additively), if we have a set `s` in `α` that is an additive fundamental domain under measure `μ` (which is `VAddInvariantMeasure`), then for every element `g` in `G`, the translate of the set `s` by `g` is a null measurable set under the same measure `μ`. Here, a set being null measurable means it can be approximated by a measurable set up to a set of null measure.
More concisely: For any additive group G acting additively on a measurable space (α, μ) with VAddInvariantMeasure μ, an additive fundamental domain s in α is null measurable for every translate g \* s.
|
MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq
theorem MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsAddFundamentalDomain G s μ →
MeasureTheory.NullMeasurableSet t μ → ↑↑μ s < ↑↑μ t → ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 0 ∧ g +ᵥ x = y
The theorem states that given a countable group `G` that performs an additive action on a set `α` (in a measurable space) which admits an invariant measure `μ`, and a "fundamental domain" `s` under this action, if we have another set `t` (in the same measurable space) that is null-measurable and its measure is strictly larger than the measure of `s`, then there must exist two distinct points `x` and `y` in `t` such that the result of the additive action of a non-zero element `g` of `G` on `x` yields `y`. This emphasizes the connection between measures, additive actions, and the concept of a fundamental domain.
More concisely: Given a countable group acting additively on a measurable set with an invariant measure and a null-measurable set of strictly larger measure containing distinct points `x` and `y`, there exists a non-zero group element `g` such that `y = g(x)`.
|
MeasureTheory.IsFundamentalDomain.mk''
theorem MeasureTheory.IsFundamentalDomain.mk'' :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.NullMeasurableSet s μ →
(∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s) →
(∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) →
(∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) →
MeasureTheory.IsFundamentalDomain G s μ
This theorem states that for a set `s` to be a fundamental domain with respect to a group `G` acting on a type `α` (via multiplication, denoted as `MulAction G α`), it is sufficient to satisfy the following conditions:
1. The set `s` is null-measurable with respect to a measure `μ` (denoted as `MeasureTheory.NullMeasurableSet s μ`). This means that set `s` can be approximated by a measurable set up to a set of null measure.
2. Almost every element `x` of the space `α` (with respect to the measure `μ`) has a corresponding group element `g` such that `g • x` belongs to the set `s` (denoted as `∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s`).
3. For every group element `g` that is not the identity (`g ≠ 1`), the set `g • s` (i.e., the result of the group action on the set `s`) and the set `s` are almost everywhere disjoint with respect to the measure `μ` (denoted as `MeasureTheory.AEDisjoint μ (g • s) s`). This means their intersection has measure zero.
4. For every group element `g`, the function that maps `x` to `g • x` preserves the measure `μ` quasi everywhere (denoted as `MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ`).
If these conditions are met, then set `s` is a fundamental domain with respect to group `G` and measure `μ` (denoted as `MeasureTheory.IsFundamentalDomain G s μ`).
More concisely: A set `s` is a fundamental domain for a group `G` action on a type `α` with respect to a measure `μ` if it is null-measurable, almost every element of `α` has exactly one group element mapping to it in `s`, and for all non-identity group elements `g`, the sets `g • s` and `s` are almost everywhere disjoint and the group action preserves the measure quasi-everywhere.
|
MeasureTheory.IsFundamentalDomain.mk'
theorem MeasureTheory.IsFundamentalDomain.mk' :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.NullMeasurableSet s μ → (∀ (x : α), ∃! g, g • x ∈ s) → MeasureTheory.IsFundamentalDomain G s μ
This theorem states that for any given group `G`, any type `α` with a `MulAction` of `G` on `α`, a `MeasurableSpace` structure on `α`, a set `s` of type `α`, and a measure `μ` on `α`, if `s` is a `NullMeasurableSet` with respect to `μ`, and for each element `x` of `α` there exists exactly one group element `g` such that the element `g • x` belongs to `s`, then `s` is a fundamental domain for the action of `G` on `α`. This means `s` is a set that contains exactly one element from each orbit of the group action, and it can be approximated by a measurable set up to a set of null measure.
More concisely: If a null measurable set `s` in a group action on a measurable space with a measure has exactly one element from each orbit, then `s` is a fundamental domain for the action.
|
MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self
theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] [inst_7 : Finite G],
MeasureTheory.IsAddFundamentalDomain G s μ →
∀ (t : Set α), (∀ (g : G), μ.ae.EventuallyEq (g +ᵥ t) t) → ↑↑μ t = Nat.card G • ↑↑μ (t ∩ s)
This theorem states that given a measure space with an action of a finite additive group `G`, the measure of any `G`-invariant set is determined by the measure of its intersection with a fundamental domain for the action of `G`. Specifically, for any set `t` that remains equal almost everywhere under the action of any element of `G`, the measure of `t` is equal to the cardinality of `G` times the measure of the intersection of `t` and `s`, where `s` is a set that forms a fundamental domain under the action of `G` in the measure space.
More concisely: Given a measure space with a finite additive `G`-action, the measure of any `G`-invariant set is equal to the cardinality of `G` times the measure of its intersection with a fundamental domain.
|
MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint
theorem MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsAddFundamentalDomain G s μ →
MeasureTheory.NullMeasurableSet t μ →
Pairwise (MeasureTheory.AEDisjoint μ on fun g => (g +ᵥ t) ∩ s) → ↑↑μ t ≤ ↑↑μ s
This theorem states that if a countable additive group `G` has an invariant measure `μ` with a fundamental domain `s`, then for every null-measurable set `t`, if `g +ᵥ t ∩ s` are pairwise almost everywhere-disjoint (i.e., pairs of these sets intersect on sets of measure zero), then the measure of `t` is at most the measure of `s`. In other words, if a group action has a measurable set `s` that is representative (a fundamental domain), then any set `t` that doesn't over-count intersection within `s` when translated by elements of `G`, cannot have a larger measure than `s` under the group-invariant measure `μ`.
More concisely: If a countable additive group `G` acts on a measurable set `s` with invariant measure `μ`, and for every null-measurable set `t`, the translated sets `g + t ∩ s` are pairwise almost everywhere-disjoint, then `μ(t) ≤ μ(s)`.
|
MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul
theorem MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ],
MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.NullMeasurableSet (g • s) μ
This theorem states that if a set `s` of elements of type `α` forms a fundamental domain under a group `G` with respect to a measure `μ`, then for any element `g` of the group `G`, the set resulting from the operation `g • s` (which represents the action of `g` on `s`) is a null-measurable set with respect to measure `μ`. Here, a null-measurable set means a set that can be approximated by a measurable set up to a set of null measure. The group `G` is endowed with a group action on `α`, a measurable space structure, and a structure of a `smul` invariant measure. The type `α` is also equipped with a measurable space structure and the property of being measurable with respect to the group action `smul`.
More concisely: If a set `s` forms a fundamental domain under a group `G` action on measurable space `(α, μ)` with `α` being measurable with respect to `G`, then for all `g` in `G`, `g • s` is a null-measurable set with respect to `μ`.
|
MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le
theorem MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : Countable G],
MeasureTheory.NullMeasurableSet s μ →
(∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) →
(∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) →
↑↑μ Set.univ ≤ ∑' (g : G), ↑↑μ (g +ᵥ s) → MeasureTheory.IsAddFundamentalDomain G s μ
This theorem states that, given a measurable space with a finite measure `μ` and a countable additive group `G` acting in a way that quasi-preserves the measure, a set `s` can be established as a fundamental domain by satisfying a few conditions. Specifically, if `s` is a null measurable set under `μ` and the sets resulting from adding an element `g` from `G` to `s` (denoted `g +ᵥ s`) are almost everywhere disjoint with `s` for non-zero `g`, and if the action of adding `g` to `x` (denoted `g +ᵥ x`) quasi-preserves the measure under `μ`, and the measure of the universal set is less than or equal to the sum of the measures of the sets `g +ᵥ s` over all `g` in `G`—then `s` is a fundamental domain under the additive action of `G` with respect to the measure `μ`.
More concisely: Given a measurable space with a finite measure and a countable additive group acting quasi-preservingly, a null measurable set `s` is a fundamental domain if it is almost everywhere disjoint with the sets `g +ᵥ s` for non-zero `g`, and the measure of the union of `g +ᵥ s` equals the measure of the universal set for all `g` in the group.
|
MeasureTheory.IsAddFundamentalDomain.measure_eq
theorem MeasureTheory.IsAddFundamentalDomain.measure_eq :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s t : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → ↑↑μ s = ↑↑μ t
This theorem asserts that if `s` and `t` are two fundamental domains of the same additive group action, then they have equal measures. More specifically, for any type `G` that forms an additive group, and another type `α` equipped with an action of `G` and a measurable space structure, if `s` and `t` are sets of `α` and `μ` is a measure on `α`, and given that `G` forms a measurable space, `α` has a vadd measurable structure with respect to `G` and `μ` is vadd invariant under the action of `G` and `G` is countable, then if `s` and `t` are fundamental domains under the additive action of `G` with respect to the measure `μ`, the measures of `s` and `t` with respect to `μ` are equal.
More concisely: If `s` and `t` are fundamental domains of the same additive group action on a measurable space `(α, μ)` with respect to a countable additive group `G`, where `μ` is a vadd invariant measure, then the measures of `s` and `t` are equal.
|
MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq
theorem MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsFundamentalDomain G s μ →
MeasureTheory.NullMeasurableSet t μ → ↑↑μ s < ↑↑μ t → ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 1 ∧ g • x = y
The theorem states that if a countable group `G` has an invariant measure `μ` with a fundamental domain `s`, then any null-measurable set `t` whose measure is strictly greater than the measure of `s` must contain two distinct points `x` and `y` such that there exists an element `g` in `G` (which is not the identity element) that satisfies the equation `g • x = y`. In other words, in the context of measure theory, it asserts that if a group action has a set of a certain measure, any larger null-measurable set must have some symmetry under the group action.
More concisely: If a countable group `G` acts on a measure space with an invariant measure `μ` and has a fundamental domain `s` of finite measure, then any null-measurable set of strictly greater measure contains distinct points `x` and `y` such that there exists a non-identity `g` in `G` with `g • x = y`.
|
MeasureTheory.IsAddFundamentalDomain.mk'
theorem MeasureTheory.IsAddFundamentalDomain.mk' :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.NullMeasurableSet s μ →
(∀ (x : α), ∃! g, g +ᵥ x ∈ s) → MeasureTheory.IsAddFundamentalDomain G s μ
This theorem, `MeasureTheory.IsAddFundamentalDomain.mk'`, states that for any type `G` that forms an additive group, another type `α` with an additive action of `G` on `α`, a measurable space structure on `α`, a set `s` of type `α`, and a measure `μ` of type `α`, if `s` is a null measurable set according to `μ`, and for each element `x` of type `α`, there exists exactly one element `g` of type `G` such that the sum of `g` and `x` belongs to `s`, then `s` is a fundamental domain for the additive action of `G` on `α` with respect to the measure `μ`. In other words, the theorem relates the concept of fundamental domains to the uniqueness of representation in terms of the additive action, in the context of measure theory.
More concisely: If a null measurable set `s` in an additive group `α` with an additive action of another additive group `G`, and a measure `μ`, has the property that for each `x` in `α`, there exists exactly one `g` in `G` such that `g + x` belongs to `s`, then `s` is a fundamental domain for the additive action of `G` on `α` with respect to the measure `μ`.
|
MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self
theorem MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G] [inst_7 : Finite G],
MeasureTheory.IsFundamentalDomain G s μ →
∀ (t : Set α), (∀ (g : G), μ.ae.EventuallyEq (g • t) t) → ↑↑μ t = Nat.card G • ↑↑μ (t ∩ s)
The theorem `MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self` states that given a measure space with an action of a finite group `G`, the measure of any `G`-invariant set is determined by the measure of its intersection with a fundamental domain for the action of `G`. In other words, for any set `t` that is invariant under the action of any element `g` of `G` (i.e., the set `t` is such that for each `g`, `g` acting on `t` is almost everywhere equal to `t`), the measure of `t` is equal to the cardinality of `G` times the measure of the intersection of `t` and `s`, where `s` is a fundamental domain for the action of `G`. Here, `Nat.card G` denotes the cardinality of the finite group `G` as a natural number, and `•` denotes the action of `G` on the set `t`.
More concisely: Given a measure space with a finite group action, the measure of any invariant set is equal to the cardinality of the group times the measure of its intersection with a fundamental domain.
|
MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint
theorem MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsFundamentalDomain G s μ →
MeasureTheory.NullMeasurableSet t μ →
Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • t ∩ s) → ↑↑μ t ≤ ↑↑μ s
This theorem states that given a countable group `G` acting on a set `α`, if this action admits an invariant measure `μ` with a fundamental domain `s`, then for any null-measurable set `t`, if the sets formed by the intersection of the action of each group element on `t` with `s` are pairwise almost everywhere disjoint, then the measure of `t` is at most the measure of `s`. In other words, if the actions of the group on `t` don't overlap too much within the fundamental domain `s`, then `t` cannot have a larger measure than `s`.
More concisely: Given a countable group `G` acting on a measure space `(α, μ)` with an invariant measure `μ` and fundamental domain `s`, if for any null-measurable `t`, the intersections of `t` with the actions of group elements are pairwise almost everywhere disjoint, then the measure of `t` is at most the measure of `s`.
|
MeasureTheory.IsFundamentalDomain.measure_eq_tsum
theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), ↑↑μ t = ∑' (g : G), ↑↑μ (g • t ∩ s)
This theorem states that for any given types 'G' and 'α', where 'G' is a group with a multiplication action on 'α', and 'α' is equipped with a measurable space structure, along with a set 's' of type 'α' and a measure 'μ' on 'α'. Further, 'G' is also equipped with a measurable space structure and a measurable scalar multiplication operation, and 'μ' is assumed to be a scalar multiplication-invariant measure on 'α' under the action of 'G', with 'G' being countable. Under these conditions, the theorem asserts that if 's' is a fundamental domain for the action of 'G' on 'α' with respect to the measure 'μ', then for any set 't' of type 'α', the measure of 't' is equal to the sum of the measures of the intersections of 't' acted on by elements 'g' of 'G' and the set 's'. The sum is over all elements 'g' in 'G'.
More concisely: If 'G' is a countable group acting measurably on measurable space ('α', μ) with 's' as a fundamental domain, then for any measurable set 't', the measure of 't' equals the sum of measures of intersections 't ∩ g(s)' over all elements 'g' in 'G'.
|
MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac
theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α},
MeasureTheory.IsAddFundamentalDomain G s μ →
ν.AbsolutelyContinuous μ → (MeasureTheory.Measure.sum fun g => ν.restrict (g +ᵥ s)) = ν
This theorem, "MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac", states that for any Additive Group `G` and type `α`, given an action of `G` on `α`, a measurable space structure on `α`, a set `s` of type `α`, a measure `μ` on `α`, a measurable space structure on `G`, a measurable addition structure on `α` with `G`, a `G`-additive invariant measure `μ` on `α`, a countability on `G`, and another measure `ν` on `α`, if `s` is an additive fundamental domain of `G` with respect to measure `μ` and if measure `ν` is absolutely continuous with respect to measure `μ`, then the sum of the measures `ν` restricted to `g +ᵥ s` for all `g` in `G` is equal to the measure `ν`. Here, `g +ᵥ s` denotes the `G`-action on `s`.
More concisely: For any additive group `G`, measurable space `α`, action of `G` on `α`, measurable space structure, additive invariant measure `μ` on `α` (countable `G`), measurable addition structure, measurable space structure on `G`, and measures `μ` and `ν` on `α` with `μ` being `G`-invariant and `ν` absolutely continuous with respect to `μ`, if `s` is an additive fundamental domain of `G` with respect to `μ`, then the sum of `ν` restricted to `g + s` for all `g` in `G` equals `ν`.
|
MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le
theorem MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : Countable G],
MeasureTheory.NullMeasurableSet s μ →
(∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) →
(∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) →
↑↑μ Set.univ ≤ ∑' (g : G), ↑↑μ (g • s) → MeasureTheory.IsFundamentalDomain G s μ
The theorem `MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le` states that for a given group `G` acting on a measurable space `α` via a quasi-measure-preserving action, if we have a set `s` in `α` such that it is null-measurable with respect to a finite measure `μ`, and for each element `g` in `G` (excluding the identity), the translates `g • s` are almost everywhere disjoint from `s`; moreover, if the measure of the universal set is less than or equal to the sum of the measures of the translates `g • s` over all `g` in `G`, then `s` is a fundamental domain for the action of `G` with respect to the measure `μ`. In terms of group theory, `s` serves as a 'tile' that can cover the entire space `α` up to sets of measure zero, and the elements of `G` can be seen as the 'shifts' or 'translations' of this 'tile.
More concisely: If a null-measurable, set `s` in a measurable space `α` with respect to a finite measure `μ` and whose translates under a group `G`'s quasi-measure-preserving action are almost everywhere disjoint from `s`, is such that the measure of `α` is less than or equal to the sum of the measures of the translates `g • s` for all non-identity `g` in `G`, then `s` is a fundamental domain for the `G` action on `α` with respect to `μ`.
|
MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac
theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableVAdd G α]
[inst_5 : MeasureTheory.VAddInvariantMeasure G α μ] [inst_6 : Countable G] {ν : MeasureTheory.Measure α},
MeasureTheory.IsAddFundamentalDomain G s μ →
ν.AbsolutelyContinuous μ → ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂ν
The theorem `MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac` states the following: Given a type `G` with an additive group structure, a type `α` with a measurable space structure, an `AddAction` of `G` on `α`, a measurable addition operation (`MeasurableVAdd`) between `G` and `α`, a measure `μ` on `α` that is invariant under the action of `G` (`MeasureTheory.VAddInvariantMeasure`), a countable set `G`, a set `s` of `α`, and another measure `ν` on `α`, if `s` is an additive fundamental domain for `G` under the measure `μ` and the measure `ν` is absolutely continuous with respect to `μ`, then for any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), the integral of `f` with respect to `ν` equals the sum over all `g` in `G` of the integral of `f` over the set `g + s` with respect to `ν`. In mathematical terms, $\int f d\nu = \sum_{g \in G} \int_{g + s} f d\nu$.
More concisely: Given a measurable space `(α, Σ, μ)`, a group `G` acting measurably on `α` with invariant measure `μ`, an absolutely continuous measure `ν` on `α` with respect to `μ`, and an additive fundamental domain `s` for `G` under `μ`, for any measurable function `f` from `α` to the extended nonnegative real numbers, the integral of `f` with respect to `ν` equals the sum of the integrals of `f` over `g+s` for all `g` in `G` with respect to `ν`. In symbols, $\int f d\nu = \sum\_{g \in G} \int\_{g+s} f d\nu$.
|
MeasureTheory.IsFundamentalDomain.essSup_measure_restrict
theorem MeasureTheory.IsFundamentalDomain.essSup_measure_restrict :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
{μ : MeasureTheory.Measure α} [inst_3 : MeasurableSpace G] [inst_4 : MeasurableSMul G α]
[inst_5 : MeasureTheory.SMulInvariantMeasure G α μ] [inst_6 : Countable G],
MeasureTheory.IsFundamentalDomain G s μ →
∀ {f : α → ENNReal}, (∀ (γ : G) (x : α), f (γ • x) = f x) → essSup f (μ.restrict s) = essSup f μ
This theorem states that if a function `f` is invariant under the action of a countable group `G`, and a measure `μ` is also invariant under the same group's action with a fundamental domain `s`, then the essential supremum (`essSup`) of `f` when restricted to `s` is the same as the essential supremum of `f` on its entire domain. In other words, the largest value that `f` takes on almost everywhere in `s` is the same as the largest value it takes on almost everywhere in its entire domain. This is under the condition that for every element `γ` in group `G` and every element `x` in the domain of `f`, the value of `f` at `γ • x` (the action of `γ` on `x`) is equal to the value of `f` at `x`.
More concisely: If a function `f` is invariant under the action of a countable group `G`, and `μ` is a measure invariant under `G` with a fundamental domain `s`, then the essential supremum of `f` on `s` equals the essential supremum of `f` on its entire domain.
|
MeasureTheory.IsAddFundamentalDomain.mk''
theorem MeasureTheory.IsAddFundamentalDomain.mk'' :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
{s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.NullMeasurableSet s μ →
(∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s) →
(∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) →
(∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) →
MeasureTheory.IsAddFundamentalDomain G s μ
This theorem states that, for a set `s` to be considered a fundamental domain with regards to addition in a given measure space, four conditions must be satisfied. These conditions are as follows:
1. The set `s` is a null measurable set under some measure `μ`.
2. Almost every element `x` in the measure space can have an element `g` added to it such that `g + x` is in `s`.
3. For every non-zero element `g`, the set `g + s` (which is the set obtained by adding `g` to every element in `s`) and `s` are almost everywhere disjoint under the measure `μ`. In other words, their intersection has measure zero.
4. For every element `g`, the function that adds `g` to every element is quasi measure preserving under the measure `μ`. This means that the function does not change the measure of sets by much.
In the context of Group Theory, `G` is a group under addition, and `α` is a set on which `G` acts. If these conditions are satisfied, then `s` is considered an additive fundamental domain of `G` under the measure `μ`.
More concisely: A set `s` is an additive fundamental domain of a group `G` under a measure `μ` if it is a null measurable set, almost every element `x` has a group element `g` such that `g + x` is in `s` and the sets `g + s` and `s` have measure zero intersection for all non-zero `g`, and the group action is quasi measure preserving.
|