case pos
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in t, f x ∂μ

case neg
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in t, f x ∂μ
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in t, f x ∂μ
by_cases hfs : IntegrableOn f s μ
case pos
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in t, f x ∂μ
case pos
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in t, f x ∂μ
have hft : IntegrableOn f t μ := by rwa [ht.integrableOn_iff hs hf]
no goals
case pos
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in t, f x ∂μ
calc
  (∫ x in s, f x ∂μ) = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ := ht.set_integral_eq_tsum hfs
  _ = ∑' g : G, ∫ x in g • t ∩ s, f (g⁻¹ • x) ∂μ := by simp only [hf, inter_comm]
  _ = ∫ x in t, f x ∂μ := (hs.set_integral_eq_tsum' hft).symm
no goals
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s
⊢ IntegrableOn f t
rwa [ht.integrableOn_iff hs hf]
no goals
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ (∑' (g : G), ∫ (x : α) in s ∩ g • t, f x ∂μ) = ∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ
simp only [hf, inter_comm]
case neg
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s
⊢ ¬Integrable fun x => f x
case neg
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s
⊢ (∫ (x : α) in s, f x ∂μ) = ∫ (x : α) in t, f x ∂μ
rw [integral_undef hfs, integral_undef]
no goals
case neg
G : Type u_1
H : Type ?u.410725
α : Type u_2
β : Type ?u.410731
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
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s
⊢ ¬Integrable fun x => f x
rwa [hs.integrableOn_iff ht hf] at hfs