G : Type u_1
H : Type ?u.349531
α : Type u_2
β : Type ?u.349537
E : Type u_3
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : IsFundamentalDomain G s
hν : ν ≪ μ
f : α → E
hf : Integrable f
⊢ Integrable fun x => f x
G : Type u_1
H : Type ?u.349531
α : Type u_2
β : Type ?u.349537
E : Type u_3
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : IsFundamentalDomain G s
hν : ν ≪ μ
f : α → E
hf : Integrable f
⊢ (∫ (x : α), f x ∂ν) = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν
rw [← MeasureTheory.integral_sum_measure, h.sum_restrict_of_ac hν]
G : Type u_1
H : Type ?u.349531
α : Type u_2
β : Type ?u.349537
E : Type u_3
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : IsFundamentalDomain G s
hν : ν ≪ μ
f : α → E
hf : Integrable f
⊢ Integrable fun x => f x
G : Type u_1
H : Type ?u.349531
α : Type u_2
β : Type ?u.349537
E : Type u_3
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : IsFundamentalDomain G s
hν : ν ≪ μ
f : α → E
hf : Integrable f
⊢ Integrable fun x => f x
rw [h.sum_restrict_of_ac hν]
no goals
G : Type u_1
H : Type ?u.349531
α : Type u_2
β : Type ?u.349537
E : Type u_3
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
h : IsFundamentalDomain G s
hν : ν ≪ μ
f : α → E
hf : Integrable f
⊢ Integrable fun x => f x
exact hf