# Fundamental domain of a group action #

A set s is said to be a fundamental domain of an action of a group G on a measurable space α with respect to a measure μ if

• s is a measurable set;

• the sets g • s over all g : G cover almost all points of the whole space;

• the sets g • s, are pairwise a.e. disjoint, i.e., μ (g₁ • s ∩ g₂ • s) = 0 whenever g₁ ≠ g₂; we require this for g₂ = 1 in the definition, then deduce it for any two g₁ ≠ g₂.

In this file we prove that in case of a countable group G and a measure preserving action, any two fundamental domains have the same measure, and for a G-invariant function, its integrals over any two fundamental domains are equal to each other.

We also generate additive versions of all theorems in this file using the to_additive attribute.

• We define the HasFundamentalDomain typeclass, in particular to be able to define the covolume of a quotient of α by a group G, which under reasonable conditions does not depend on the choice of fundamental domain.

• We define the QuotientMeasureEqMeasurePreimage typeclass to describe a situation in which a measure μ on α ⧸ G can be computed by taking a measure ν on α of the intersection of the pullback with a fundamental domain.

## Main declarations #

• MeasureTheory.IsFundamentalDomain: Predicate for a set to be a fundamental domain of the action of a group
• MeasureTheory.fundamentalFrontier: Fundamental frontier of a set under the action of a group. Elements of s that belong to some other translate of s.
• MeasureTheory.fundamentalInterior: Fundamental interior of a set under the action of a group. Elements of s that do not belong to any other translate of s.
structure MeasureTheory.IsAddFundamentalDomain (G : Type u_1) {α : Type u_2} [Zero G] [VAdd G α] [] (s : Set α) (μ : ) :

A measurable set s is a fundamental domain for an additive action of an additive group G on a measurable space α with respect to a measure α if the sets g +ᵥ s, g : G, are pairwise a.e. disjoint and cover the whole space.

• nullMeasurableSet :
• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x s
• aedisjoint : Pairwise ( on fun (g : G) => g +ᵥ s)
Instances For
theorem MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet {G : Type u_1} {α : Type u_2} [Zero G] [VAdd G α] [] {s : Set α} {μ : } (self : ) :
theorem MeasureTheory.IsAddFundamentalDomain.ae_covers {G : Type u_1} {α : Type u_2} [Zero G] [VAdd G α] [] {s : Set α} {μ : } (self : ) :
∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x s
theorem MeasureTheory.IsAddFundamentalDomain.aedisjoint {G : Type u_1} {α : Type u_2} [Zero G] [VAdd G α] [] {s : Set α} {μ : } (self : ) :
Pairwise ( on fun (g : G) => g +ᵥ s)
structure MeasureTheory.IsFundamentalDomain (G : Type u_1) {α : Type u_2} [One G] [SMul G α] [] (s : Set α) (μ : ) :

A measurable set s is a fundamental domain for an action of a group G on a measurable space α with respect to a measure α if the sets g • s, g : G, are pairwise a.e. disjoint and cover the whole space.

• nullMeasurableSet :
• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g x s
• aedisjoint : Pairwise ( on fun (g : G) => g s)
Instances For
theorem MeasureTheory.IsFundamentalDomain.nullMeasurableSet {G : Type u_1} {α : Type u_2} [One G] [SMul G α] [] {s : Set α} {μ : } (self : ) :
theorem MeasureTheory.IsFundamentalDomain.ae_covers {G : Type u_1} {α : Type u_2} [One G] [SMul G α] [] {s : Set α} {μ : } (self : ) :
∀ᵐ (x : α) ∂μ, ∃ (g : G), g x s
theorem MeasureTheory.IsFundamentalDomain.aedisjoint {G : Type u_1} {α : Type u_2} [One G] [SMul G α] [] {s : Set α} {μ : } (self : ) :
Pairwise ( on fun (g : G) => g s)
theorem MeasureTheory.IsAddFundamentalDomain.mk' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h_meas : ) (h_exists : ∀ (x : α), ∃! g : G, g +ᵥ x s) :

If for each x : α, exactly one of g +ᵥ x, g : G, belongs to a measurable set s, then s is a fundamental domain for the additive action of G on α.

theorem MeasureTheory.IsFundamentalDomain.mk' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h_meas : ) (h_exists : ∀ (x : α), ∃! g : G, g x s) :

If for each x : α, exactly one of g • x, g : G, belongs to a measurable set s, then s is a fundamental domain for the action of G on α.

theorem MeasureTheory.IsAddFundamentalDomain.mk'' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h_meas : ) (h_ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x s) (h_ae_disjoint : ∀ (g : G), g 0MeasureTheory.AEDisjoint μ (g +ᵥ s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ) :

For s to be a fundamental domain, it's enough to check MeasureTheory.AEDisjoint (g +ᵥ s) s for g ≠ 0.

theorem MeasureTheory.IsFundamentalDomain.mk'' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h_meas : ) (h_ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g x s) (h_ae_disjoint : ∀ (g : G), g 1MeasureTheory.AEDisjoint μ (g s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g x) μ μ) :

For s to be a fundamental domain, it's enough to check MeasureTheory.AEDisjoint (g • s) s for g ≠ 1.

theorem MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] (h_meas : ) (h_ae_disjoint : ∀ (g : G), g 0MeasureTheory.AEDisjoint μ (g +ᵥ s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ) (h_measure_univ_le : μ Set.univ ∑' (g : G), μ (g +ᵥ s)) :

If a measurable space has a finite measure μ and a countable additive group G acts quasi-measure-preservingly, then to show that a set s is a fundamental domain, it is sufficient to check that its translates g +ᵥ s are (almost) disjoint and that the sum ∑' g, μ (g +ᵥ s) is sufficiently large.

theorem MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] (h_meas : ) (h_ae_disjoint : ∀ (g : G), g 1MeasureTheory.AEDisjoint μ (g s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g x) μ μ) (h_measure_univ_le : μ Set.univ ∑' (g : G), μ (g s)) :

If a measurable space has a finite measure μ and a countable group G acts quasi-measure-preservingly, then to show that a set s is a fundamental domain, it is sufficient to check that its translates g • s are (almost) disjoint and that the sum ∑' g, μ (g • s) is sufficiently large.

theorem MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h : ) :
⋃ (g : G), g +ᵥ s =ᵐ[μ] Set.univ
abbrev MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq.match_1 {G : Type u_1} {α : Type u_2} [] [] {s : Set α} :
∀ (x : α) (motive : (∃ (g : G), g +ᵥ x s)Prop) (x_1 : ∃ (g : G), g +ᵥ x s), (∀ (g : G) (hg : g +ᵥ x s), motive )motive x_1
Equations
• =
Instances For
theorem MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h : ) :
⋃ (g : G), g s =ᵐ[μ] Set.univ
theorem MeasureTheory.IsAddFundamentalDomain.measure_ne_zero {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] (hμ : μ 0) (h : ) :
μ s 0
theorem MeasureTheory.IsFundamentalDomain.measure_ne_zero {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] (hμ : μ 0) (h : ) :
μ s 0
theorem MeasureTheory.IsAddFundamentalDomain.mono {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h : ) {ν : } (hle : ν.AbsolutelyContinuous μ) :
theorem MeasureTheory.IsFundamentalDomain.mono {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } (h : ) {ν : } (hle : ν.AbsolutelyContinuous μ) :
theorem MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] {s : Set α} {μ : } {ν : } (h : ) {f : βα} (hf : ) {e : GH} (he : ) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g +ᵥ x) fun (x : α) => g +ᵥ x) :
abbrev MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv.match_1 {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set α} {f : βα} (x : β) (motive : (∃ (g : G), g +ᵥ f x s)Prop) :
∀ (x_1 : ∃ (g : G), g +ᵥ f x s), (∀ (g : G) (hg : g +ᵥ f x s), motive )motive x_1
Equations
• =
Instances For
theorem MeasureTheory.IsFundamentalDomain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] {s : Set α} {μ : } {ν : } (h : ) {f : βα} (hf : ) {e : GH} (he : ) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g x) fun (x : α) => g x) :
theorem MeasureTheory.IsAddFundamentalDomain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] {s : Set α} {μ : } {ν : } (h : ) (f : α β) (hf : MeasureTheory.Measure.QuasiMeasurePreserving (f.symm) ν μ) (e : H G) (hef : ∀ (g : H), Function.Semiconj (f) (fun (x : α) => e g +ᵥ x) fun (x : β) => g +ᵥ x) :
theorem MeasureTheory.IsFundamentalDomain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] {s : Set α} {μ : } {ν : } (h : ) (f : α β) (hf : MeasureTheory.Measure.QuasiMeasurePreserving (f.symm) ν μ) (e : H G) (hef : ∀ (g : H), Function.Semiconj (f) (fun (x : α) => e g x) fun (x : β) => g x) :
theorem MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) :
Pairwise fun (g₁ g₂ : G) => MeasureTheory.AEDisjoint ν (g₁ +ᵥ s) (g₂ +ᵥ s)
theorem MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) :
Pairwise fun (g₁ g₂ : G) => MeasureTheory.AEDisjoint ν (g₁ s) (g₂ s)
theorem MeasureTheory.IsAddFundamentalDomain.vadd_of_comm {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } {G' : Type u_6} [AddGroup G'] [AddAction G' α] [] [] [] [VAddCommClass G' G α] (h : ) (g : G') :
theorem MeasureTheory.IsFundamentalDomain.smul_of_comm {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } {G' : Type u_6} [Group G'] [MulAction G' α] [] [] [] [SMulCommClass G' G α] (h : ) (g : G') :
theorem MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] (h : ) (g : G) :
theorem MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] (h : ) (g : G) :
theorem MeasureTheory.IsAddFundamentalDomain.restrict_restrict {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] (h : ) (g : G) (t : Set α) :
(μ.restrict t).restrict (g +ᵥ s) = μ.restrict ((g +ᵥ s) t)
theorem MeasureTheory.IsFundamentalDomain.restrict_restrict {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] (h : ) (g : G) (t : Set α) :
(μ.restrict t).restrict (g s) = μ.restrict (g s t)
theorem MeasureTheory.IsAddFundamentalDomain.vadd {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] (h : ) (g : G) :
theorem MeasureTheory.IsFundamentalDomain.smul {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] (h : ) (g : G) :
theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) :
(MeasureTheory.Measure.sum fun (g : G) => ν.restrict (g +ᵥ s)) = ν
theorem MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) :
(MeasureTheory.Measure.sum fun (g : G) => ν.restrict (g s)) = ν
theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) (f : αENNReal) :
∫⁻ (x : α), f xν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f xν
theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) (f : αENNReal) :
∫⁻ (x : α), f xν = ∑' (g : G), ∫⁻ (x : α) in g s, f xν
theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) :
(MeasureTheory.Measure.sum fun (g : G) => μ.restrict (g +ᵥ s)) = μ
theorem MeasureTheory.IsFundamentalDomain.sum_restrict {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) :
(MeasureTheory.Measure.sum fun (g : G) => μ.restrict (g s)) = μ
theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) :
∫⁻ (x : α), f xμ = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f xμ
theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) :
∫⁻ (x : α), f xμ = ∑' (g : G), ∫⁻ (x : α) in g s, f xμ
theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) :
∫⁻ (x : α), f xμ = ∑' (g : G), ∫⁻ (x : α) in s, f (-g +ᵥ x)μ
theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) :
∫⁻ (x : α), f xμ = ∑' (g : G), ∫⁻ (x : α) in s, f (g⁻¹ x)μ
theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) :
∫⁻ (x : α), f xμ = ∑' (g : G), ∫⁻ (x : α) in s, f (g +ᵥ x)μ
theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) :
∫⁻ (x : α), f xμ = ∑' (g : G), ∫⁻ (x : α) in s, f (g x)μ
theorem MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) (t : Set α) :
∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in t (g +ᵥ s), f xμ
theorem MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) (t : Set α) :
∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in t g s, f xμ
@[deprecated MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum]
theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) (t : Set α) :
∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in t g s, f xμ

Alias of MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum.

theorem MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) (t : Set α) :
∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) s, f (-g +ᵥ x)μ
theorem MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) (t : Set α) :
∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in g t s, f (g⁻¹ x)μ
@[deprecated MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum']
theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (f : αENNReal) (t : Set α) :
∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in g t s, f (g⁻¹ x)μ

Alias of MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum'.

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) (t : Set α) :
ν t = ∑' (g : G), ν (t (g +ᵥ s))
theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } (h : ) (hν : ν.AbsolutelyContinuous μ) (t : Set α) :
ν t = ∑' (g : G), ν (t g s)
theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (t : Set α) :
μ t = ∑' (g : G), μ (t (g +ᵥ s))
theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum' {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (t : Set α) :
μ t = ∑' (g : G), μ (t g s)
theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (t : Set α) :
μ t = ∑' (g : G), μ ((g +ᵥ t) s)
theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (t : Set α) :
μ t = ∑' (g : G), μ (g t s)
theorem MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (t : Set α) (ht : ∀ (g : G), g +ᵥ t = t) (hts : μ (t s) = 0) :
μ t = 0
theorem MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (h : ) (t : Set α) (ht : ∀ (g : G), g t = t) (hts : μ (t s) = 0) :
μ t = 0
theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (t : Set α) (ht : ∀ (g : G), g +ᵥ t =ᵐ[μ] t) :
μ t = μ (t s)

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.

theorem MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (t : Set α) (ht : ∀ (g : G), g t =ᵐ[μ] t) :
μ t = μ (t s)

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.

theorem MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) (f : αENNReal) (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in t, f xμ
theorem MeasureTheory.IsFundamentalDomain.setLIntegral_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) (f : αENNReal) (hf : ∀ (g : G) (x : α), f (g x) = f x) :
∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in t, f xμ
@[deprecated MeasureTheory.IsFundamentalDomain.setLIntegral_eq]
theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) (f : αENNReal) (hf : ∀ (g : G) (x : α), f (g x) = f x) :
∫⁻ (x : α) in s, f xμ = ∫⁻ (x : α) in t, f xμ

Alias of MeasureTheory.IsFundamentalDomain.setLIntegral_eq.

theorem MeasureTheory.IsAddFundamentalDomain.measure_set_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) {A : Set α} (hA₀ : ) (hA : ∀ (g : G), (fun (x : α) => g +ᵥ x) ⁻¹' A = A) :
μ (A s) = μ (A t)
theorem MeasureTheory.IsFundamentalDomain.measure_set_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) {A : Set α} (hA₀ : ) (hA : ∀ (g : G), (fun (x : α) => g x) ⁻¹' A = A) :
μ (A s) = μ (A t)
theorem MeasureTheory.IsAddFundamentalDomain.measure_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) :
μ s = μ t

If s and t are two fundamental domains of the same action, then their measures are equal.

theorem MeasureTheory.IsFundamentalDomain.measure_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) :
μ s = μ t

If s and t are two fundamental domains of the same action, then their measures are equal.

theorem MeasureTheory.IsAddFundamentalDomain.aEStronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] {β : Type u_6} [] (hs : ) (ht : ) {f : αβ} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
theorem MeasureTheory.IsFundamentalDomain.aEStronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] {β : Type u_6} [] (hs : ) (ht : ) {f : αβ} (hf : ∀ (g : G) (x : α), f (g x) = f x) :
theorem MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) {f : αE} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
theorem MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) {f : αE} (hf : ∀ (g : G) (x : α), f (g x) = f x) :
theorem MeasureTheory.IsAddFundamentalDomain.integrableOn_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) {f : αE} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
theorem MeasureTheory.IsFundamentalDomain.integrableOn_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) {f : αE} (hf : ∀ (g : G) (x : α), f (g x) = f x) :
theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } [] (h : ) (hν : ν.AbsolutelyContinuous μ) (f : αE) (hf : ) :
∫ (x : α), f xν = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f xν
theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] {ν : } [] (h : ) (hν : ν.AbsolutelyContinuous μ) (f : αE) (hf : ) :
∫ (x : α), f xν = ∑' (g : G), ∫ (x : α) in g s, f xν
theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (f : αE) (hf : ) :
∫ (x : α), f xμ = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f xμ
theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (f : αE) (hf : ) :
∫ (x : α), f xμ = ∑' (g : G), ∫ (x : α) in g s, f xμ
theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (f : αE) (hf : ) :
∫ (x : α), f xμ = ∑' (g : G), ∫ (x : α) in s, f (-g +ᵥ x)μ
theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (f : αE) (hf : ) :
∫ (x : α), f xμ = ∑' (g : G), ∫ (x : α) in s, f (g⁻¹ x)μ
theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'' {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (f : αE) (hf : ) :
∫ (x : α), f xμ = ∑' (g : G), ∫ (x : α) in s, f (g +ᵥ x)μ
theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum'' {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) (f : αE) (hf : ) :
∫ (x : α), f xμ = ∑' (g : G), ∫ (x : α) in s, f (g x)μ
theorem MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) {f : αE} {t : Set α} (hf : ) :
∫ (x : α) in t, f xμ = ∑' (g : G), ∫ (x : α) in t (g +ᵥ s), f xμ
theorem MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) {f : αE} {t : Set α} (hf : ) :
∫ (x : α) in t, f xμ = ∑' (g : G), ∫ (x : α) in t g s, f xμ
@[deprecated MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum]
theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) {f : αE} {t : Set α} (hf : ) :
∫ (x : α) in t, f xμ = ∑' (g : G), ∫ (x : α) in t g s, f xμ

Alias of MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum.

theorem MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) {f : αE} {t : Set α} (hf : ) :
∫ (x : α) in t, f xμ = ∑' (g : G), ∫ (x : α) in (g +ᵥ t) s, f (-g +ᵥ x)μ
theorem MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) {f : αE} {t : Set α} (hf : ) :
∫ (x : α) in t, f xμ = ∑' (g : G), ∫ (x : α) in g t s, f (g⁻¹ x)μ
@[deprecated MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum']
theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {μ : } [] [] [] [] (h : ) {f : αE} {t : Set α} (hf : ) :
∫ (x : α) in t, f xμ = ∑' (g : G), ∫ (x : α) in g t s, f (g⁻¹ x)μ

Alias of MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum'.

theorem MeasureTheory.IsAddFundamentalDomain.setIntegral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] [] (hs : ) (ht : ) {f : αE} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) :
∫ (x : α) in s, f xμ = ∫ (x : α) in t, f xμ
theorem MeasureTheory.IsFundamentalDomain.setIntegral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] [] (hs : ) (ht : ) {f : αE} (hf : ∀ (g : G) (x : α), f (g x) = f x) :
∫ (x : α) in s, f xμ = ∫ (x : α) in t, f xμ
@[deprecated MeasureTheory.IsFundamentalDomain.setIntegral_eq]
theorem MeasureTheory.IsFundamentalDomain.set_integral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] [] (hs : ) (ht : ) {f : αE} (hf : ∀ (g : G) (x : α), f (g x) = f x) :
∫ (x : α) in s, f xμ = ∫ (x : α) in t, f xμ

Alias of MeasureTheory.IsFundamentalDomain.setIntegral_eq.

theorem MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) (hd : Pairwise ( on fun (g : G) => (g +ᵥ t) s)) :
μ t μ s

If the additive action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t such that the sets g +ᵥ t ∩ s are pairwise a.e.-disjoint has measure at most μ s.

theorem MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (ht : ) (hd : Pairwise ( on fun (g : G) => g t s)) :
μ t μ s

If the action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t such that the sets g • t ∩ s are pairwise a.e.-disjoint has measure at most μ s.

theorem MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (htm : ) (ht : μ s < μ t) :
xt, yt, ∃ (g : G), g 0 g +ᵥ x = y

If the additive action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t of measure strictly greater than μ s contains two points x y such that g +ᵥ x = y for some g ≠ 0.

theorem MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {t : Set α} {μ : } [] [] [] (hs : ) (htm : ) (ht : μ s < μ t) :
xt, yt, ∃ (g : G), g 1 g x = y

If the action of a countable group G admits an invariant measure μ with a fundamental domain s, then every null-measurable set t of measure strictly greater than μ s contains two points x y such that g • x = y for some g ≠ 1.

theorem MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (hs : ) {f : αENNReal} (hf : ∀ (γ : G) (x : α), f (γ +ᵥ x) = f x) :
essSup f (μ.restrict s) = essSup f μ

If 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 essSup of f restricted to s is the same as that of f on all of its domain.

theorem MeasureTheory.IsFundamentalDomain.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [] [] [] {s : Set α} {μ : } [] [] [] (hs : ) {f : αENNReal} (hf : ∀ (γ : G) (x : α), f (γ x) = f x) :
essSup f (μ.restrict s) = essSup f μ

If f is invariant under the action of a countable group G, and μ is a G-invariant measure with a fundamental domain s, then the essSup of f restricted to s is the same as that of f on all of its domain.

### Interior/frontier of a fundamental domain #

def MeasureTheory.addFundamentalFrontier (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
Set α

The boundary of a fundamental domain, those points of the domain that also lie in a nontrivial translate.

Equations
Instances For
def MeasureTheory.fundamentalFrontier (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
Set α

The boundary of a fundamental domain, those points of the domain that also lie in a nontrivial translate.

Equations
Instances For
def MeasureTheory.addFundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
Set α

The interior of a fundamental domain, those points of the domain not lying in any translate.

Equations
• = s \ ⋃ (g : G), ⋃ (_ : g 0), g +ᵥ s
Instances For
def MeasureTheory.fundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
Set α

The interior of a fundamental domain, those points of the domain not lying in any translate.

Equations
• = s \ ⋃ (g : G), ⋃ (_ : g 1), g s
Instances For
@[simp]
theorem MeasureTheory.mem_addFundamentalFrontier {G : Type u_1} {α : Type u_3} [] [] {s : Set α} {x : α} :
x s ∃ (g : G), g 0 x g +ᵥ s
@[simp]
theorem MeasureTheory.mem_fundamentalFrontier {G : Type u_1} {α : Type u_3} [] [] {s : Set α} {x : α} :
x s ∃ (g : G), g 1 x g s
@[simp]
theorem MeasureTheory.mem_addFundamentalInterior {G : Type u_1} {α : Type u_3} [] [] {s : Set α} {x : α} :
x s ∀ (g : G), g 0xg +ᵥ s
@[simp]
theorem MeasureTheory.mem_fundamentalInterior {G : Type u_1} {α : Type u_3} [] [] {s : Set α} {x : α} :
x s ∀ (g : G), g 1xg s
theorem MeasureTheory.addFundamentalFrontier_subset {G : Type u_1} {α : Type u_3} [] [] {s : Set α} :
theorem MeasureTheory.fundamentalFrontier_subset {G : Type u_1} {α : Type u_3} [] [] {s : Set α} :
theorem MeasureTheory.addFundamentalInterior_subset {G : Type u_1} {α : Type u_3} [] [] {s : Set α} :
theorem MeasureTheory.fundamentalInterior_subset {G : Type u_1} {α : Type u_3} [] [] {s : Set α} :
@[simp]
@[simp]
theorem MeasureTheory.fundamentalInterior_union_fundamentalFrontier (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
@[simp]
@[simp]
theorem MeasureTheory.fundamentalFrontier_union_fundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
@[simp]
theorem MeasureTheory.sdiff_addFundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
@[simp]
theorem MeasureTheory.sdiff_fundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
@[simp]
theorem MeasureTheory.sdiff_addFundamentalFrontier (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
@[simp]
theorem MeasureTheory.sdiff_fundamentalFrontier (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
@[simp]
theorem MeasureTheory.addFundamentalFrontier_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [] [] (s : Set α) [] [] [] (g : H) :
@[simp]
theorem MeasureTheory.fundamentalFrontier_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [] [] (s : Set α) [] [] [] (g : H) :
@[simp]
theorem MeasureTheory.addFundamentalInterior_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [] [] (s : Set α) [] [] [] (g : H) :
@[simp]
theorem MeasureTheory.fundamentalInterior_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [] [] (s : Set α) [] [] [] (g : H) :
theorem MeasureTheory.pairwise_disjoint_addFundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
Pairwise (Disjoint on fun (g : G) => )
theorem MeasureTheory.pairwise_disjoint_fundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) :
Pairwise (Disjoint on fun (g : G) => )
theorem MeasureTheory.NullMeasurableSet.addFundamentalFrontier (G : Type u_1) {α : Type u_3} [] [] (s : Set α) [] [] [] [] {μ : } (hs : ) :
theorem MeasureTheory.NullMeasurableSet.fundamentalFrontier (G : Type u_1) {α : Type u_3} [] [] (s : Set α) [] [] [] [] {μ : } (hs : ) :
theorem MeasureTheory.NullMeasurableSet.addFundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) [] [] [] [] {μ : } (hs : ) :
theorem MeasureTheory.NullMeasurableSet.fundamentalInterior (G : Type u_1) {α : Type u_3} [] [] (s : Set α) [] [] [] [] {μ : } (hs : ) :
theorem MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier {G : Type u_1} {α : Type u_3} [] [] [] [] {μ : } {s : Set α} (hs : ) :
theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier {G : Type u_1} {α : Type u_3} [] [] [] [] {μ : } {s : Set α} (hs : ) :
= 0
theorem MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior {G : Type u_1} {α : Type u_3} [] [] [] [] {μ : } {s : Set α} (hs : ) :
= μ s
theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior {G : Type u_1} {α : Type u_3} [] [] [] [] {μ : } {s : Set α} (hs : ) :
= μ s
theorem MeasureTheory.IsFundamentalDomain.fundamentalInterior {G : Type u_1} {α : Type u_3} [] [] [] [] {μ : } {s : Set α} (hs : ) [] [] :
theorem MeasureTheory.addMeasure_map_restrict_apply {G : Type u_1} {α : Type u_3} [] [] [] (μ : ) (s : Set α) {U : Set ()} (meas_U : ) :
(MeasureTheory.Measure.map () (μ.restrict s)) U = μ ( ⁻¹' U s)
theorem MeasureTheory.measure_map_restrict_apply {G : Type u_1} {α : Type u_3} [] [] [] (μ : ) (s : Set α) {U : Set ()} (meas_U : ) :
(MeasureTheory.Measure.map () (μ.restrict s)) U = μ ( ⁻¹' U s)
theorem MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq {G : Type u_1} {α : Type u_3} [] [] [] (μ : ) [] [] {s : Set α} {t : Set α} [] (fund_dom_s : ) (fund_dom_t : ) :
MeasureTheory.Measure.map () (μ.restrict s) = MeasureTheory.Measure.map () (μ.restrict t)
theorem MeasureTheory.IsFundamentalDomain.quotientMeasure_eq {G : Type u_1} {α : Type u_3} [] [] [] (μ : ) [] [] {s : Set α} {t : Set α} [] (fund_dom_s : ) (fund_dom_t : ) :
MeasureTheory.Measure.map () (μ.restrict s) = MeasureTheory.Measure.map () (μ.restrict t)

## HasFundamentalDomain typeclass #

We define HasFundamentalDomain in order to be able to define the covolume of a quotient of α by a group G, which under reasonable conditions does not depend on the choice of fundamental domain. Even though any "sensible" action should have a fundamental domain, this is a rather delicate question which was recently addressed by Misha Kapovich: https://arxiv.org/abs/2301.05325

TODO: Formalize the existence of a Dirichlet domain as in Kapovich's paper.

class MeasureTheory.HasAddFundamentalDomain (G : Type u_6) (α : Type u_7) [Zero G] [VAdd G α] [] (ν : ) :

We say a quotient of α by G HasAddFundamentalDomain if there is a measurable set s for which IsAddFundamentalDomain G s holds.

• ExistsIsAddFundamentalDomain : ∃ (s : Set α),
Instances
theorem MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain {G : Type u_6} {α : Type u_7} [Zero G] [VAdd G α] [] {ν : } [self : ] :
∃ (s : Set α),
class MeasureTheory.HasFundamentalDomain (G : Type u_6) (α : Type u_7) [One G] [SMul G α] [] (ν : ) :

We say a quotient of α by G HasFundamentalDomain if there is a measurable set s for which IsFundamentalDomain G s holds.

• ExistsIsFundamentalDomain : ∃ (s : Set α),
Instances
theorem MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain {G : Type u_6} {α : Type u_7} [One G] [SMul G α] [] {ν : } [self : ] :
∃ (s : Set α),
noncomputable def MeasureTheory.addCovolume (G : Type u_6) (α : Type u_7) [Zero G] [VAdd G α] [] (ν : ) :

The addCovolume of an action of G on α is the volume of some fundamental domain, or 0 if none exists.

Equations
• = if funDom : then ν .choose else 0
Instances For
noncomputable def MeasureTheory.covolume (G : Type u_6) (α : Type u_7) [One G] [SMul G α] [] (ν : ) :

The covolume of an action of G on α the volume of some fundamental domain, or 0 if none exists.

Equations
• = if funDom : then ν .choose else 0
Instances For
theorem MeasureTheory.IsAddFundamentalDomain.hasAddFundamentalDomain {G : Type u_1} {α : Type u_3} [] [] [] (ν : ) {s : Set α} (fund_dom_s : ) :
theorem MeasureTheory.IsFundamentalDomain.hasFundamentalDomain {G : Type u_1} {α : Type u_3} [] [] [] (ν : ) {s : Set α} (fund_dom_s : ) :

If there is a fundamental domain s, then HasFundamentalDomain holds.

theorem MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume {G : Type u_1} {α : Type u_3} [] [] [] [] (ν : ) [] [] {s : Set α} (fund_dom_s : ) :
= ν s
theorem MeasureTheory.IsFundamentalDomain.covolume_eq_volume {G : Type u_1} {α : Type u_3} [] [] [] [] (ν : ) [] [] {s : Set α} (fund_dom_s : ) :
= ν s

The covolume can be computed by taking the volume of any given fundamental domain s.

## QuotientMeasureEqMeasurePreimage typeclass #

This typeclass describes a situation in which a measure μ on α ⧸ G can be computed by taking a measure ν on α of the intersection of the pullback with a fundamental domain.

It's curious that in measure theory, measures can be pushed forward, while in geometry, volumes can be pulled back. And yet here, we are describing a situation involving measures in a geometric way.

Another viewpoint is that if a set is small enough to fit in a single fundamental domain, then its ν measure in α is the same as the μ measure of its pushforward in α ⧸ G.

class MeasureTheory.AddQuotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [] [] [] (ν : ) (μ : ) :

A measure μ on the AddQuotient of α mod G satisfies AddQuotientMeasureEqMeasurePreimage if: for any fundamental domain t, and any measurable subset U of the quotient, μ U = volume ((π ⁻¹' U) ∩ t).

• addProjection_respects_measure' : ∀ (t : Set α),
Instances
theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure' {G : Type u_1} {α : Type u_3} [] [] [] {ν : } {μ : } (t : Set α) :
class MeasureTheory.QuotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [] [] [] (ν : ) (μ : ) :

Measures ν on α and μ on the Quotient of α mod G satisfy QuotientMeasureEqMeasurePreimage if: for any fundamental domain t, and any measurable subset U of the quotient, μ U = ν ((π ⁻¹' U) ∩ t).

• projection_respects_measure' : ∀ (t : Set α),
Instances
theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure' {G : Type u_1} {α : Type u_3} [] [] [] {ν : } {μ : } [self : ] (t : Set α) :
theorem MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure {G : Type u_1} {α : Type u_3} [] [] [] {ν : } (μ : ) {t : Set α} (fund_dom_t : ) :
μ = MeasureTheory.Measure.map () (ν.restrict t)
theorem MeasureTheory.IsFundamentalDomain.projection_respects_measure {G : Type u_1} {α : Type u_3} [] [] [] {ν : } (μ : ) {t : Set α} (fund_dom_t : ) :
μ = MeasureTheory.Measure.map () (ν.restrict t)
theorem MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply {G : Type u_1} {α : Type u_3} [] [] [] {ν : } (μ : ) {t : Set α} (fund_dom_t : ) {U : Set ()} (meas_U : ) :
μ U = ν ( ⁻¹' U t)
theorem MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply {G : Type u_1} {α : Type u_3} [] [] [] {ν : } (μ : ) {t : Set α} (fund_dom_t : ) {U : Set ()} (meas_U : ) :
μ U = ν ( ⁻¹' U t)
theorem MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] {s : Set α} (fund_dom_s : ) :

Given a measure upstairs (i.e., on α), and a choice s of fundamental domain, there's always an artificial way to generate a measure downstairs such that the pair satisfies the QuotientMeasureEqMeasurePreimage typeclass.

theorem MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] {μ : } {s : Set α} (fund_dom_s : ) (h : μ = MeasureTheory.Measure.map () (ν.restrict s)) :
theorem MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] {μ : } {s : Set α} (fund_dom_s : ) (h : μ = MeasureTheory.Measure.map () (ν.restrict s)) :

One can prove QuotientMeasureEqMeasurePreimage by checking behavior with respect to a single fundamental domain.

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.unique {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [hasFun : ] (μ : ) (μ' : ) :
μ = μ'
theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.unique {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [hasFun : ] (μ : ) (μ' : ) :
μ = μ'

Any two measures satisfying QuotientMeasureEqMeasurePreimage are equal.

theorem MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk {G : Type u_1} {α : Type u_3} [] [] [] {ν : } {𝓕 : Set α} (h𝓕 : ) (μ : ) :
MeasureTheory.MeasurePreserving () (ν.restrict 𝓕) μ
theorem MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk {G : Type u_1} {α : Type u_3} [] [] [] {ν : } {𝓕 : Set α} (h𝓕 : ) (μ : ) :
MeasureTheory.MeasurePreserving () (ν.restrict 𝓕) μ

The quotient map to α ⧸ G is measure-preserving between the restriction of volume to a fundamental domain in α and a related measure satisfying QuotientMeasureEqMeasurePreimage.

theorem MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] {s : Set α} (fund_dom_s : ) (vol_s : ν s = 0) :
theorem MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] {s : Set α} (fund_dom_s : ) (vol_s : ν s = 0) :

If a fundamental domain has volume 0, then QuotientMeasureEqMeasurePreimage holds.

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] [i : ] [i' : ] (μ : ) :
theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] [i : ] [i' : ] (μ : ) :

If a measure μ on a quotient satisfies QuotientMeasureEqMeasurePreimage with respect to a sigma-finite measure ν, then it is itself SigmaFinite.

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] (μ : ) [hasFun : ] (h : ) :
theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] (μ : ) [hasFun : ] (h : ) :

A measure μ on α ⧸ G satisfying QuotientMeasureEqMeasurePreimage and having finite covolume is a finite measure.

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.covolume_ne_top {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] (μ : ) :
theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.covolume_ne_top {G : Type u_1} {α : Type u_3} [] [] [] {ν : } [] [] [] (μ : ) :

A finite measure μ on α ⧸ G satisfying QuotientMeasureEqMeasurePreimage has finite covolume.

instance MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace {G : Type u_1} {α : Type u_3} [] [] [] [] [MeasureTheory.VAddInvariantMeasure G α MeasureTheory.volume] [] [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasureTheory.HasAddFundamentalDomain G α MeasureTheory.volume] (μ : ) [MeasureTheory.AddQuotientMeasureEqMeasurePreimage MeasureTheory.volume μ] :
Equations
• =

If a measure μ on a quotient satisfies QuotientVolumeEqVolumePreimage with respect to a sigma-finite measure, then it is itself SigmaFinite.

Equations
• =