ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>NormedSpace 𝕝 F<VAR>IsScalarTower 𝕜 𝕝 F<VAR>f : E → 𝕝<VAR>g : E → F<VAR>z : E<VAR>hf : AnalyticAt 𝕜 f z<VAR>hg : AnalyticAt 𝕜 g z<GOAL>AnalyticAt 𝕜 (fun x => f x • g x) z
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>NormedSpace 𝕝 F<VAR>IsScalarTower 𝕜 𝕝 F<VAR>f : E → 𝕝<VAR>g : E → F<VAR>s : Set E<VAR>hf : AnalyticOn 𝕜 f s<VAR>hg : AnalyticOn 𝕜 g s<GOAL>AnalyticOn 𝕜 (fun x => f x • g x) s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>A : Type u_8<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>f g : E → A<VAR>z : E<VAR>hf : AnalyticAt 𝕜 f z<VAR>hg : AnalyticAt 𝕜 g z<GOAL>AnalyticAt 𝕜 (fun x => f x * g x) z
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>A : Type u_8<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>f g : E → A<VAR>s : Set E<VAR>hf : AnalyticOn 𝕜 f s<VAR>hg : AnalyticOn 𝕜 g s<GOAL>AnalyticOn 𝕜 (fun x => f x * g x) s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>A : Type u_8<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>f : E → A<VAR>z : E<VAR>hf : AnalyticAt 𝕜 f z<VAR>n : ℕ<GOAL>AnalyticAt 𝕜 (fun x => f x ^ n) z
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>A : Type u_8<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>f : E → A<VAR>s : Set E<VAR>hf : AnalyticOn 𝕜 f s<VAR>n : ℕ<GOAL>AnalyticOn 𝕜 (fun x => f x ^ n) s
<VAR>𝕜 : Type u_9<VAR>A : Type u_10<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>NormOneClass A<VAR>n : ℕ<GOAL>‖formalMultilinearSeries_geometric 𝕜 A n‖ = 1
<VAR>𝕜 : Type u_10<VAR>NontriviallyNormedField 𝕜<VAR>A : Type u_9<VAR>NormedRing A<VAR>NormOneClass A<VAR>NormedAlgebra 𝕜 A<GOAL>(formalMultilinearSeries_geometric 𝕜 A).radius = 1
<VAR>𝕜 : Type u_9<VAR>𝕝 : Type u_10<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<GOAL>HasFPowerSeriesOnBall (fun x => (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>𝕝 : Type u_9<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<GOAL>AnalyticAt 𝕜 (fun x => (1 - x)⁻¹) 0
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>z : 𝕝<VAR>hz : z ≠ 0<GOAL>AnalyticAt 𝕜 Inv.inv z
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<GOAL>AnalyticOn 𝕜 (fun z => z⁻¹) {z | z ≠ 0}
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>f : E → 𝕝<VAR>x : E<VAR>fa : AnalyticAt 𝕜 f x<VAR>f0 : f x ≠ 0<GOAL>AnalyticAt 𝕜 (fun x => (f x)⁻¹) x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>f : E → 𝕝<VAR>s : Set E<VAR>fa : AnalyticOn 𝕜 f s<VAR>f0 : ∀ x ∈ s, f x ≠ 0<GOAL>AnalyticOn 𝕜 (fun x => (f x)⁻¹) s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>f g : E → 𝕝<VAR>x : E<VAR>fa : AnalyticAt 𝕜 f x<VAR>ga : AnalyticAt 𝕜 g x<VAR>g0 : g x ≠ 0<GOAL>AnalyticAt 𝕜 (fun x => f x / g x) x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕝 : Type u_7<VAR>NontriviallyNormedField 𝕝<VAR>NormedAlgebra 𝕜 𝕝<VAR>f g : E → 𝕝<VAR>s : Set E<VAR>fa : AnalyticOn 𝕜 f s<VAR>ga : AnalyticOn 𝕜 g s<VAR>g0 : ∀ x ∈ s, g x ≠ 0<GOAL>AnalyticOn 𝕜 (fun x => f x / g x) s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>c : E<VAR>N : Finset α<VAR>h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∑ n ∈ N, f n z) c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>s : Set E<VAR>N : Finset α<VAR>h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s<GOAL>AnalyticOn 𝕜 (fun z => ∑ n ∈ N, f n z) s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>A : Type u_9<VAR>NormedCommRing A<VAR>NormedAlgebra 𝕜 A<VAR>f : α → E → A<VAR>c : E<VAR>N : Finset α<VAR>h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∏ n ∈ N, f n z) c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>A : Type u_9<VAR>NormedCommRing A<VAR>NormedAlgebra 𝕜 A<VAR>f : α → E → A<VAR>s : Set E<VAR>N : Finset α<VAR>h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s<GOAL>AnalyticOn 𝕜 (fun z => ∏ n ∈ N, f n z) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<GOAL>T.IsSymmetric ↔ sesqFormOfInner.IsSelfAdjoint T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x y : E<GOAL>(starRingEnd 𝕜) ⟪T x, y⟫_𝕜 = ⟪T y, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>hT : (↑T).IsSymmetric<VAR>x y : E<GOAL>⟪T x, y⟫_𝕜 = ⟪x, T y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>LinearMap.IsSymmetric 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>LinearMap.id.IsSymmetric
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T S : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>hS : S.IsSymmetric<GOAL>(T + S).IsSymmetric
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>Continuous ⇑T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>hT : (↑T).IsSymmetric<VAR>x : E<GOAL>↑(T.reApplyInnerSelf x) = ⟪T x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>V : Submodule 𝕜 E<VAR>hV : ∀ v ∈ V, T v ∈ V<GOAL>(T.restrict hV).IsSymmetric
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>(↑ℝ T).IsSymmetric
<VAR>V : Type u_6<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℂ V<VAR>T : V →ₗ[ℂ] V<GOAL>T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x y : E<GOAL>⟪T x, y⟫_𝕜 = (⟪T (x + y), x + y⟫_𝕜 - ⟪T (x - y), x - y⟫_𝕜 - RCLike.I * ⟪T (x + RCLike.I • y), x + RCLike.I • y⟫_𝕜 + RCLike.I * ⟪T (x - RCLike.I • y), x - RCLike.I • y⟫_𝕜) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>(∀ (x : E), ⟪T x, x⟫_𝕜 = 0) ↔ T = 0
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Zero G<VAR>VAdd G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.IsAddFundamentalDomain G s μ<GOAL>∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Zero G<VAR>VAdd G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.IsAddFundamentalDomain G s μ<GOAL>Pairwise (MeasureTheory.AEDisjoint μ on fun g => g +ᵥ s)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Zero G<VAR>VAdd G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.IsAddFundamentalDomain G s μ<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>One G<VAR>SMul G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.IsFundamentalDomain G s μ<GOAL>Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • s)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>One G<VAR>SMul G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.IsFundamentalDomain G s μ<GOAL>MeasureTheory.NullMeasurableSet s μ
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>One G<VAR>SMul G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.IsFundamentalDomain G s μ<GOAL>∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ 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>h_meas : MeasureTheory.NullMeasurableSet s μ<VAR>h_exists : ∀ (x : α), ∃! g, g • x ∈ s<GOAL>MeasureTheory.IsFundamentalDomain 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>h_meas : MeasureTheory.NullMeasurableSet s μ<VAR>h_exists : ∀ (x : α), ∃! g, g +ᵥ x ∈ s<GOAL>MeasureTheory.IsAddFundamentalDomain 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>h_meas : MeasureTheory.NullMeasurableSet s μ<VAR>h_ae_covers : ∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s<VAR>h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ<GOAL>MeasureTheory.IsAddFundamentalDomain 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>h_meas : MeasureTheory.NullMeasurableSet s μ<VAR>h_ae_covers : ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ<GOAL>MeasureTheory.IsFundamentalDomain 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>MeasureTheory.IsFiniteMeasure μ<VAR>Countable G<VAR>h_meas : MeasureTheory.NullMeasurableSet s μ<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s<VAR>h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ<VAR>h_measure_univ_le : μ Set.univ ≤ ∑' (g : G), μ (g +ᵥ s)<GOAL>MeasureTheory.IsAddFundamentalDomain 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>MeasureTheory.IsFiniteMeasure μ<VAR>Countable G<VAR>h_meas : MeasureTheory.NullMeasurableSet s μ<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>h_measure_univ_le : μ Set.univ ≤ ∑' (g : G), μ (g • s)<GOAL>MeasureTheory.IsFundamentalDomain 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>h : MeasureTheory.IsFundamentalDomain G s μ<GOAL>⋃ g, g • s =ᵐ[μ] Set.univ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<GOAL>⋃ g, g +ᵥ s =ᵐ[μ] Set.univ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>hμ : μ ≠ 0<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<GOAL>μ s ≠ 0
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>hμ : μ ≠ 0<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<GOAL>μ s ≠ 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>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>ν : MeasureTheory.Measure α<VAR>hle : ν ≪ μ<GOAL>MeasureTheory.IsAddFundamentalDomain 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>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>ν : MeasureTheory.Measure α<VAR>hle : ν ≪ μ<GOAL>MeasureTheory.IsFundamentalDomain G s ν
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup G<VAR>AddGroup H<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>AddAction H β<VAR>MeasurableSpace β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : β → α<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f ν μ<VAR>e : G → H<VAR>he : Function.Bijective e<VAR>hef : ∀ (g : G), Function.Semiconj f (fun x => e g +ᵥ x) fun x => g +ᵥ x<GOAL>MeasureTheory.IsAddFundamentalDomain H (f ⁻¹' s) ν
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group G<VAR>Group H<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>MulAction H β<VAR>MeasurableSpace β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : β → α<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving f ν μ<VAR>e : G → H<VAR>he : Function.Bijective e<VAR>hef : ∀ (g : G), Function.Semiconj f (fun x => e g • x) fun x => g • x<GOAL>MeasureTheory.IsFundamentalDomain H (f ⁻¹' s) ν
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group G<VAR>Group H<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>MulAction H β<VAR>MeasurableSpace β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>f : α ≃ β<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving (⇑f.symm) ν μ<VAR>e : H ≃ G<VAR>hef : ∀ (g : H), Function.Semiconj (⇑f) (fun x => e g • x) fun x => g • x<GOAL>MeasureTheory.IsFundamentalDomain H (⇑f '' s) ν
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup G<VAR>AddGroup H<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>AddAction H β<VAR>MeasurableSpace β<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>f : α ≃ β<VAR>hf : MeasureTheory.Measure.QuasiMeasurePreserving (⇑f.symm) ν μ<VAR>e : H ≃ G<VAR>hef : ∀ (g : H), Function.Semiconj (⇑f) (fun x => e g +ᵥ x) fun x => g +ᵥ x<GOAL>MeasureTheory.IsAddFundamentalDomain H (⇑f '' 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>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>hν : ν ≪ μ<GOAL>Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ +ᵥ s) (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>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<GOAL>Pairwise fun g₁ g₂ => MeasureTheory.AEDisjoint ν (g₁ • s) (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>G' : Type u_6<VAR>Group G'<VAR>MulAction G' α<VAR>MeasurableSpace G'<VAR>MeasurableSMul G' α<VAR>MeasureTheory.SMulInvariantMeasure G' α μ<VAR>SMulCommClass G' G α<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>g : G'<GOAL>MeasureTheory.IsFundamentalDomain G (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>G' : Type u_6<VAR>AddGroup G'<VAR>AddAction G' α<VAR>MeasurableSpace G'<VAR>MeasurableVAdd G' α<VAR>MeasureTheory.VAddInvariantMeasure G' α μ<VAR>VAddCommClass G' G α<VAR>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>g : G'<GOAL>MeasureTheory.IsAddFundamentalDomain G (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>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>g : G<GOAL>MeasureTheory.NullMeasurableSet (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>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>g : G<GOAL>MeasureTheory.NullMeasurableSet (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>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>g : G<VAR>t : Set α<GOAL>(μ.restrict t).restrict (g +ᵥ s) = μ.restrict ((g +ᵥ s) ∩ t)
<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>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>g : G<VAR>t : Set α<GOAL>(μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t)
<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>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>g : G<GOAL>MeasureTheory.IsFundamentalDomain G (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>h : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>g : G<GOAL>MeasureTheory.IsAddFundamentalDomain G (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ν : ν ≪ μ<GOAL>(MeasureTheory.Measure.sum fun g => ν.restrict (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>ν : MeasureTheory.Measure α<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<GOAL>(MeasureTheory.Measure.sum fun g => ν.restrict (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>ν : MeasureTheory.Measure α<VAR>h : MeasureTheory.IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν
<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>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f x ∂ν
<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 μ<GOAL>(MeasureTheory.Measure.sum fun g => μ.restrict (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 μ<GOAL>(MeasureTheory.Measure.sum fun g => μ.restrict (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>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ
<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∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g +ᵥ s, f 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∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g⁻¹ • x) ∂μ
<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∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in 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∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g • x) ∂μ
<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∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in 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 t ∩ g • s, f x ∂μ
<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 t ∩ (g +ᵥ s), f x ∂μ