[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
cases' le_or_lt ε 0 with hε hε
[GOAL]
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall, min_eq_right (by linarith [hT.out] : 2 * ε ≤ T),
  ENNReal.ofReal_eq_zero]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ T
[PROOFSTEP]
linarith [hT.out]
[GOAL]
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0
[PROOFSTEP]
exact mul_nonpos_of_nonneg_of_nonpos zero_le_two hε
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
suffices volume (closedBall x ε) ≤ volume (ball x ε) by
  exact (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this measurableSet_ball (measure_ne_top _ _)).symm
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : ↑↑volume (closedBall x ε) ≤ ↑↑volume (ball x ε)
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
exact (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this measurableSet_ball (measure_ne_top _ _)).symm
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ ↑↑volume (closedBall x ε) ≤ ↑↑volume (ball x ε)
[PROOFSTEP]
have : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 <| volume (closedBall x ε)) :=
  by
  simp_rw [volume_closedBall]
  refine' ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ _)
  convert (@monotone_id ℝ _).tendsto_nhdsWithin_Iio ε
  simp
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ => ↑↑volume (closedBall x δ)) (𝓝[Iio ε] ε) (𝓝 (↑↑volume (closedBall x ε)))
[PROOFSTEP]
simp_rw [volume_closedBall]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ => ENNReal.ofReal (min T (2 * δ))) (𝓝[Iio ε] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))
[PROOFSTEP]
refine' ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ _)
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun k => k) (𝓝[Iio ε] ε) (𝓝 ε)
[PROOFSTEP]
convert (@monotone_id ℝ _).tendsto_nhdsWithin_Iio ε
[GOAL]
case h.e'_5.h.e'_3
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ ε = sSup (id '' Iio ε)
[PROOFSTEP]
simp
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => ↑↑volume (closedBall x δ)) (𝓝[Iio ε] ε) (𝓝 (↑↑volume (closedBall x ε)))
⊢ ↑↑volume (closedBall x ε) ≤ ↑↑volume (ball x ε)
[PROOFSTEP]
refine' le_of_tendsto this (mem_nhdsWithin_Iio_iff_exists_Ioo_subset.mpr ⟨0, hε, fun r hr => _⟩)
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => ↑↑volume (closedBall x δ)) (𝓝[Iio ε] ε) (𝓝 (↑↑volume (closedBall x ε)))
r : ℝ
hr : r ∈ Ioo 0 ε
⊢ r ∈ {x_1 | (fun c => ↑↑volume (closedBall x c) ≤ ↑↑volume (ball x ε)) x_1}
[PROOFSTEP]
exact measure_mono (closedBall_subset_ball hr.2)
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
⊢ IsAddFundamentalDomain { x // x ∈ AddSubgroup.zmultiples u } I
[PROOFSTEP]
set G := AddSubgroup.zmultiples u
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
set n := addOrderOf u
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑n))
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
set B := ball x (T / (2 * n))
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
have hn : 1 ≤ (n : ℝ) := by norm_cast; linarith [addOrderOf_pos' hu]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ 1 ≤ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ 1 ≤ n
[PROOFSTEP]
linarith [addOrderOf_pos' hu]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
refine' IsAddFundamentalDomain.mk_of_measure_univ_le _ _ _ _
[GOAL]
case refine'_1
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ NullMeasurableSet I
[PROOFSTEP]
exact measurableSet_ball.nullMeasurableSet.congr hI.symm
[GOAL]
case refine'_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : { x // x ∈ G }), g ≠ 0 → AEDisjoint volume (g +ᵥ I) I
[PROOFSTEP]
rintro ⟨g, hg⟩ hg'
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : { val := g, property := hg } ≠ 0
⊢ AEDisjoint volume ({ val := g, property := hg } +ᵥ I) I
[PROOFSTEP]
replace hg' : g ≠ 0
[GOAL]
case hg'
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : { val := g, property := hg } ≠ 0
⊢ g ≠ 0
[PROOFSTEP]
simpa only [Ne.def, AddSubgroup.mk_eq_zero_iff] using hg'
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint volume ({ val := g, property := hg } +ᵥ I) I
[PROOFSTEP]
change AEDisjoint volume (g +ᵥ I) I
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint volume (g +ᵥ I) I
[PROOFSTEP]
refine'
  AEDisjoint.congr (Disjoint.aedisjoint _) ((quasiMeasurePreserving_add_left volume (-g)).vadd_ae_eq_of_ae_eq g hI) hI
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ Disjoint (g +ᵥ B) B
[PROOFSTEP]
have hBg : g +ᵥ B = ball (g + x) (T / (2 * n)) := by
  rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ g +ᵥ B = ball (g + x) (T / (2 * ↑n))
[PROOFSTEP]
rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ Disjoint (g +ᵥ B) B
[PROOFSTEP]
rw [hBg]
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ Disjoint (ball (g + x) (T / (2 * ↑n))) B
[PROOFSTEP]
apply ball_disjoint_ball
[GOAL]
case refine'_2.mk.h
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / (2 * ↑n) + T / (2 * ↑n) ≤ dist (g + x) x
[PROOFSTEP]
rw [dist_eq_norm, add_sub_cancel, div_mul_eq_div_div, ← add_div, ← add_div, add_self_div_two,
  div_le_iff' (by positivity : 0 < (n : ℝ)), ← nsmul_eq_mul]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ 0 < ↑n
[PROOFSTEP]
positivity
[GOAL]
case refine'_2.mk.h
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T ≤ n • ‖g‖
[PROOFSTEP]
refine'
  (le_add_order_smul_norm_of_isOfFinAddOrder (hu.of_mem_zmultiples hg) hg').trans (nsmul_le_nsmul (norm_nonneg g) _)
[GOAL]
case refine'_2.mk.h
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ addOrderOf g ≤ n
[PROOFSTEP]
exact Nat.le_of_dvd (addOrderOf_pos_iff.mpr hu) (addOrderOf_dvd_of_mem_zmultiples hg)
[GOAL]
case refine'_3
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : { x // x ∈ G }), QuasiMeasurePreserving ((fun x x_1 => x +ᵥ x_1) g)
[PROOFSTEP]
exact fun g => quasiMeasurePreserving_add_left (G := AddCircle T) volume g
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
replace hI := hI.trans closedBall_ae_eq_ball.symm
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
have hG_card : (Finset.univ : Finset G).card = n :=
  by
  show _ = addOrderOf u
  rw [add_order_eq_card_zmultiples', Nat.card_eq_fintype_card]; rfl
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ Finset.card Finset.univ = n
[PROOFSTEP]
show _ = addOrderOf u
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ Finset.card Finset.univ = addOrderOf u
[PROOFSTEP]
rw [add_order_eq_card_zmultiples', Nat.card_eq_fintype_card]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ Finset.card Finset.univ = Fintype.card { x // x ∈ AddSubgroup.zmultiples u }
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
hG_card : Finset.card Finset.univ = n
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
simp_rw [measure_vadd]
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
hG_card : Finset.card Finset.univ = n
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ AddSubgroup.zmultiples u }), ↑↑volume I
[PROOFSTEP]
rw [AddCircle.measure_univ, tsum_fintype, Finset.sum_const, measure_congr hI, volume_closedBall, ← ENNReal.ofReal_nsmul,
  mul_div, mul_div_mul_comm, div_self, one_mul, min_eq_right (div_le_self hT.out.le hn), hG_card, nsmul_eq_mul,
  mul_div_cancel' T (lt_of_lt_of_le zero_lt_one hn).ne.symm]
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
hG_card : Finset.card Finset.univ = n
⊢ 2 ≠ 0
[PROOFSTEP]
exact two_ne_zero
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
let G := AddSubgroup.zmultiples u
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
have hsG : ∀ g : G, (g +ᵥ s : Set <| AddCircle T) =ᵐ[volume] s := by rintro ⟨y, hy⟩;
  exact (vadd_ae_eq_self_of_mem_zmultiples hs hy : _)
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
⊢ ∀ (g : { x // x ∈ G }), g +ᵥ s =ᶠ[ae volume] s
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
y : AddCircle T
hy : y ∈ G
⊢ { val := y, property := hy } +ᵥ s =ᶠ[ae volume] s
[PROOFSTEP]
exact (vadd_ae_eq_self_of_mem_zmultiples hs hy : _)
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
hsG : ∀ (g : { x // x ∈ G }), g +ᵥ s =ᶠ[ae volume] s
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
rw [(isAddFundamentalDomain_of_ae_ball I u x hu hI).measure_eq_card_smul_of_vadd_ae_eq_self s hsG,
  add_order_eq_card_zmultiples' u, Nat.card_eq_fintype_card]
