Documentation

Mathlib.MeasureTheory.Group.FundamentalDomain

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

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.

Main declarations #

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

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.

Instances For
    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
    structure MeasureTheory.IsFundamentalDomain (G : Type u_1) {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] (s : Set α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) :

    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.

    Instances For
      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.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) :

      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) :

      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 0MeasureTheory.AEDisjoint μ (g +ᵥ s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ) :

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

      theorem MeasureTheory.IsFundamentalDomain.mk'' {G : Type u_1} {α : Type u_3} [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 1MeasureTheory.AEDisjoint μ (g s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g x) μ μ) :

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

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

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

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

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

      theorem MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq {G : Type u_1} {α : Type u_3} [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.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 μ) :
      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 μ) :
      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 : GH} (he : Function.Bijective e) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g +ᵥ x) fun (x : α) => g +ᵥ x) :
      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 : GH} (he : Function.Bijective e) (hef : ∀ (g : G), Function.Semiconj f (fun (x : β) => e g x) fun (x : α) => g x) :
      theorem MeasureTheory.IsAddFundamentalDomain.image_of_equiv {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [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) :
      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) :
      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.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.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.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.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.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

      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.

      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)

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

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

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

      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.

      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) :
      xt, yt, ∃ (g : G), g 0 g +ᵥ x = y

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

      theorem MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq {G : Type u_1} {α : Type u_3} [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) :
      xt, yt, ∃ (g : G), g 1 g x = y

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

      theorem MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict {G : Type u_1} {α : Type u_3} [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
      Instances For
        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
        Instances For
          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
          Instances For
            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
            Instances For
              @[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 0xg +ᵥ 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 1xg 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) :
              @[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) :
              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)

              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.

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

              Instances

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

                Instances
                  theorem MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain {G : Type u_6} {α : Type u_7} :
                  ∀ {inst : One G} {inst_1 : SMul G α} {inst_2 : 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✝) :

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

                  Equations
                  Instances For
                    noncomputable def MeasureTheory.covolume (G : Type u_6) (α : Type u_7) [One G] [SMul G α] [MeasurableSpace α] (ν : autoParam (MeasureTheory.Measure α) _auto✝) :

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

                    Equations
                    Instances For

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

                      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.

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

                      Instances

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

                        Instances

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

                          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.

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

                          Equations
                          • =