ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>t : Set α<GOAL>∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>t : Set α<GOAL>∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>ν : MeasureTheory.Measure α<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>t : Set α<GOAL>ν t = ∑' (g : G), ν (t ∩ g • s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>ν : MeasureTheory.Measure α<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>t : Set α<GOAL>ν t = ∑' (g : G), ν (t ∩ (g +ᵥ s))
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>t : Set α<GOAL>μ t = ∑' (g : G), μ (t ∩ g • s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>t : Set α<GOAL>μ t = ∑' (g : G), μ (t ∩ (g +ᵥ s))
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>t : Set α<GOAL>μ t = ∑' (g : G), μ ((g +ᵥ t) ∩ s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>t : Set α<GOAL>μ t = ∑' (g : G), μ (g • t ∩ s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g • t = t<VAR>hts : μ (t ∩ s) = 0<GOAL>μ t = 0
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g +ᵥ t = t<VAR>hts : μ (t ∩ s) = 0<GOAL>μ t = 0
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>Finite G<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g +ᵥ t =ᵐ[μ] t<GOAL>μ t = Nat.card G • μ (t ∩ s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>Finite G<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g • t =ᵐ[μ] t<GOAL>μ t = Nat.card G • μ (t ∩ s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsFundamentalDomain G t μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsAddFundamentalDomain G t μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsAddFundamentalDomain G t μ<VAR>A : Set α<VAR>hA₀ : MeasurableSet A<VAR>hA : ∀ (g : G), (fun x => g +ᵥ x) ⁻¹' A = A<GOAL>μ (A ∩ s) = μ (A ∩ t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsFundamentalDomain G t μ<VAR>A : Set α<VAR>hA₀ : MeasurableSet A<VAR>hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A<GOAL>μ (A ∩ s) = μ (A ∩ t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsFundamentalDomain G t μ<GOAL>μ s = μ t
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsAddFundamentalDomain G t μ<GOAL>μ s = μ t
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>β : Type u_6<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsAddFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>β : Type u_6<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsFundamentalDomain G t μ<VAR>f : α → β<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsAddFundamentalDomain G t μ<VAR>f : α → E<VAR>hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x<GOAL>MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral f (μ.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsFundamentalDomain G t μ<VAR>f : α → E<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>MeasureTheory.HasFiniteIntegral f (μ.restrict s) ↔ MeasureTheory.HasFiniteIntegral f (μ.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsFundamentalDomain G t μ<VAR>f : α → E<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsAddFundamentalDomain G t μ<VAR>f : α → E<VAR>hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x<GOAL>MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>ν : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f ν<GOAL>∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>ν : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f ν<GOAL>∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂ν
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g • s, f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g⁻¹ • x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (-g +ᵥ x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g • x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g +ᵥ x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α → E<VAR>t : Set α<VAR>hf : MeasureTheory.IntegrableOn f t μ<GOAL>∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ (g +ᵥ s), f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α → E<VAR>t : Set α<VAR>hf : MeasureTheory.IntegrableOn f t μ<GOAL>∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α → E<VAR>t : Set α<VAR>hf : MeasureTheory.IntegrableOn f t μ<GOAL>∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α → E<VAR>t : Set α<VAR>hf : MeasureTheory.IntegrableOn f t μ<GOAL>∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsFundamentalDomain G t μ<VAR>f : α → E<VAR>hf : ∀ (g : G) (x : α), f (g • x) = f x<GOAL>∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>E : Type u_5<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>NormedSpace ℝ E<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.IsAddFundamentalDomain G t μ<VAR>f : α → E<VAR>hf : ∀ (g : G) (x : α), f (g +ᵥ x) = f x<GOAL>∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • t ∩ s)<GOAL>μ t ≤ μ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ht : MeasureTheory.NullMeasurableSet t μ<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on fun g => (g +ᵥ t) ∩ s)<GOAL>μ t ≤ μ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>htm : MeasureTheory.NullMeasurableSet t μ<VAR>ht : μ s < μ t<GOAL>∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 0 ∧ g +ᵥ x = y
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s t : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>htm : MeasureTheory.NullMeasurableSet t μ<VAR>ht : μ s < μ t<GOAL>∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 1 ∧ g • x = y
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ +ᵥ x) = f x<GOAL>essSup f (μ.restrict s) = essSup f μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>Countable G<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (γ : G) (x : α), f (γ • x) = f x<GOAL>essSup f (μ.restrict s) = essSup f μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ MeasureTheory.fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 1 ∧ x ∈ g • s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ MeasureTheory.addFundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 0 ∧ x ∈ g +ᵥ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ MeasureTheory.addFundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 0 → x ∉ g +ᵥ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ MeasureTheory.fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>MeasureTheory.addFundamentalFrontier G s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>MeasureTheory.fundamentalFrontier G s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>MeasureTheory.fundamentalInterior G s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>MeasureTheory.addFundamentalInterior G s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>Disjoint (MeasureTheory.fundamentalInterior G s) (MeasureTheory.fundamentalFrontier G s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>Disjoint (MeasureTheory.addFundamentalInterior G s) (MeasureTheory.addFundamentalFrontier G s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>MeasureTheory.addFundamentalInterior G s ∪ MeasureTheory.addFundamentalFrontier G s = s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>MeasureTheory.fundamentalInterior G s ∪ MeasureTheory.fundamentalFrontier G s = s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>MeasureTheory.addFundamentalFrontier G s ∪ MeasureTheory.addFundamentalInterior G s = s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>MeasureTheory.fundamentalFrontier G s ∪ MeasureTheory.fundamentalInterior G s = s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>s \ MeasureTheory.addFundamentalInterior G s = MeasureTheory.addFundamentalFrontier G s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>s \ MeasureTheory.fundamentalInterior G s = MeasureTheory.fundamentalFrontier G s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>s \ MeasureTheory.fundamentalFrontier G s = MeasureTheory.fundamentalInterior G s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>s \ MeasureTheory.addFundamentalFrontier G s = MeasureTheory.addFundamentalInterior G s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>AddGroup H<VAR>AddAction H α<VAR>VAddCommClass H G α<VAR>g : H<GOAL>MeasureTheory.addFundamentalFrontier G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalFrontier G s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>Group H<VAR>MulAction H α<VAR>SMulCommClass H G α<VAR>g : H<GOAL>MeasureTheory.fundamentalFrontier G (g • s) = g • MeasureTheory.fundamentalFrontier G s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>Group H<VAR>MulAction H α<VAR>SMulCommClass H G α<VAR>g : H<GOAL>MeasureTheory.fundamentalInterior G (g • s) = g • MeasureTheory.fundamentalInterior G s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>AddGroup H<VAR>AddAction H α<VAR>VAddCommClass H G α<VAR>g : H<GOAL>MeasureTheory.addFundamentalInterior G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalInterior G s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<GOAL>Pairwise (Disjoint on fun g => g +ᵥ MeasureTheory.addFundamentalInterior G s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<GOAL>Pairwise (Disjoint on fun g => g • MeasureTheory.fundamentalInterior G s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalFrontier G s) μ