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

theorem MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet {G : Type u_1} {α : Type u_2} [Zero G] [VAdd G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (self : MeasureTheory.IsAddFundamentalDomain G s μ) : MeasureTheory.NullMeasurableSet s μ

theorem MeasureTheory.IsAddFundamentalDomain.ae_covers {G : Type u_1} {α : Type u_2} [Zero G] [VAdd G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (self : MeasureTheory.IsAddFundamentalDomain G s μ) : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g +ᵥ x ∈ s

theorem MeasureTheory.IsAddFundamentalDomain.aedisjoint {G : Type u_1} {α : Type u_2} [Zero G] [VAdd G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (self : MeasureTheory.IsAddFundamentalDomain G s μ) : Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g +ᵥ s)

structure MeasureTheory.IsFundamentalDomain (G : Type u_1) {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] (s : Set α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) : 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 : MeasureTheory.NullMeasurableSet s μ
• ae_covers : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
• aedisjoint : Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g • s)

theorem MeasureTheory.IsFundamentalDomain.nullMeasurableSet {G : Type u_1} {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (self : MeasureTheory.IsFundamentalDomain G s μ) : MeasureTheory.NullMeasurableSet s μ

theorem MeasureTheory.IsFundamentalDomain.ae_covers {G : Type u_1} {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (self : MeasureTheory.IsFundamentalDomain G s μ) : ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s

theorem MeasureTheory.IsFundamentalDomain.aedisjoint {G : Type u_1} {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (self : MeasureTheory.IsFundamentalDomain G s μ) : Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g • s)

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

theorem MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) : ⋃ (g : G), g • s =ᵐ[μ] Set.univ

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

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

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

theorem MeasureTheory.IsFundamentalDomain.mono {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) {ν : MeasureTheory.Measure α} (hle : ν.AbsolutelyContinuous μ) : MeasureTheory.IsFundamentalDomain G 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 α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsAddFundamentalDomain G s μ) {f : β → α} (hf : MeasureTheory.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) : MeasureTheory.IsAddFundamentalDomain H (f ⁻¹' 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 α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsFundamentalDomain G s μ) {f : β → α} (hf : MeasureTheory.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) : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsAddFundamentalDomain G s μ) (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) : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (h : MeasureTheory.IsFundamentalDomain G s μ) (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) : MeasureTheory.IsFundamentalDomain H (⇑f '' s) ν

theorem MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} {G' : Type u_6} [AddGroup G'] [AddAction G' α] [MeasurableSpace G'] [MeasurableVAdd G' α] [MeasureTheory.VAddInvariantMeasure G' α μ] [VAddCommClass G' G α] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (g : G') : MeasureTheory.IsAddFundamentalDomain G (g +ᵥ s) μ

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

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

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

theorem MeasureTheory.IsAddFundamentalDomain.restrict_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] (h : MeasureTheory.IsFundamentalDomain G s μ) (g : G) (t : Set α) : (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t)

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

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

theorem MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s μ) : (MeasureTheory.Measure.sum fun (g : G) => μ.restrict (g +ᵥ s)) = μ

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

theorem MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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.setLIntegral_eq_tsum' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (t : Set α) : μ t = ∑' (g : G), μ ((g +ᵥ t) ∩ s)

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

theorem MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (h : MeasureTheory.IsFundamentalDomain G s μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [Finite G] (h : MeasureTheory.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.measure_eq_card_smul_of_smul_ae_eq_self {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [Finite G] (h : MeasureTheory.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.setLIntegral_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.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.setLIntegral_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.IsFundamentalDomain G t μ) (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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.IsFundamentalDomain G t μ) (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.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_set_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.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_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.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.measure_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.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.aEStronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {β : Type u_6} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.IsAddFundamentalDomain G t μ) {f : α → β} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)

theorem MeasureTheory.IsFundamentalDomain.aEStronglyMeasurable_on_iff {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {β : Type u_6} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.IsFundamentalDomain G t μ) {f : α → β} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable 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 : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.IsAddFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral 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 : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.IsFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral f (μ.restrict 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 : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.IsAddFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x) : MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f 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 : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.IsFundamentalDomain G t μ) {f : α → E} (hf : ∀ (g : G) (x : α), f (g • x) = f x) : MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ

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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (f : α → E) (hf : MeasureTheory.Integrable f ν) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] {ν : MeasureTheory.Measure α} [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) (f : α → E) (hf : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (f : α → E) (hf : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) (f : α → E) (hf : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (f : α → E) (hf : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) (f : α → E) (hf : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s μ) (f : α → E) (hf : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) (f : α → E) (hf : MeasureTheory.Integrable f μ) : ∫ (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t μ) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t μ) : ∫ (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsAddFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t μ) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t μ) : ∫ (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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (h : MeasureTheory.IsFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : MeasureTheory.IntegrableOn f t μ) : ∫ (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} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.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.setIntegral_eq {G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.IsFundamentalDomain G t μ) {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} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [NormedSpace ℝ E] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.IsFundamentalDomain G t μ) {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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (ht : MeasureTheory.NullMeasurableSet t μ) (hd : Pairwise (MeasureTheory.AEDisjoint μ 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} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (ht : MeasureTheory.NullMeasurableSet t μ) (hd : Pairwise (MeasureTheory.AEDisjoint μ 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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsAddFundamentalDomain G s μ) (htm : MeasureTheory.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.exists_ne_one_smul_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.IsFundamentalDomain G s μ) (htm : MeasureTheory.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.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.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.

theorem MeasureTheory.IsFundamentalDomain.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] (hs : MeasureTheory.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.

Interior/frontier of a fundamental domain

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.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.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

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

@[simp]

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

@[simp]

theorem MeasureTheory.mem_fundamentalFrontier {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {x : α} : x ∈ MeasureTheory.fundamentalFrontier 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 ∈ MeasureTheory.addFundamentalInterior 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 ∈ MeasureTheory.fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem MeasureTheory.sdiff_fundamentalFrontier (G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : s \ MeasureTheory.fundamentalFrontier G s = MeasureTheory.fundamentalInterior 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) : MeasureTheory.addFundamentalFrontier G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalFrontier 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) : MeasureTheory.fundamentalFrontier G (g • s) = g • MeasureTheory.fundamentalFrontier 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) : MeasureTheory.addFundamentalInterior G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalInterior 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) : MeasureTheory.fundamentalInterior G (g • s) = g • MeasureTheory.fundamentalInterior G s

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [Countable G] [MeasurableSpace G] {s : Set α} {t : Set α} [MeasureTheory.VAddInvariantMeasure G α μ] [MeasurableVAdd G α] (fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s μ) (fund_dom_t : MeasureTheory.IsAddFundamentalDomain G t μ) : MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s) = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict t)

theorem MeasureTheory.IsFundamentalDomain.quotientMeasure_eq {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [Countable G] [MeasurableSpace G] {s : Set α} {t : Set α} [MeasureTheory.SMulInvariantMeasure G α μ] [MeasurableSMul G α] (fund_dom_s : MeasureTheory.IsFundamentalDomain G s μ) (fund_dom_t : MeasureTheory.IsFundamentalDomain G t μ) : MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s) = MeasureTheory.Measure.map (Quotient.mk (MulAction.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 α] (ν : autoParam (MeasureTheory.Measure α) _auto✝) : 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 α), MeasureTheory.IsAddFundamentalDomain G s ν

theorem MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain {G : Type u_6} {α : Type u_7} [Zero G] [VAdd G α] [MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} [self : MeasureTheory.HasAddFundamentalDomain G α ν] : ∃ (s : Set α), MeasureTheory.IsAddFundamentalDomain G s ν

class MeasureTheory.HasFundamentalDomain (G : Type u_6) (α : Type u_7) [One G] [SMul G α] [MeasurableSpace α] (ν : autoParam (MeasureTheory.Measure α) _auto✝) : 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 α), MeasureTheory.IsFundamentalDomain G s ν

theorem MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain {G : Type u_6} {α : Type u_7} [One G] [SMul G α] [MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} [self : MeasureTheory.HasFundamentalDomain G α ν] : ∃ (s : Set α), MeasureTheory.IsFundamentalDomain G s ν

noncomputable def MeasureTheory.addCovolume (G : Type u_6) (α : Type u_7) [Zero G] [VAdd G α] [MeasurableSpace α] (ν : autoParam (MeasureTheory.Measure α) _auto✝) : 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

noncomputable def MeasureTheory.covolume (G : Type u_6) (α : Type u_7) [One G] [SMul G α] [MeasurableSpace α] (ν : autoParam (MeasureTheory.Measure α) _auto✝) : 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

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

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

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

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

theorem MeasureTheory.IsFundamentalDomain.covolume_eq_volume {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (ν : MeasureTheory.Measure α) [Countable G] [MeasurableSpace G] [MeasurableSMul G α] [MeasureTheory.SMulInvariantMeasure G α ν] {s : Set α} (fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν) : MeasureTheory.covolume G α ν = ν 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} [AddGroup G] [AddAction G α] [MeasurableSpace α] (ν : autoParam (MeasureTheory.Measure α) _auto✝) (μ : MeasureTheory.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 α), MeasureTheory.IsAddFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t)

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

class MeasureTheory.QuotientMeasureEqMeasurePreimage {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (ν : autoParam (MeasureTheory.Measure α) _auto✝) (μ : MeasureTheory.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 α), MeasureTheory.IsFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t)

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

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

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

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

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

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

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

Any two measures satisfying QuotientMeasureEqMeasurePreimage are equal.

theorem MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} {𝓕 : Set α} (h𝓕 : MeasureTheory.IsAddFundamentalDomain G 𝓕 ν) (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))) [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] : MeasureTheory.MeasurePreserving (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict 𝓕) μ

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

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

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

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

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

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

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

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

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

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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableSpace G] [MeasurableVAdd G α] (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))) [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] [hasFun : MeasureTheory.HasAddFundamentalDomain G α ν] (h : MeasureTheory.addCovolume G α ν ≠ ⊤) : MeasureTheory.IsFiniteMeasure μ

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

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} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableSpace G] [MeasurableVAdd G α] (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))) [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.addCovolume G α ν < ⊤

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯