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 α] [MeasurableSpace α] (s : Set α) (μ : Measure α := by volume_tac) : Prop

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 : NullMeasurableSet s μ
• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x ∈ s
• aedisjoint : Pairwise (Function.onFun (AEDisjoint μ) fun (g : G) => g +ᵥ s)

structure MeasureTheory.IsFundamentalDomain (G : Type u_1) {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] (s : Set α) (μ : Measure α := by volume_tac) : Prop

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 : NullMeasurableSet s μ
• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
• aedisjoint : Pairwise (Function.onFun (AEDisjoint μ) fun (g : G) => g • s)

theorem MeasureTheory.IsFundamentalDomain.mk' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} (h_meas : NullMeasurableSet s μ) (h_exists : ∀ (x : α), ∃! g : G, g • x ∈ s) : IsFundamentalDomain G 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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} (h_meas : NullMeasurableSet s μ) (h_exists : ∀ (x : α), ∃! g : G, g +ᵥ x ∈ s) : IsAddFundamentalDomain G 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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} (h_meas : NullMeasurableSet s μ) (h_ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s) (h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s) (h_qmp : ∀ (g : G), Measure.QuasiMeasurePreserving (fun (x : α) => g • x) μ μ) : IsFundamentalDomain G s μ

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

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

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

theorem MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [IsFiniteMeasure μ] [Countable G] (h_meas : NullMeasurableSet s μ) (h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s) (h_qmp : ∀ (g : G), Measure.QuasiMeasurePreserving (fun (x : α) => g • x) μ μ) (h_measure_univ_le : μ Set.univ ≤ ∑' (g : G), μ (g • s)) : IsFundamentalDomain 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.mk_of_measure_univ_le {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [IsFiniteMeasure μ] [Countable G] (h_meas : NullMeasurableSet s μ) (h_ae_disjoint : ∀ (g : G), g ≠ 0 → AEDisjoint μ (g +ᵥ s) s) (h_qmp : ∀ (g : G), Measure.QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ) (h_measure_univ_le : μ Set.univ ≤ ∑' (g : G), μ (g +ᵥ s)) : IsAddFundamentalDomain 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.iUnion_smul_ae_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} (h : IsFundamentalDomain G s μ) : ⋃ (g : G), g • s =ᵐ[μ] Set.univ

theorem MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} (h : IsAddFundamentalDomain G s μ) : ⋃ (g : G), g +ᵥ s =ᵐ[μ] Set.univ

theorem MeasureTheory.IsFundamentalDomain.measure_ne_zero {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [Countable G] [SMulInvariantMeasure G α μ] (hμ : μ ≠ 0) (h : IsFundamentalDomain G s μ) : μ s ≠ 0

theorem MeasureTheory.IsAddFundamentalDomain.measure_ne_zero {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [Countable G] [VAddInvariantMeasure G α μ] (hμ : μ ≠ 0) (h : IsAddFundamentalDomain G s μ) : μ s ≠ 0

theorem MeasureTheory.IsFundamentalDomain.mono {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} (h : IsFundamentalDomain G s μ) {ν : Measure α} (hle : ν.AbsolutelyContinuous μ) : IsFundamentalDomain G s ν

theorem MeasureTheory.IsAddFundamentalDomain.mono {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} (h : IsAddFundamentalDomain G s μ) {ν : Measure α} (hle : ν.AbsolutelyContinuous μ) : IsAddFundamentalDomain G s ν

theorem MeasureTheory.IsFundamentalDomain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [Group G] [Group H] [MulAction G α] [MeasurableSpace α] [MulAction H β] [MeasurableSpace β] {s : Set α} {μ : Measure α} {ν : Measure β} (h : IsFundamentalDomain G s μ) {f : β → α} (hf : Measure.QuasiMeasurePreserving f ν μ) {e : G → H} (he : Function.Bijective e) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g • x) fun (x : α) => g • x) : IsFundamentalDomain H (f ⁻¹' s) ν

theorem MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddGroup H] [AddAction G α] [MeasurableSpace α] [AddAction H β] [MeasurableSpace β] {s : Set α} {μ : Measure α} {ν : Measure β} (h : IsAddFundamentalDomain G s μ) {f : β → α} (hf : Measure.QuasiMeasurePreserving f ν μ) {e : G → H} (he : Function.Bijective e) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g +ᵥ x) fun (x : α) => g +ᵥ x) : IsAddFundamentalDomain H (f ⁻¹' s) ν

theorem MeasureTheory.IsFundamentalDomain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [Group G] [Group H] [MulAction G α] [MeasurableSpace α] [MulAction H β] [MeasurableSpace β] {s : Set α} {μ : Measure α} {ν : Measure β} (h : IsFundamentalDomain G s μ) (f : α ≃ β) (hf : Measure.QuasiMeasurePreserving (⇑f.symm) ν μ) (e : H ≃ G) (hef : ∀ (g : H), Function.Semiconj (⇑f) (fun (x : α) => e g • x) fun (x : β) => g • x) : IsFundamentalDomain H (⇑f '' s) ν

theorem MeasureTheory.IsAddFundamentalDomain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddGroup H] [AddAction G α] [MeasurableSpace α] [AddAction H β] [MeasurableSpace β] {s : Set α} {μ : Measure α} {ν : Measure β} (h : IsAddFundamentalDomain G s μ) (f : α ≃ β) (hf : Measure.QuasiMeasurePreserving (⇑f.symm) ν μ) (e : H ≃ G) (hef : ∀ (g : H), Function.Semiconj (⇑f) (fun (x : α) => e g +ᵥ x) fun (x : β) => g +ᵥ x) : IsAddFundamentalDomain H (⇑f '' s) ν

theorem MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ ν : Measure α} (h : IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) : Pairwise fun (g₁ g₂ : G) => AEDisjoint ν (g₁ • s) (g₂ • s)

theorem MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ ν : Measure α} (h : IsAddFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) : Pairwise fun (g₁ g₂ : G) => AEDisjoint ν (g₁ +ᵥ s) (g₂ +ᵥ s)

theorem MeasureTheory.IsFundamentalDomain.smul_of_comm {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} {G' : Type u_6} [Group G'] [MulAction G' α] [MeasurableConstSMul G' α] [SMulInvariantMeasure G' α μ] [SMulCommClass G' G α] (h : IsFundamentalDomain G s μ) (g : G') : IsFundamentalDomain G (g • s) μ

theorem MeasureTheory.IsAddFundamentalDomain.vadd_of_comm {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} {G' : Type u_6} [AddGroup G'] [AddAction G' α] [MeasurableConstVAdd G' α] [VAddInvariantMeasure G' α μ] [VAddCommClass G' G α] (h : IsAddFundamentalDomain G s μ) (g : G') : IsAddFundamentalDomain G (g +ᵥ s) μ

theorem MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] (h : IsFundamentalDomain G s μ) (g : G) : NullMeasurableSet (g • s) μ

theorem MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] (h : IsAddFundamentalDomain G s μ) (g : G) : NullMeasurableSet (g +ᵥ s) μ

theorem MeasureTheory.IsFundamentalDomain.restrict_restrict {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] (h : IsFundamentalDomain G s μ) (g : G) (t : Set α) : (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t)

theorem MeasureTheory.IsAddFundamentalDomain.restrict_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] (h : IsAddFundamentalDomain G s μ) (g : G) (t : Set α) : (μ.restrict t).restrict (g +ᵥ s) = μ.restrict ((g +ᵥ s) ∩ t)

theorem MeasureTheory.IsFundamentalDomain.smul {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] (h : IsFundamentalDomain G s μ) (g : G) : IsFundamentalDomain G (g • s) μ

theorem MeasureTheory.IsAddFundamentalDomain.vadd {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] (h : IsAddFundamentalDomain G s μ) (g : G) : IsAddFundamentalDomain G (g +ᵥ s) μ

theorem MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] {ν : Measure α} (h : IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) : (Measure.sum fun (g : G) => ν.restrict (g • s)) = ν

theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] {ν : Measure α} (h : IsAddFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) : (Measure.sum fun (g : G) => ν.restrict (g +ᵥ s)) = ν

theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] {ν : Measure α} (h : IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν

theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] {ν : Measure α} (h : IsAddFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂ν

theorem MeasureTheory.IsFundamentalDomain.sum_restrict {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) : (Measure.sum fun (g : G) => μ.restrict (g • s)) = μ

theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) : (Measure.sum fun (g : G) => μ.restrict (g +ᵥ s)) = μ

theorem MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (f : α → ENNReal) : ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (f : α → ENNReal) (t : Set α) : ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (f : α → ENNReal) (t : Set α) : ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (f : α → ENNReal) (t : Set α) : ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] {ν : Measure α} (h : IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (t : Set α) : ν t = ∑' (g : G), ν (t ∩ g • s)

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] {ν : Measure α} (h : IsAddFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (t : Set α) : ν t = ∑' (g : G), ν (t ∩ (g +ᵥ s))

theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (t : Set α) : μ t = ∑' (g : G), μ (t ∩ g • s)

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (t : Set α) : μ t = ∑' (g : G), μ (t ∩ (g +ᵥ s))

theorem MeasureTheory.IsFundamentalDomain.measure_eq_tsum {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (t : Set α) : μ t = ∑' (g : G), μ (g • t ∩ s)

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (t : Set α) : μ t = ∑' (g : G), μ ((g +ᵥ t) ∩ s)

theorem MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (h : IsFundamentalDomain G s μ) (t : Set α) (ht : ∀ (g : G), g • t = t) (hts : μ (t ∩ s) = 0) : μ t = 0

theorem MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (h : IsAddFundamentalDomain G s μ) (t : Set α) (ht : ∀ (g : G), g +ᵥ t = t) (hts : μ (t ∩ s) = 0) : μ t = 0

theorem MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] [Finite G] (h : IsFundamentalDomain G s μ) (t : Set α) (ht : ∀ (g : G), g • t =ᵐ[μ] t) : μ t = Nat.card G • μ (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.measure_eq_card_smul_of_vadd_ae_eq_self {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] [Finite G] (h : IsAddFundamentalDomain G s μ) (t : Set α) (ht : ∀ (g : G), g +ᵥ t =ᵐ[μ] t) : μ t = Nat.card G • μ (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.setLIntegral_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) (f : α → ENNReal) (hf : ∀ (g : G) (x : α), f (g • x) = f x) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) (ht : IsAddFundamentalDomain G t μ) (f : α → ENNReal) (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.measure_set_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {A : Set α} (hA₀ : MeasurableSet A) (hA : ∀ (g : G), (fun (x : α) => g • x) ⁻¹' A = A) : μ (A ∩ s) = μ (A ∩ t)

theorem MeasureTheory.IsAddFundamentalDomain.measure_set_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) (ht : IsAddFundamentalDomain G t μ) {A : Set α} (hA₀ : MeasurableSet A) (hA : ∀ (g : G), (fun (x : α) => g +ᵥ x) ⁻¹' A = A) : μ (A ∩ s) = μ (A ∩ t)

theorem MeasureTheory.IsFundamentalDomain.measure_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) : μ s = μ t

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

theorem MeasureTheory.IsAddFundamentalDomain.measure_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) (ht : IsAddFundamentalDomain G t μ) : μ s = μ t

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

theorem MeasureTheory.IsFundamentalDomain.aestronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] {β : Type u_6} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → β} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (μ.restrict t)

theorem MeasureTheory.IsAddFundamentalDomain.aestronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] {β : Type u_6} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] (hs : IsAddFundamentalDomain G s μ) (ht : IsAddFundamentalDomain G t μ) {f : α → β} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (μ.restrict t)

theorem MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : HasFiniteIntegral f (μ.restrict s) ↔ HasFiniteIntegral f (μ.restrict t)

theorem MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) (ht : IsAddFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : HasFiniteIntegral f (μ.restrict s) ↔ HasFiniteIntegral f (μ.restrict t)

theorem MeasureTheory.IsFundamentalDomain.integrableOn_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : IntegrableOn f s μ ↔ IntegrableOn f t μ

theorem MeasureTheory.IsAddFundamentalDomain.integrableOn_iff {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) (ht : IsAddFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : IntegrableOn f s μ ↔ IntegrableOn f t μ

theorem MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] {ν : Measure α} [NormedSpace ℝ E] (h : IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (f : α → E) (hf : Integrable f ν) : ∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν

theorem MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] {ν : Measure α} [NormedSpace ℝ E] (h : IsAddFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (f : α → E) (hf : Integrable f ν) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) : ∫ (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsAddFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) : ∫ (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsAddFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) : ∫ (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsAddFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) : ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : IntegrableOn f t μ) : ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsAddFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : IntegrableOn f t μ) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : IntegrableOn f t μ) : ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum' {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : IsAddFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : IntegrableOn f t μ) : ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ

theorem MeasureTheory.IsFundamentalDomain.setIntegral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsAddFundamentalDomain.setIntegral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (hs : IsAddFundamentalDomain G s μ) (ht : IsAddFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

theorem MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) (ht : NullMeasurableSet t μ) (hd : Pairwise (Function.onFun (AEDisjoint μ) 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.measure_le_of_pairwise_disjoint {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) (ht : NullMeasurableSet t μ) (hd : Pairwise (Function.onFun (AEDisjoint μ) 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.exists_ne_one_smul_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) (htm : NullMeasurableSet t μ) (ht : μ s < μ t) : ∃ x ∈ t, ∃ y ∈ t, ∃ (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.exists_ne_zero_vadd_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s t : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) (htm : NullMeasurableSet t μ) (ht : μ s < μ t) : ∃ x ∈ t, ∃ y ∈ t, ∃ (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.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] [Countable G] (hs : IsFundamentalDomain G s μ) {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.

theorem MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : Measure α} [MeasurableConstVAdd G α] [VAddInvariantMeasure G α μ] [Countable G] (hs : IsAddFundamentalDomain G s μ) {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.

Interior/frontier of a fundamental domain

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

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

Equations

• MeasureTheory.fundamentalFrontier G s = s ∩ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s

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

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

Equations

• MeasureTheory.addFundamentalFrontier G s = s ∩ ⋃ (g : G), ⋃ (_ : g ≠ 0), g +ᵥ s

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

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

Equations

• MeasureTheory.fundamentalInterior G s = s \ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s

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

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

Equations

• MeasureTheory.addFundamentalInterior G s = s \ ⋃ (g : G), ⋃ (_ : g ≠ 0), g +ᵥ s

@[simp]

theorem MeasureTheory.mem_fundamentalFrontier {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {x : α} : x ∈ fundamentalFrontier G s ↔ x ∈ s ∧ ∃ (g : G), g ≠ 1 ∧ x ∈ g • s

@[simp]

theorem MeasureTheory.mem_addFundamentalFrontier {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {x : α} : x ∈ addFundamentalFrontier G s ↔ x ∈ s ∧ ∃ (g : G), g ≠ 0 ∧ x ∈ g +ᵥ s

@[simp]

theorem MeasureTheory.mem_fundamentalInterior {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {x : α} : x ∈ fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s

@[simp]

theorem MeasureTheory.mem_addFundamentalInterior {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {x : α} : x ∈ addFundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 0 → x ∉ g +ᵥ s

theorem MeasureTheory.fundamentalFrontier_subset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} : fundamentalFrontier G s ⊆ s

theorem MeasureTheory.addFundamentalFrontier_subset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} : addFundamentalFrontier G s ⊆ s

theorem MeasureTheory.fundamentalInterior_subset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} : fundamentalInterior G s ⊆ s

theorem MeasureTheory.addFundamentalInterior_subset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} : addFundamentalInterior G s ⊆ s

theorem MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Disjoint (fundamentalInterior G s) (fundamentalFrontier G s)

theorem MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Disjoint (addFundamentalInterior G s) (addFundamentalFrontier G s)

@[simp]

theorem MeasureTheory.fundamentalInterior_union_fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : fundamentalInterior G s ∪ fundamentalFrontier G s = s

@[simp]

theorem MeasureTheory.addFundamentalInterior_union_addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : addFundamentalInterior G s ∪ addFundamentalFrontier G s = s

@[simp]

theorem MeasureTheory.fundamentalFrontier_union_fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : fundamentalFrontier G s ∪ fundamentalInterior G s = s

@[simp]

theorem MeasureTheory.addFundamentalFrontier_union_addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : addFundamentalFrontier G s ∪ addFundamentalInterior G s = s

@[simp]

theorem MeasureTheory.sdiff_fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : s \ fundamentalInterior G s = fundamentalFrontier G s

@[simp]

theorem MeasureTheory.sdiff_addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : s \ addFundamentalInterior G s = addFundamentalFrontier G s

@[simp]

theorem MeasureTheory.sdiff_fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : s \ fundamentalFrontier G s = fundamentalInterior G s

@[simp]

theorem MeasureTheory.sdiff_addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : s \ addFundamentalFrontier G s = addFundamentalInterior G s

@[simp]

theorem MeasureTheory.fundamentalFrontier_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) : fundamentalFrontier G (g • s) = g • fundamentalFrontier G s

@[simp]

theorem MeasureTheory.addFundamentalFrontier_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [AddGroup H] [AddAction H α] [VAddCommClass H G α] (g : H) : addFundamentalFrontier G (g +ᵥ s) = g +ᵥ addFundamentalFrontier G s

@[simp]

theorem MeasureTheory.fundamentalInterior_smul (G : Type u_1) {H : Type u_2} {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Group H] [MulAction H α] [SMulCommClass H G α] (g : H) : fundamentalInterior G (g • s) = g • fundamentalInterior G s

@[simp]

theorem MeasureTheory.addFundamentalInterior_vadd (G : Type u_1) {H : Type u_2} {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [AddGroup H] [AddAction H α] [VAddCommClass H G α] (g : H) : addFundamentalInterior G (g +ᵥ s) = g +ᵥ addFundamentalInterior G s

theorem MeasureTheory.pairwise_disjoint_fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Pairwise (Function.onFun Disjoint fun (g : G) => g • fundamentalInterior G s)

theorem MeasureTheory.pairwise_disjoint_addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Pairwise (Function.onFun Disjoint fun (g : G) => g +ᵥ addFundamentalInterior G s)

theorem MeasureTheory.NullMeasurableSet.fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Countable G] [MeasurableSpace α] [MeasurableConstSMul G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (hs : NullMeasurableSet s μ) : NullMeasurableSet (fundamentalFrontier G s) μ

theorem MeasureTheory.NullMeasurableSet.addFundamentalFrontier (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [Countable G] [MeasurableSpace α] [MeasurableConstVAdd G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (hs : NullMeasurableSet s μ) : NullMeasurableSet (addFundamentalFrontier G s) μ

theorem MeasureTheory.NullMeasurableSet.fundamentalInterior (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) [Countable G] [MeasurableSpace α] [MeasurableConstSMul G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (hs : NullMeasurableSet s μ) : NullMeasurableSet (fundamentalInterior G s) μ

theorem MeasureTheory.NullMeasurableSet.addFundamentalInterior (G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) [Countable G] [MeasurableSpace α] [MeasurableConstVAdd G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (hs : NullMeasurableSet s μ) : NullMeasurableSet (addFundamentalInterior G s) μ

theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier {G : Type u_1} {α : Type u_3} [Countable G] [Group G] [MulAction G α] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : IsFundamentalDomain G s μ) : μ (fundamentalFrontier G s) = 0

theorem MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier {G : Type u_1} {α : Type u_3} [Countable G] [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : IsAddFundamentalDomain G s μ) : μ (addFundamentalFrontier G s) = 0

theorem MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior {G : Type u_1} {α : Type u_3} [Countable G] [Group G] [MulAction G α] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : IsFundamentalDomain G s μ) : μ (fundamentalInterior G s) = μ s

theorem MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior {G : Type u_1} {α : Type u_3} [Countable G] [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : IsAddFundamentalDomain G s μ) : μ (addFundamentalInterior G s) = μ s

theorem MeasureTheory.IsFundamentalDomain.fundamentalInterior {G : Type u_1} {α : Type u_3} [Countable G] [Group G] [MulAction G α] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : IsFundamentalDomain G s μ) [MeasurableConstSMul G α] [SMulInvariantMeasure G α μ] : IsFundamentalDomain G (fundamentalInterior G s) μ

theorem MeasureTheory.measure_map_restrict_apply {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (μ : Measure α) (s : Set α) {U : Set (Quotient (MulAction.orbitRel G α))} (meas_U : MeasurableSet U) : (Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s)) U = μ (Quotient.mk (MulAction.orbitRel G α) ⁻¹' U ∩ s)

theorem MeasureTheory.addMeasure_map_restrict_apply {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] (μ : Measure α) (s : Set α) {U : Set (Quotient (AddAction.orbitRel G α))} (meas_U : MeasurableSet U) : (Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s)) U = μ (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ s)

theorem MeasureTheory.IsFundamentalDomain.quotientMeasure_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (μ : Measure α) [Countable G] {s t : Set α} [SMulInvariantMeasure G α μ] [MeasurableConstSMul G α] (fund_dom_s : IsFundamentalDomain G s μ) (fund_dom_t : IsFundamentalDomain G t μ) : Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s) = Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict t)

theorem MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] (μ : Measure α) [Countable G] {s t : Set α} [VAddInvariantMeasure G α μ] [MeasurableConstVAdd G α] (fund_dom_s : IsAddFundamentalDomain G s μ) (fund_dom_t : IsAddFundamentalDomain G t μ) : Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s) = Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.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 α] [MeasurableSpace α] (ν : Measure α := by volume_tac) : Prop

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

• ExistsIsAddFundamentalDomain : ∃ (s : Set α), IsAddFundamentalDomain G s ν

class MeasureTheory.HasFundamentalDomain (G : Type u_6) (α : Type u_7) [One G] [SMul G α] [MeasurableSpace α] (ν : Measure α := by volume_tac) : Prop

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

• ExistsIsFundamentalDomain : ∃ (s : Set α), IsFundamentalDomain G s ν

noncomputable def MeasureTheory.covolume (G : Type u_6) (α : Type u_7) [One G] [SMul G α] [MeasurableSpace α] (ν : Measure α := by volume_tac) : ENNReal

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

Equations

• MeasureTheory.covolume G α ν = if funDom : MeasureTheory.HasFundamentalDomain G α ν then ν ⋯.choose else 0

noncomputable def MeasureTheory.addCovolume (G : Type u_6) (α : Type u_7) [Zero G] [VAdd G α] [MeasurableSpace α] (ν : Measure α := by volume_tac) : ENNReal

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

Equations

• MeasureTheory.addCovolume G α ν = if funDom : MeasureTheory.HasAddFundamentalDomain G α ν then ν ⋯.choose else 0

theorem MeasureTheory.IsFundamentalDomain.hasFundamentalDomain {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (ν : Measure α) {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) : HasFundamentalDomain G α ν

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

theorem MeasureTheory.IsAddFundamentalDomain.hasAddFundamentalDomain {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] (ν : Measure α) {s : Set α} (fund_dom_s : IsAddFundamentalDomain G s ν) : HasAddFundamentalDomain G α ν

If there is an additive fundamental domain s, then HasAddFundamentalDomain holds.

theorem MeasureTheory.IsFundamentalDomain.covolume_eq_volume {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (ν : Measure α) [Countable G] [MeasurableConstSMul G α] [SMulInvariantMeasure G α ν] {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) : covolume G α ν = ν s

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

theorem MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] (ν : Measure α) [Countable G] [MeasurableConstVAdd G α] [VAddInvariantMeasure G α ν] {s : Set α} (fund_dom_s : IsAddFundamentalDomain G s ν) : addCovolume G α ν = ν s

The addCovolume can be computed by taking the volume of any given additive 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} [AddGroup G] [AddAction G α] [MeasurableSpace α] (ν : Measure α := by volume_tac) (μ : Measure (Quotient (AddAction.orbitRel G α))) : Prop

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 α) : IsAddFundamentalDomain G t ν → μ = Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t)

class MeasureTheory.QuotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (ν : Measure α := by volume_tac) (μ : Measure (Quotient (MulAction.orbitRel G α))) : Prop

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 α) : IsFundamentalDomain G t ν → μ = Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t)

theorem MeasureTheory.IsFundamentalDomain.projection_respects_measure {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} (μ : Measure (Quotient (MulAction.orbitRel G α))) [i : QuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : IsFundamentalDomain G t ν) : μ = Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t)

theorem MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} (μ : Measure (Quotient (AddAction.orbitRel G α))) [i : AddQuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : IsAddFundamentalDomain G t ν) : μ = Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t)

theorem MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} (μ : Measure (Quotient (MulAction.orbitRel G α))) [i : QuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : IsFundamentalDomain G t ν) {U : Set (Quotient (MulAction.orbitRel G α))} (meas_U : MeasurableSet U) : μ U = ν (Quotient.mk (MulAction.orbitRel G α) ⁻¹' U ∩ t)

theorem MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} (μ : Measure (Quotient (AddAction.orbitRel G α))) [i : AddQuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : IsAddFundamentalDomain G t ν) {U : Set (Quotient (AddAction.orbitRel G α))} (meas_U : MeasurableSet U) : μ U = ν (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ t)

theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.unique {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} [hasFun : HasFundamentalDomain G α ν] (μ μ' : Measure (Quotient (MulAction.orbitRel G α))) [QuotientMeasureEqMeasurePreimage ν μ] [QuotientMeasureEqMeasurePreimage ν μ'] : μ = μ'

Any two measures satisfying QuotientMeasureEqMeasurePreimage are equal.

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.unique {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} [hasFun : HasAddFundamentalDomain G α ν] (μ μ' : Measure (Quotient (AddAction.orbitRel G α))) [AddQuotientMeasureEqMeasurePreimage ν μ] [AddQuotientMeasureEqMeasurePreimage ν μ'] : μ = μ'

Any two measures satisfying AddQuotientMeasureEqMeasurePreimage are equal.

theorem MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} {𝓕 : Set α} (h𝓕 : IsFundamentalDomain G 𝓕 ν) (μ : Measure (Quotient (MulAction.orbitRel G α))) [QuotientMeasureEqMeasurePreimage ν μ] : MeasurePreserving (Quotient.mk (MulAction.orbitRel G α)) (ν.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.measurePreserving_add_quotient_mk {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} {𝓕 : Set α} (h𝓕 : IsAddFundamentalDomain G 𝓕 ν) (μ : Measure (Quotient (AddAction.orbitRel G α))) [AddQuotientMeasureEqMeasurePreimage ν μ] : MeasurePreserving (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict 𝓕) μ

The quotient map to the additive quotient of α by G is measure-preserving between the restriction of volume to an additive fundamental domain in α and a related measure satisfying AddQuotientMeasureEqMeasurePreimage.

theorem MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} [SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α] {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) : QuotientMeasureEqMeasurePreimage ν (Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict 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_addQuotientMeasure {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} [VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α] {s : Set α} (fund_dom_s : IsAddFundamentalDomain G s ν) : AddQuotientMeasureEqMeasurePreimage ν (Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s))

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

theorem MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} [SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α] {μ : Measure (Quotient (MulAction.orbitRel G α))} {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) (h : μ = Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s)) : QuotientMeasureEqMeasurePreimage ν μ

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

theorem MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} [VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α] {μ : Measure (Quotient (AddAction.orbitRel G α))} {s : Set α} (fund_dom_s : IsAddFundamentalDomain G s ν) (h : μ = Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s)) : AddQuotientMeasureEqMeasurePreimage ν μ

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

theorem MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} [SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α] {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) (vol_s : ν s = 0) : QuotientMeasureEqMeasurePreimage ν 0

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

theorem MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} [VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α] {s : Set α} (fund_dom_s : IsAddFundamentalDomain G s ν) (vol_s : ν s = 0) : AddQuotientMeasureEqMeasurePreimage ν 0

If an additive fundamental domain has volume 0, then AddQuotientMeasureEqMeasurePreimage holds.

theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} [SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α] [i : SigmaFinite ν] [i' : HasFundamentalDomain G α ν] (μ : Measure (Quotient (MulAction.orbitRel G α))) [QuotientMeasureEqMeasurePreimage ν μ] : SigmaFinite μ

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

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} [VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α] [i : SigmaFinite ν] [i' : HasAddFundamentalDomain G α ν] (μ : Measure (Quotient (AddAction.orbitRel G α))) [AddQuotientMeasureEqMeasurePreimage ν μ] : SigmaFinite μ

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

theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} [SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α] (μ : Measure (Quotient (MulAction.orbitRel G α))) [QuotientMeasureEqMeasurePreimage ν μ] [hasFun : HasFundamentalDomain G α ν] (h : covolume G α ν ≠ ⊤) : IsFiniteMeasure μ

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

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} [VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α] (μ : Measure (Quotient (AddAction.orbitRel G α))) [AddQuotientMeasureEqMeasurePreimage ν μ] [hasFun : HasAddFundamentalDomain G α ν] (h : addCovolume G α ν ≠ ⊤) : IsFiniteMeasure μ

A measure μ on the additive quotient of α by G satisfying AddQuotientMeasureEqMeasurePreimage and having finite covolume is a finite measure.

theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.covolume_ne_top {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : Measure α} [SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α] (μ : Measure (Quotient (MulAction.orbitRel G α))) [QuotientMeasureEqMeasurePreimage ν μ] [IsFiniteMeasure μ] : covolume G α ν < ⊤

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

theorem MeasureTheory.AddQuotientMeasureEqMeasurePreimage.covolume_ne_top {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : Measure α} [VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α] (μ : Measure (Quotient (AddAction.orbitRel G α))) [AddQuotientMeasureEqMeasurePreimage ν μ] [IsFiniteMeasure μ] : addCovolume G α ν < ⊤

A finite measure μ on the additive quotient of α by G satisfying AddQuotientMeasureEqMeasurePreimage has finite covolume.

instance MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasureSpace α] [Countable G] [SMulInvariantMeasure G α volume] [MeasurableConstSMul G α] [SigmaFinite volume] [HasFundamentalDomain G α volume] (μ : Measure (Quotient (MulAction.orbitRel G α))) [QuotientMeasureEqMeasurePreimage volume μ] : SigmaFinite μ

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

instance MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasureSpace α] [Countable G] [VAddInvariantMeasure G α volume] [MeasurableConstVAdd G α] [SigmaFinite volume] [HasAddFundamentalDomain G α volume] (μ : Measure (Quotient (AddAction.orbitRel G α))) [AddQuotientMeasureEqMeasurePreimage volume μ] : SigmaFinite μ

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