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

      abbrev MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq.match_1 {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {s : Set α} :
      ∀ (x : α) (motive : (∃ (g : G), g +ᵥ x s)Prop) (x_1 : ∃ (g : G), g +ᵥ x s), (∀ (g : G) (hg : g +ᵥ x s), motive )motive x_1
      Equations
      • =
      Instances For
        abbrev MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv.match_1 {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {f : βα} (x : β) (motive : (∃ (g : G), g +ᵥ f x s)Prop) :
        ∀ (x_1 : ∃ (g : G), g +ᵥ f x s), (∀ (g : G) (hg : g +ᵥ f x s), motive )motive x_1
        Equations
        • =
        Instances For
          theorem MeasureTheory.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.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.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ν : MeasureTheory.Measure.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ν : MeasureTheory.Measure.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.set_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) (t : Set α) :
          ∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in t (g +ᵥ s), f xμ
          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μ
          theorem MeasureTheory.IsAddFundamentalDomain.set_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) (t : Set α) :
          ∫⁻ (x : α) in t, f xμ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) s, f (-g +ᵥ x)μ
          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)μ
          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

          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.set_lintegral_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.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μ
          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ν : MeasureTheory.Measure.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ν : MeasureTheory.Measure.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.set_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} {t : Set α} (hf : MeasureTheory.IntegrableOn f t μ) :
          ∫ (x : α) in t, f xμ = ∑' (g : G), ∫ (x : α) in t (g +ᵥ s), f xμ
          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μ
          theorem MeasureTheory.IsAddFundamentalDomain.set_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} {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.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)μ
          theorem MeasureTheory.IsAddFundamentalDomain.set_integral_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.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μ

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

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

                              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.

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

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

                              Equations
                              • =