Loogle!
Result
Found 380 definitions whose name contains "fundamental". Of these, only the first 200 are shown.
- Ordinal.IsFundamentalSequence 📋 Mathlib.SetTheory.Cardinal.Cofinality
(a o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}) : Prop - Ordinal.IsFundamentalSequence.blsub_eq 📋 Mathlib.SetTheory.Cardinal.Cofinality
{a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : o.blsub f = a - Ordinal.IsFundamentalSequence.cof_eq 📋 Mathlib.SetTheory.Cardinal.Cofinality
{a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : a.cof.ord = o - Ordinal.IsFundamentalSequence.id_of_le_cof 📋 Mathlib.SetTheory.Cardinal.Cofinality
{o : Ordinal.{u}} (h : o ≤ o.cof.ord) : o.IsFundamentalSequence o fun a x => a - Ordinal.IsFundamentalSequence.zero 📋 Mathlib.SetTheory.Cardinal.Cofinality
{f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}} : Ordinal.IsFundamentalSequence 0 0 f - Ordinal.IsFundamentalSequence.succ 📋 Mathlib.SetTheory.Cardinal.Cofinality
{o : Ordinal.{u}} : (Order.succ o).IsFundamentalSequence 1 fun x x => o - Ordinal.exists_fundamental_sequence 📋 Mathlib.SetTheory.Cardinal.Cofinality
(a : Ordinal.{u}) : ∃ f, a.IsFundamentalSequence a.cof.ord f - Ordinal.IsFundamentalSequence.lt 📋 Mathlib.SetTheory.Cardinal.Cofinality
{a o : Ordinal.{u_1}} {s : (p : Ordinal.{u_1}) → p < o → Ordinal.{u_1}} (h : a.IsFundamentalSequence o s) {p : Ordinal.{u_1}} (hp : p < o) : s p hp < a - Ordinal.IsNormal.isFundamentalSequence 📋 Mathlib.SetTheory.Cardinal.Cofinality
{f : Ordinal.{u} → Ordinal.{u}} (hf : Ordinal.IsNormal f) {a o : Ordinal.{u}} (ha : a.IsLimit) {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hg : a.IsFundamentalSequence o g) : (f a).IsFundamentalSequence o fun b hb => f (g b hb) - Ordinal.IsFundamentalSequence.monotone 📋 Mathlib.SetTheory.Cardinal.Cofinality
{a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {i j : Ordinal.{u}} (hi : i < o) (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj - Ordinal.IsFundamentalSequence.strict_mono 📋 Mathlib.SetTheory.Cardinal.Cofinality
{a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {i j : Ordinal.{u}} (hi : i < o) (hj : j < o) : i < j → f i hi < f j hj - Ordinal.IsFundamentalSequence.ord_cof 📋 Mathlib.SetTheory.Cardinal.Cofinality
{a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯ - Ordinal.IsFundamentalSequence.trans 📋 Mathlib.SetTheory.Cardinal.Cofinality
{a o o' : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}} (hg : o.IsFundamentalSequence o' g) : a.IsFundamentalSequence o' fun i hi => f (g i hi) ⋯ - MeasureTheory.HasAddFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_6) (α : Type u_7) [Zero G] [VAdd G α] [MeasurableSpace α] (ν : MeasureTheory.Measure α := by volume_tac) : Prop - MeasureTheory.HasFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_6) (α : Type u_7) [One G] [SMul G α] [MeasurableSpace α] (ν : MeasureTheory.Measure α := by volume_tac) : Prop - MeasureTheory.addFundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Set α - MeasureTheory.addFundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Set α - MeasureTheory.fundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Set α - MeasureTheory.fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Set α - MeasureTheory.IsAddFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_2} [Zero G] [VAdd G α] [MeasurableSpace α] (s : Set α) (μ : MeasureTheory.Measure α := by volume_tac) : Prop - MeasureTheory.IsFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] (s : Set α) (μ : MeasureTheory.Measure α := by volume_tac) : Prop - MeasureTheory.addFundamentalFrontier_subset 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} : MeasureTheory.addFundamentalFrontier G s ⊆ s - MeasureTheory.addFundamentalInterior_subset 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} : MeasureTheory.addFundamentalInterior G s ⊆ s - MeasureTheory.fundamentalFrontier_subset 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} : MeasureTheory.fundamentalFrontier G s ⊆ s - MeasureTheory.fundamentalInterior_subset 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} : MeasureTheory.fundamentalInterior G s ⊆ s - MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 μ - MeasureTheory.IsFundamentalDomain.nullMeasurableSet 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 μ - MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_6} {α : Type u_7} {inst✝ : Zero G} {inst✝¹ : VAdd G α} {inst✝² : MeasurableSpace α} {ν : autoParam (MeasureTheory.Measure α) _auto✝} [self : MeasureTheory.HasAddFundamentalDomain G α ν] : ∃ s, MeasureTheory.IsAddFundamentalDomain G s ν - MeasureTheory.HasAddFundamentalDomain.mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_6} {α : Type u_7} [Zero G] [VAdd G α] [MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} (ExistsIsAddFundamentalDomain : ∃ s, MeasureTheory.IsAddFundamentalDomain G s ν) : MeasureTheory.HasAddFundamentalDomain G α ν - MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_6} {α : Type u_7} {inst✝ : One G} {inst✝¹ : SMul G α} {inst✝² : MeasurableSpace α} {ν : autoParam (MeasureTheory.Measure α) _auto✝} [self : MeasureTheory.HasFundamentalDomain G α ν] : ∃ s, MeasureTheory.IsFundamentalDomain G s ν - MeasureTheory.HasFundamentalDomain.mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_6} {α : Type u_7} [One G] [SMul G α] [MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} (ExistsIsFundamentalDomain : ∃ s, MeasureTheory.IsFundamentalDomain G s ν) : MeasureTheory.HasFundamentalDomain G α ν - MeasureTheory.addFundamentalFrontier_union_addFundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : MeasureTheory.addFundamentalFrontier G s ∪ MeasureTheory.addFundamentalInterior G s = s - MeasureTheory.addFundamentalInterior_union_addFundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : MeasureTheory.addFundamentalInterior G s ∪ MeasureTheory.addFundamentalFrontier G s = s - MeasureTheory.fundamentalFrontier_union_fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : MeasureTheory.fundamentalFrontier G s ∪ MeasureTheory.fundamentalInterior G s = s - MeasureTheory.fundamentalInterior_union_fundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : MeasureTheory.fundamentalInterior G s ∪ MeasureTheory.fundamentalFrontier G s = s - MeasureTheory.sdiff_addFundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : s \ MeasureTheory.addFundamentalFrontier G s = MeasureTheory.addFundamentalInterior G s - MeasureTheory.sdiff_addFundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : s \ MeasureTheory.addFundamentalInterior G s = MeasureTheory.addFundamentalFrontier G s - MeasureTheory.sdiff_fundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : s \ MeasureTheory.fundamentalFrontier G s = MeasureTheory.fundamentalInterior G s - MeasureTheory.sdiff_fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : s \ MeasureTheory.fundamentalInterior G s = MeasureTheory.fundamentalFrontier G s - MeasureTheory.IsAddFundamentalDomain.aedisjoint 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 +ᵥ s) - MeasureTheory.IsFundamentalDomain.aedisjoint 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 • s) - MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Disjoint (MeasureTheory.addFundamentalInterior G s) (MeasureTheory.addFundamentalFrontier G s) - MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Disjoint (MeasureTheory.fundamentalInterior G s) (MeasureTheory.fundamentalFrontier G s) - MeasureTheory.IsAddFundamentalDomain.ae_covers 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 +ᵥ x ∈ s - MeasureTheory.IsFundamentalDomain.ae_covers 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 • x ∈ s - MeasureTheory.IsAddFundamentalDomain.hasAddFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 α ν - MeasureTheory.IsFundamentalDomain.hasFundamentalDomain 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 α ν - MeasureTheory.NullMeasurableSet.addFundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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) μ - MeasureTheory.NullMeasurableSet.addFundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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) μ - MeasureTheory.NullMeasurableSet.fundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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) μ - MeasureTheory.NullMeasurableSet.fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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) μ - MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsAddFundamentalDomain.mono 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ν - MeasureTheory.IsFundamentalDomain.mono 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ν - MeasureTheory.IsAddFundamentalDomain.mk' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 +ᵥ x ∈ s) : MeasureTheory.IsAddFundamentalDomain G s μ - MeasureTheory.IsFundamentalDomain.mk' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 • x ∈ s) : MeasureTheory.IsFundamentalDomain G s μ - MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.pairwise_disjoint_addFundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : Pairwise (Disjoint on fun g => g +ᵥ MeasureTheory.addFundamentalInterior G s) - MeasureTheory.pairwise_disjoint_fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : Pairwise (Disjoint on fun g => g • MeasureTheory.fundamentalInterior G s) - MeasureTheory.mem_addFundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.mem_fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s μ) : ⋃ g, g +ᵥ s =ᵐ[μ] Set.univ - MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) : ⋃ g, g • s =ᵐ[μ] Set.univ - MeasureTheory.mem_addFundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {x : α} : x ∈ MeasureTheory.addFundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 0 ∧ x ∈ g +ᵥ s - MeasureTheory.mem_fundamentalFrontier 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {x : α} : x ∈ MeasureTheory.fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 1 ∧ x ∈ g • s - MeasureTheory.addFundamentalFrontier.eq_1 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : MeasureTheory.addFundamentalFrontier G s = s ∩ ⋃ g, ⋃ (_ : g ≠ 0), g +ᵥ s - MeasureTheory.addFundamentalInterior.eq_1 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [AddGroup G] [AddAction G α] (s : Set α) : MeasureTheory.addFundamentalInterior G s = s \ ⋃ g, ⋃ (_ : g ≠ 0), g +ᵥ s - MeasureTheory.fundamentalFrontier.eq_1 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : MeasureTheory.fundamentalFrontier G s = s ∩ ⋃ g, ⋃ (_ : g ≠ 1), g • s - MeasureTheory.fundamentalInterior.eq_1 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(G : Type u_1) {α : Type u_3} [Group G] [MulAction G α] (s : Set α) : MeasureTheory.fundamentalInterior G s = s \ ⋃ g, ⋃ (_ : g ≠ 1), g • s - MeasureTheory.IsAddFundamentalDomain.mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_2} [Zero G] [VAdd G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (nullMeasurableSet : MeasureTheory.NullMeasurableSet s μ) (ae_covers : ∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s) (aedisjoint : Pairwise (MeasureTheory.AEDisjoint μ on fun g => g +ᵥ s)) : MeasureTheory.IsAddFundamentalDomain G s μ - MeasureTheory.IsFundamentalDomain.mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_2} [One G] [SMul G α] [MeasurableSpace α] {s : Set α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (nullMeasurableSet : MeasureTheory.NullMeasurableSet s μ) (ae_covers : ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s) (aedisjoint : Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • s)) : MeasureTheory.IsFundamentalDomain G s μ - MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 𝓕) μ - MeasureTheory.IsAddFundamentalDomain.measure_ne_zero 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 𝓕) μ - MeasureTheory.IsFundamentalDomain.measure_ne_zero 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) μ - MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) μ - MeasureTheory.IsFundamentalDomain.fundamentalInterior 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) μ - MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {μ ν : MeasureTheory.Measure α} (h : MeasureTheory.IsAddFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) : Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ +ᵥ s) (g₂ +ᵥ s) - MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {μ ν : MeasureTheory.Measure α} (h : MeasureTheory.IsFundamentalDomain G s μ) (hν : ν.AbsolutelyContinuous μ) : Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ • s) (g₂ • s) - MeasureTheory.addFundamentalFrontier_vadd 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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 - MeasureTheory.addFundamentalInterior_vadd 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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 - MeasureTheory.fundamentalFrontier_smul 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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 - MeasureTheory.fundamentalInterior_smul 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
(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 - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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)) - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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)) - MeasureTheory.IsAddFundamentalDomain.sum_restrict 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 => μ.restrict (g +ᵥ s)) = μ - MeasureTheory.IsFundamentalDomain.sum_restrict 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 => μ.restrict (g • s)) = μ - MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsFundamentalDomain.covolume_eq_volume 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsFundamentalDomain.projection_respects_measure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 => ν.restrict (g +ᵥ s)) = ν - MeasureTheory.IsAddFundamentalDomain.vadd 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) μ - MeasureTheory.IsFundamentalDomain.smul 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) μ - MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 => ν.restrict (g • s)) = ν - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsAddFundamentalDomain.measure_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s 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 - MeasureTheory.IsFundamentalDomain.measure_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s 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 - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 μ - MeasureTheory.IsFundamentalDomain.essSup_measure_restrict 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 μ - MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 μ - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂ν - MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂ν - MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsAddFundamentalDomain.restrict_restrict 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsFundamentalDomain.restrict_restrict 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ν μ - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ν μ - MeasureTheory.IsAddFundamentalDomain.integrableOn_iff 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s 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 μ - MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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)) - MeasureTheory.IsAddFundamentalDomain.preimage_of_equiv 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ν - MeasureTheory.IsFundamentalDomain.integrableOn_iff 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s 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 μ - MeasureTheory.IsFundamentalDomain.measure_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsFundamentalDomain.measure_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsFundamentalDomain.preimage_of_equiv 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ν - MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s 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 ∂μ - MeasureTheory.IsFundamentalDomain.setLIntegral_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s 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 ∂μ - MeasureTheory.IsFundamentalDomain.set_lintegral_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s 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 ∂μ - MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s 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) - MeasureTheory.IsAddFundamentalDomain.vadd_of_comm 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) μ - MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s 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) - MeasureTheory.IsFundamentalDomain.smul_of_comm 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) μ - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.integral_eq_tsum'' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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)) - MeasureTheory.IsAddFundamentalDomain.measure_zero_of_invariant 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 - MeasureTheory.IsAddFundamentalDomain.aEStronglyMeasurable_on_iff 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s 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) - MeasureTheory.IsFundamentalDomain.aEStronglyMeasurable_on_iff 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s 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) - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsFundamentalDomain.integral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsAddFundamentalDomain.mk'' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 +ᵥ 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 μ - MeasureTheory.IsFundamentalDomain.mk'' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 • 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 μ - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.integral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s 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 +ᵥ t) ∩ s)) : μ t ≤ μ s - MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s 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 • t ∩ s)) : μ t ≤ μ s - MeasureTheory.IsAddFundamentalDomain.setIntegral_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {E : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s 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 ∂μ - MeasureTheory.IsFundamentalDomain.setIntegral_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s 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 ∂μ - MeasureTheory.IsFundamentalDomain.set_integral_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {E : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] [NormedAddCommGroup E] {s 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 ∂μ - MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂ν - MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂ν - MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 ∂μ - MeasureTheory.IsAddFundamentalDomain.measure_set_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s 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) - MeasureTheory.IsFundamentalDomain.measure_set_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s 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) - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [Countable G] [MeasurableSpace G] {s 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) - MeasureTheory.IsFundamentalDomain.quotientMeasure_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [Countable G] [MeasurableSpace G] {s 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) - MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) - MeasureTheory.IsAddFundamentalDomain.image_of_equiv 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ν - MeasureTheory.IsFundamentalDomain.image_of_equiv 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ν - MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s 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 ≠ 0 ∧ g +ᵥ x = y - MeasureTheory.IsFundamentalDomain.exists_ne_one_smul_eq 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {s 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 ≠ 1 ∧ g • x = y - MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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) ∂μ - MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 μ - MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{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 μ - ZSpan.fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) : Set E - ZSpan.fundamentalDomain_measurableSet 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] : MeasurableSet (ZSpan.fundamentalDomain b) - ZSpan.fract_mem_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (x : E) : ZSpan.fract b x ∈ ZSpan.fundamentalDomain b - ZSpan.fundamentalDomain_pi_basisFun 📋 Mathlib.Algebra.Module.ZLattice.Basic
{ι : Type u_2} [Fintype ι] : ZSpan.fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x => Set.Ico 0 1 - ZSpan.measure_fundamentalDomain_ne_zero 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] : μ (ZSpan.fundamentalDomain b) ≠ 0 - ZSpan.fundamentalDomain_subset_parallelepiped 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Fintype ι] : ZSpan.fundamentalDomain b ⊆ parallelepiped ⇑b - ZSpan.fundamentalDomain_isBounded 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Finite ι] [HasSolidNorm K] : Bornology.IsBounded (ZSpan.fundamentalDomain b) - ZSpan.fundamentalDomain_reindex 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {ι' : Type u_4} (e : ι ≃ ι') : ZSpan.fundamentalDomain (b.reindex e) = ZSpan.fundamentalDomain b - ZSpan.fundamentalDomain_ae_parallelepiped 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Fintype ι] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [μ.IsAddHaarMeasure] : ZSpan.fundamentalDomain b =ᵐ[μ] parallelepiped ⇑b - ZSpan.volume_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ (ι → ℝ)) : MeasureTheory.volume (ZSpan.fundamentalDomain b) = ENNReal.ofReal |(Matrix.of ⇑b).det| - ZSpan.measure_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Fintype ι] [DecidableEq ι] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [μ.IsAddHaarMeasure] (b₀ : Basis ι ℝ E) : μ (ZSpan.fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (ZSpan.fundamentalDomain b₀) - ZSpan.isAddFundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) : MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b))) (ZSpan.fundamentalDomain b) μ - ZLattice.isAddFundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{ι : Type u_3} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] [Finite ι] (b : Basis ι ℤ ↥L) [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) : MeasureTheory.IsAddFundamentalDomain (↥L) (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) μ - ZSpan.map_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) : ⇑f '' ZSpan.fundamentalDomain b = ZSpan.fundamentalDomain (b.map f) - ZSpan.isAddFundamentalDomain' 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) [Finite ι] [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) : MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup) (ZSpan.fundamentalDomain b) μ - ZSpan.exist_unique_vadd_mem_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Finite ι] (x : E) : ∃! v, v +ᵥ x ∈ ZSpan.fundamentalDomain b - ZSpan.fundamentalDomain.eq_1 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) : ZSpan.fundamentalDomain b = {m | ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1} - ZSpan.mem_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {m : E} : m ∈ ZSpan.fundamentalDomain b ↔ ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1 - ZSpan.vadd_mem_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
{E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedLinearOrderedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (y : ↥(Submodule.span ℤ (Set.range ⇑b))) (x : E) : y +ᵥ x ∈ ZSpan.fundamentalDomain b ↔ y = -ZSpan.floor b x - ZLattice.covolume_eq_measure_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Covolume
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [MeasureTheory.Measure.IsAddHaarMeasure μ] {F : Set E} (h : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) : ZLattice.covolume L μ = (μ F).toReal - FundamentalGroupoid.termπ 📋 Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
: Lean.ParserDescr
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle
command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?a
If the pattern has parameters, they are matched in any order. Both of these will find
List.map
:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→
and∀
) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin
and tsum
, have "two"
as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _
(if
there were any such lemmas). Metavariables (?a
) are
assigned independently in each filter.
The #lucky
button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 4e1aab0
serving mathlib revision 2d53f5f