[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
h_meas : NullMeasurableSet s
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : x ∈ (fun g => g • s) a
hxb : x ∈ (fun g => g • s) b
⊢ False
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb 
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
h_meas : NullMeasurableSet s
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : a⁻¹ • x ∈ s
hxb : b⁻¹ • x ∈ s
⊢ False
[PROOFSTEP]
exact hab (inv_injective <| (h_exists x).unique hxa hxb)
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_meas : NullMeasurableSet s
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s
[PROOFSTEP]
replace h_meas : ∀ g : G, NullMeasurableSet (g • s) μ := fun g => by rw [← inv_inv g, ← preimage_smul];
  exact h_meas.preimage (h_qmp g⁻¹)
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_meas : NullMeasurableSet s
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
g : G
⊢ NullMeasurableSet (g • s)
[PROOFSTEP]
rw [← inv_inv g, ← preimage_smul]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_meas : NullMeasurableSet s
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
g : G
⊢ NullMeasurableSet ((fun x => g⁻¹ • x) ⁻¹' s)
[PROOFSTEP]
exact h_meas.preimage (h_qmp g⁻¹)
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s)
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s
[PROOFSTEP]
have h_meas' : NullMeasurableSet {a | ∃ g : G, g • a ∈ s} μ := by rw [← iUnion_smul_eq_setOf_exists];
  exact .iUnion h_meas
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s)
⊢ NullMeasurableSet {a | ∃ g, g • a ∈ s}
[PROOFSTEP]
rw [← iUnion_smul_eq_setOf_exists]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s)
⊢ NullMeasurableSet (⋃ (g : G), g • s)
[PROOFSTEP]
exact .iUnion h_meas
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s)
h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s}
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s
[PROOFSTEP]
rw [ae_iff_measure_eq h_meas', ← iUnion_smul_eq_setOf_exists]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s)
h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s}
⊢ ↑↑μ (⋃ (g : G), g • s) = ↑↑μ univ
[PROOFSTEP]
refine' le_antisymm (measure_mono <| subset_univ _) _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s)
h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s}
⊢ ↑↑μ univ ≤ ↑↑μ (⋃ (g : G), g • s)
[PROOFSTEP]
rw [measure_iUnion₀ aedisjoint h_meas]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : Group H
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MulAction H β
inst✝³ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)
h_measure_univ_le : ↑↑μ univ ≤ ∑' (g : G), ↑↑μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s)
h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s}
⊢ ↑↑μ univ ≤ ∑' (i : G), ↑↑μ (i • s)
[PROOFSTEP]
exact h_measure_univ_le
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : β → α
hf : QuasiMeasurePreserving f
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
x : β
x✝ : ∃ g, g • f x ∈ s
g : G
hg : g • f x ∈ s
⊢ e g • x ∈ f ⁻¹' s
[PROOFSTEP]
rwa [mem_preimage, hef g x]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : β → α
hf : QuasiMeasurePreserving f
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
a b : H
hab : a ≠ b
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b
[PROOFSTEP]
lift e to G ≃ H using he
[GOAL]
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : β → α
hf : QuasiMeasurePreserving f
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => ↑e g • x) fun x => g • x
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b
[PROOFSTEP]
have : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹ := by simp [hab]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : β → α
hf : QuasiMeasurePreserving f
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => ↑e g • x) fun x => g • x
⊢ (↑e.symm a⁻¹)⁻¹ ≠ (↑e.symm b⁻¹)⁻¹
[PROOFSTEP]
simp [hab]
[GOAL]
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : β → α
hf : QuasiMeasurePreserving f
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => ↑e g • x) fun x => g • x
this : (↑e.symm a⁻¹)⁻¹ ≠ (↑e.symm b⁻¹)⁻¹
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b
[PROOFSTEP]
have := (h.aedisjoint this).preimage hf
[GOAL]
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : β → α
hf : QuasiMeasurePreserving f
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => ↑e g • x) fun x => g • x
this✝ : (↑e.symm a⁻¹)⁻¹ ≠ (↑e.symm b⁻¹)⁻¹
this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (↑e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (↑e.symm b⁻¹)⁻¹)
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b
[PROOFSTEP]
simp only [Semiconj] at hef 
[GOAL]
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : β → α
hf : QuasiMeasurePreserving f
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G) (x : β), f (↑e g • x) = g • f x
this✝ : (↑e.symm a⁻¹)⁻¹ ≠ (↑e.symm b⁻¹)⁻¹
this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (↑e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (↑e.symm b⁻¹)⁻¹)
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b
[PROOFSTEP]
simpa only [onFun, ← preimage_smul_inv, preimage_preimage, ← hef, e.apply_symm_apply, inv_inv] using this
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
⊢ IsFundamentalDomain H (↑f '' s)
[PROOFSTEP]
rw [f.image_eq_preimage]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
⊢ IsFundamentalDomain H (↑f.symm ⁻¹' s)
[PROOFSTEP]
refine' h.preimage_of_equiv hf e.symm.bijective fun g x => _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
g : G
x : β
⊢ ↑f.symm ((fun x => ↑e.symm g • x) x) = (fun x => g • x) (↑f.symm x)
[PROOFSTEP]
rcases f.surjective x with ⟨x, rfl⟩
[GOAL]
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
g : G
x : α
⊢ ↑f.symm ((fun x => ↑e.symm g • x) (↑f x)) = (fun x => g • x) (↑f.symm (↑f x))
[PROOFSTEP]
rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α μ
h : IsFundamentalDomain G s
g g' : G
⊢ (fun g' => g * g' * g⁻¹) ((fun g' => g⁻¹ * g' * g) g') = g'
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α μ
h : IsFundamentalDomain G s
g g' : G
⊢ (fun g' => g⁻¹ * g' * g) ((fun g' => g * g' * g⁻¹) g') = g'
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α μ
h : IsFundamentalDomain G s
g g' : G
x : α
⊢ ↑(MulAction.toPerm g)
      ((fun x =>
          ↑{ toFun := fun g' => g⁻¹ * g' * g, invFun := fun g' => g * g' * g⁻¹,
                  left_inv := (_ : ∀ (g' : G), g * (g⁻¹ * g' * g) * g⁻¹ = g'),
                  right_inv := (_ : ∀ (g' : G), g⁻¹ * (g * g' * g⁻¹) * g = g') }
              g' •
            x)
        x) =
    (fun x => g' • x) (↑(MulAction.toPerm g) x)
[PROOFSTEP]
simp [smul_smul, mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
hν : ν ≪ μ
⊢ (sum fun g => Measure.restrict ν (g • s)) = ν
[PROOFSTEP]
rw [← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g => (h.nullMeasurableSet_smul g).mono_ac hν,
  restrict_congr_set (hν h.iUnion_smul_ae_eq), restrict_univ]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
hν : ν ≪ μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν
[PROOFSTEP]
rw [← lintegral_sum_measure, h.sum_restrict_of_ac hν]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
f : α → ℝ≥0∞
t : Set α
⊢ ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂Measure.restrict μ t = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ
[PROOFSTEP]
simp only [h.restrict_restrict, inter_comm]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
f : α → ℝ≥0∞
t : Set α
⊢ ∑' (g : G), ∫⁻ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ
[PROOFSTEP]
simp only [smul_set_inter, inv_smul_smul]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
hν : ν ≪ μ
t : Set α
⊢ ↑↑ν t = ∑' (g : G), ↑↑ν (t ∩ g • s)
[PROOFSTEP]
have H : ν.restrict t ≪ μ := Measure.restrict_le_self.absolutelyContinuous.trans hν
[GOAL]
G : Type u_1
H✝ : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
hν : ν ≪ μ
t : Set α
H : Measure.restrict ν t ≪ μ
⊢ ↑↑ν t = ∑' (g : G), ↑↑ν (t ∩ g • s)
[PROOFSTEP]
simpa only [set_lintegral_one, Pi.one_def, Measure.restrict_apply₀ ((h.nullMeasurableSet_smul _).mono_ac H),
  inter_comm] using h.lintegral_eq_tsum_of_ac H 1
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
t : Set α
⊢ ↑↑μ t = ∑' (g : G), ↑↑μ (g • t ∩ s)
[PROOFSTEP]
simpa only [set_lintegral_one] using h.set_lintegral_eq_tsum' (fun _ => 1) t
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t = t
hts : ↑↑μ (t ∩ s) = 0
⊢ ↑↑μ t = 0
[PROOFSTEP]
rw [measure_eq_tsum h]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t = t
hts : ↑↑μ (t ∩ s) = 0
⊢ ∑' (g : G), ↑↑μ (g • t ∩ s) = 0
[PROOFSTEP]
simp [ht, hts]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
⊢ ↑↑μ t = Nat.card G • ↑↑μ (t ∩ s)
[PROOFSTEP]
haveI : Fintype G := Fintype.ofFinite G
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ ↑↑μ t = Nat.card G • ↑↑μ (t ∩ s)
[PROOFSTEP]
rw [h.measure_eq_tsum]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t =ᶠ[ae μ] t
this : Fintype G
⊢ ∑' (g : G), ↑↑μ (g • t ∩ s) = Nat.card G • ↑↑μ (t ∩ s)
[PROOFSTEP]
replace ht : ∀ g : G, (g • t ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := fun g => ae_eq_set_inter (ht g) (ae_eq_refl s)
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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✝ : Finite G
h : IsFundamentalDomain G s
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s
⊢ ∑' (g : G), ↑↑μ (g • t ∩ s) = Nat.card G • ↑↑μ (t ∩ s)
[PROOFSTEP]
simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card, Finset.card_univ]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → ℝ≥0∞
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∑' (g : G), ∫⁻ (x : α) in s ∩ g • t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ
[PROOFSTEP]
simp only [hf, inter_comm]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
⊢ ↑↑μ (A ∩ s) = ↑↑μ (A ∩ t)
[PROOFSTEP]
have : ∫⁻ x in s, A.indicator 1 x ∂μ = ∫⁻ x in t, A.indicator 1 x ∂μ :=
  by
  refine hs.set_lintegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_
  convert (Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).symm
  rw [hA g]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
⊢ ∫⁻ (x : α) in s, indicator A 1 x ∂μ = ∫⁻ (x : α) in t, indicator A 1 x ∂μ
[PROOFSTEP]
refine hs.set_lintegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
g : G
x : α
⊢ indicator A (fun x => 1) (g • x) = indicator A (fun x => 1) x
[PROOFSTEP]
convert (Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).symm
[GOAL]
case h.e'_3.h.e'_4
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
g : G
x : α
⊢ A = (fun x => g • x) ⁻¹' A
[PROOFSTEP]
rw [hA g]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
this : ∫⁻ (x : α) in s, indicator A 1 x ∂μ = ∫⁻ (x : α) in t, indicator A 1 x ∂μ
⊢ ↑↑μ (A ∩ s) = ↑↑μ (A ∩ t)
[PROOFSTEP]
simpa [Measure.restrict_apply hA₀, lintegral_indicator _ hA₀] using this
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
⊢ ↑↑μ s = ↑↑μ t
[PROOFSTEP]
simpa only [set_lintegral_one] using hs.set_lintegral_eq ht (fun _ => 1) fun _ _ => rfl
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ AEStronglyMeasurable f (Measure.restrict μ s) ↔ AEStronglyMeasurable f (sum fun g => Measure.restrict μ (g • t ∩ s))
[PROOFSTEP]
simp only [← ht.restrict_restrict, ht.sum_restrict_of_ac restrict_le_self.absolutelyContinuous]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ AEStronglyMeasurable f (sum fun g => Measure.restrict μ (g • t ∩ s)) ↔
    ∀ (g : G), AEStronglyMeasurable f (Measure.restrict μ (g • (g⁻¹ • s ∩ t)))
[PROOFSTEP]
simp only [smul_set_inter, inter_comm, smul_inv_smul, aestronglyMeasurable_sum_measure_iff]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (Measure.restrict μ (g⁻¹ • (g⁻¹⁻¹ • s ∩ t)))) ↔
    ∀ (g : G), AEStronglyMeasurable f (Measure.restrict μ (g⁻¹ • (g • s ∩ t)))
[PROOFSTEP]
simp only [inv_inv]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (Measure.restrict μ (g⁻¹ • (g • s ∩ t)))) ↔
    ∀ (g : G), AEStronglyMeasurable f (Measure.restrict μ (g • s ∩ t))
[PROOFSTEP]
refine' forall_congr' fun g => _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
⊢ AEStronglyMeasurable f (Measure.restrict μ (g⁻¹ • (g • s ∩ t))) ↔
    AEStronglyMeasurable f (Measure.restrict μ (g • s ∩ t))
[PROOFSTEP]
have he : MeasurableEmbedding ((· • ·) g⁻¹ : α → α) := measurableEmbedding_const_smul _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding ((fun x x_1 => x • x_1) g⁻¹)
⊢ AEStronglyMeasurable f (Measure.restrict μ (g⁻¹ • (g • s ∩ t))) ↔
    AEStronglyMeasurable f (Measure.restrict μ (g • s ∩ t))
[PROOFSTEP]
rw [← image_smul, ← ((measurePreserving_smul g⁻¹ μ).restrict_image_emb he _).aestronglyMeasurable_comp_iff he]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding ((fun x x_1 => x • x_1) g⁻¹)
⊢ AEStronglyMeasurable (f ∘ fun x => g⁻¹ • x) (Measure.restrict μ (g • s ∩ t)) ↔
    AEStronglyMeasurable f (Measure.restrict μ (g • s ∩ t))
[PROOFSTEP]
simp only [(· ∘ ·), hf]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β✝ : Type u_4
E : Type u_5
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 α
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (Measure.restrict μ (g • s ∩ t))) ↔ AEStronglyMeasurable f (Measure.restrict μ t)
[PROOFSTEP]
simp only [← aestronglyMeasurable_sum_measure_iff, ← hs.restrict_restrict,
  hs.sum_restrict_of_ac restrict_le_self.absolutelyContinuous]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ HasFiniteIntegral f ↔ HasFiniteIntegral f
[PROOFSTEP]
dsimp only [HasFiniteIntegral]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∫⁻ (a : α) in s, ↑‖f a‖₊ ∂μ < ⊤ ↔ ∫⁻ (a : α) in t, ↑‖f a‖₊ ∂μ < ⊤
[PROOFSTEP]
rw [hs.set_lintegral_eq ht]
[GOAL]
case hf
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∀ (g : G) (x : α), ↑‖f (g • x)‖₊ = ↑‖f x‖₊
[PROOFSTEP]
intro g x
[GOAL]
case hf
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 α
hs : IsFundamentalDomain G s
ht : IsFundamentalDomain G t
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
x : α
⊢ ↑‖f (g • x)‖₊ = ↑‖f x‖₊
[PROOFSTEP]
rw [hf]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 ∂ν
[PROOFSTEP]
rw [← MeasureTheory.integral_sum_measure, h.sum_restrict_of_ac hν]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
[PROOFSTEP]
rw [h.sum_restrict_of_ac hν]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact hf
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → E
hf : Integrable f
⊢ μ ≪ μ
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → E
t : Set α
hf : IntegrableOn f t
⊢ ∑' (g : G), ∫ (x : α) in g • s, f x ∂Measure.restrict μ t = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ
[PROOFSTEP]
simp only [h.restrict_restrict, measure_smul, inter_comm]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → E
t : Set α
hf : IntegrableOn f t
⊢ ∑' (g : G), ∫ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ
[PROOFSTEP]
simp only [smul_set_inter, inv_smul_smul]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 ∂μ
[PROOFSTEP]
by_cases hfs : IntegrableOn f s μ
[GOAL]
case pos
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 ∂μ
[PROOFSTEP]
have hft : IntegrableOn f t μ := by rwa [ht.integrableOn_iff hs hf]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
[PROOFSTEP]
rwa [ht.integrableOn_iff hs hf]
[GOAL]
case pos
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 ∂μ
[PROOFSTEP]
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
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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) ∂μ
[PROOFSTEP]
simp only [hf, inter_comm]
[GOAL]
case neg
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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 ∂μ
[PROOFSTEP]
rw [integral_undef hfs, integral_undef]
[GOAL]
case neg
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
[PROOFSTEP]
rwa [hs.integrableOn_iff ht hf] at hfs 
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ↑↑μ s < ↑↑μ t
⊢ ∃ x, x ∈ t ∧ ∃ y, y ∈ t ∧ ∃ g, g ≠ 1 ∧ g • x = y
[PROOFSTEP]
contrapose! ht
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
⊢ ↑↑μ t ≤ ↑↑μ s
[PROOFSTEP]
refine' hs.measure_le_of_pairwise_disjoint htm (Pairwise.aedisjoint fun g₁ g₂ hne => _)
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ (Disjoint on fun g => g • t ∩ s) g₁ g₂
[PROOFSTEP]
dsimp [Function.onFun]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t ∩ s) (g₂ • t ∩ s)
[PROOFSTEP]
refine' (Disjoint.inf_left _ _).inf_right _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t) (g₂ • t)
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ ∀ ⦃a : α⦄, a ∈ g₁ • t → ¬a ∈ g₂ • t
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy : g₂ • y = g₁ • x⟩
[GOAL]
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
⊢ False
[PROOFSTEP]
refine' ht x hx y hy (g₂⁻¹ * g₁) (mt inv_mul_eq_one.1 hne.symm) _
[GOAL]
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
⊢ (g₂⁻¹ * g₁) • x = y
[PROOFSTEP]
rw [mul_smul, ← hxy, inv_smul_smul]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ essSup f (Measure.restrict μ s) = essSup f μ
[PROOFSTEP]
refine' le_antisymm (essSup_mono_measure' Measure.restrict_le_self) _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ essSup f μ ≤ essSup f (Measure.restrict μ s)
[PROOFSTEP]
rw [essSup_eq_sInf (μ.restrict s) f, essSup_eq_sInf μ f]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ sInf {a | ↑↑μ {x | a < f x} = 0} ≤ sInf {a | ↑↑(Measure.restrict μ s) {x | a < f x} = 0}
[PROOFSTEP]
refine' sInf_le_sInf _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ {a | ↑↑(Measure.restrict μ s) {x | a < f x} = 0} ⊆ {a | ↑↑μ {x | a < f x} = 0}
[PROOFSTEP]
rintro a (ha : (μ.restrict s) {x : α | a < f x} = 0)
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : ↑↑(Measure.restrict μ s) {x | a < f x} = 0
⊢ a ∈ {a | ↑↑μ {x | a < f x} = 0}
[PROOFSTEP]
rw [Measure.restrict_apply₀' hs.nullMeasurableSet] at ha 
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : ↑↑μ ({x | a < f x} ∩ s) = 0
⊢ a ∈ {a | ↑↑μ {x | a < f x} = 0}
[PROOFSTEP]
refine' measure_zero_of_invariant hs _ _ ha
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : ↑↑μ ({x | a < f x} ∩ s) = 0
⊢ ∀ (g : G), g • {x | a < f x} = {x | a < f x}
[PROOFSTEP]
intro γ
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : ↑↑μ ({x | a < f x} ∩ s) = 0
γ : G
⊢ γ • {x | a < f x} = {x | a < f x}
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : ↑↑μ ({x | a < f x} ∩ s) = 0
γ : G
x : α
⊢ x ∈ γ • {x | a < f x} ↔ x ∈ {x | a < f x}
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem]
[GOAL]
case h
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
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
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : ↑↑μ ({x | a < f x} ∩ s) = 0
γ : G
x : α
⊢ γ⁻¹ • x ∈ {x | a < f x} ↔ x ∈ {x | a < f x}
[PROOFSTEP]
simp only [mem_setOf_eq, hf γ⁻¹ x]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 1 ∧ x ∈ g • s
[PROOFSTEP]
simp [fundamentalFrontier]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬x ∈ g • s
[PROOFSTEP]
simp [fundamentalInterior]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
x : α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s
[PROOFSTEP]
simp_rw [fundamentalFrontier, smul_set_inter, smul_set_Union, smul_comm g (_ : G) (_ : Set α)]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁴ : Group G
inst✝³ : MulAction G α
s : Set α
x : α
inst✝² : Group H
inst✝¹ : MulAction H α
inst✝ : SMulCommClass H G α
g : H
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s
[PROOFSTEP]
simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_Union, smul_comm g (_ : G) (_ : Set α)]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ Pairwise (Disjoint on fun g => g • fundamentalInterior G s)
[PROOFSTEP]
refine' fun a b hab => disjoint_left.2 _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
a b : G
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (fun g => g • fundamentalInterior G s) a → ¬a_1 ∈ (fun g => g • fundamentalInterior G s) b
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩
[GOAL]
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
a b : G
hab : a ≠ b
x : α
hx : x ∈ fundamentalInterior G s
y : α
hy : y ∈ fundamentalInterior G s
hxy : (fun x => b • x) y = (fun x => a • x) x
⊢ False
[PROOFSTEP]
rw [mem_fundamentalInterior] at hx hy 
[GOAL]
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬x ∈ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬y ∈ g • s
hxy : (fun x => b • x) y = (fun x => a • x) x
⊢ False
[PROOFSTEP]
refine' hx.2 (a⁻¹ * b) _ _
[GOAL]
case intro.intro.intro.intro.refine'_1
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬x ∈ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬y ∈ g • s
hxy : (fun x => b • x) y = (fun x => a • x) x
⊢ a⁻¹ * b ≠ 1
case intro.intro.intro.intro.refine'_2
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬x ∈ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬y ∈ g • s
hxy : (fun x => b • x) y = (fun x => a • x) x
⊢ x ∈ (a⁻¹ * b) • s
[PROOFSTEP]
rwa [Ne.def, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
[GOAL]
case intro.intro.intro.intro.refine'_2
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬x ∈ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → ¬y ∈ g • s
hxy : (fun x => b • x) y = (fun x => a • x) x
⊢ x ∈ (a⁻¹ * b) • s
[PROOFSTEP]
simpa [mul_smul, ← hxy, mem_inv_smul_set_iff] using hy.1
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝³ : Countable G
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
⊢ ↑↑μ (fundamentalFrontier G s) = 0
[PROOFSTEP]
simpa only [fundamentalFrontier, iUnion₂_inter, measure_iUnion_null_iff', one_smul, measure_iUnion_null_iff,
  inter_comm s, Function.onFun] using fun g (hg : g ≠ 1) => hs.aedisjoint hg
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ fundamentalInterior G s
[PROOFSTEP]
simp_rw [ae_iff, not_exists, ← mem_inv_smul_set_iff, setOf_forall, ← compl_setOf, setOf_mem_eq, ← compl_iUnion]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ↑↑μ (⋃ (i : G), i⁻¹ • fundamentalInterior G s)ᶜ = 0
[PROOFSTEP]
have : ((⋃ g : G, g⁻¹ • s) \ ⋃ g : G, g⁻¹ • fundamentalFrontier G s) ⊆ ⋃ g : G, g⁻¹ • fundamentalInterior G s := by
  simp_rw [diff_subset_iff, ← iUnion_union_distrib, ← smul_set_union (α := G) (β := α),
    fundamentalFrontier_union_fundamentalInterior];
  rfl
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ (⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s ⊆ ⋃ (g : G), g⁻¹ • fundamentalInterior G s
[PROOFSTEP]
simp_rw [diff_subset_iff, ← iUnion_union_distrib, ← smul_set_union (α := G) (β := α),
  fundamentalFrontier_union_fundamentalInterior]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ ⋃ (g : G), g⁻¹ • s ⊆ ⋃ (g : G), g⁻¹ • s
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s ⊆ ⋃ (g : G), g⁻¹ • fundamentalInterior G s
⊢ ↑↑μ (⋃ (i : G), i⁻¹ • fundamentalInterior G s)ᶜ = 0
[PROOFSTEP]
refine' eq_bot_mono (μ.mono <| compl_subset_compl.2 this) _
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s ⊆ ⋃ (g : G), g⁻¹ • fundamentalInterior G s
⊢ ↑↑μ ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)ᶜ = ⊥
[PROOFSTEP]
simp only [iUnion_inv_smul, compl_sdiff, ENNReal.bot_eq_zero, himp_eq, sup_eq_union,
  @iUnion_smul_eq_setOf_exists _ _ _ _ s]
[GOAL]
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst✝⁶ : Countable G
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
this : (⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s ⊆ ⋃ (g : G), g⁻¹ • fundamentalInterior G s
⊢ ↑↑μ ((⋃ (g : G), g • fundamentalFrontier G s) ∪ {a | ∃ g, g • a ∈ s}ᶜ) = 0
[PROOFSTEP]
exact measure_union_null (measure_iUnion_null fun _ => measure_smul_null hs.measure_fundamentalFrontier _) hs.ae_covers
