isAddFundamentalDomain_of_ae_ball

English

If u has finite additive order n and I is almost equal to a ball of radius T/(2n), then I is a fundamental domain for the subgroup generated by u.

Русский

Если u имеет конечный порядок n по сложению и I почти равно шару радиуса T/(2n), то I является фундаментальной областью для подгруппы, порожденной u.

LaTeX

$$$\\text{IsAddFundamentalDomain} (\\text{AddSubgroup.zmultiples }u)\\ I$ under the given assumptions$$

Lean4

/-- Let `G` be the subgroup of `AddCircle T` generated by a point `u` of finite order `n : ℕ`. Then
any set `I` that is almost equal to a ball of radius `T / 2n` is a fundamental domain for the action
of `G` on `AddCircle T` by left addition. -/
theorem isAddFundamentalDomain_of_ae_ball (I : Set <| AddCircle T) (u x : AddCircle T) (hu : IsOfFinAddOrder u)
    (hI : I =ᵐ[volume] ball x (T / (2 * addOrderOf u))) : IsAddFundamentalDomain (AddSubgroup.zmultiples u) I :=
  by
  set G := AddSubgroup.zmultiples u
  set n := addOrderOf u
  set B := ball x (T / (2 * n))
  have hn : 1 ≤ (n : ℝ) := by norm_cast; linarith [hu.addOrderOf_pos]
  refine IsAddFundamentalDomain.mk_of_measure_univ_le ?_ ?_ ?_ ?_
  · -- `NullMeasurableSet I volume`
    exact measurableSet_ball.nullMeasurableSet.congr hI.symm
  · -- `∀ (g : G), g ≠ 0 → AEDisjoint volume (g +ᵥ I) I`

    rintro ⟨g, hg⟩ hg'
    replace hg' : g ≠ 0 := by simpa only [Ne, AddSubgroup.mk_eq_zero] using hg'
    change AEDisjoint volume (g +ᵥ I) I
    refine
      AEDisjoint.congr (Disjoint.aedisjoint ?_) ((quasiMeasurePreserving_add_left volume (-g)).vadd_ae_eq_of_ae_eq g hI)
        hI
    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]
    rw [hBg]
    apply ball_disjoint_ball
    rw [dist_eq_norm, add_sub_cancel_right, div_mul_eq_div_div, ← add_div, ← add_div, add_self_div_two,
      div_le_iff₀' (by positivity : 0 < (n : ℝ)), ← nsmul_eq_mul]
    refine
      (le_add_order_smul_norm_of_isOfFinAddOrder (hu.of_mem_zmultiples hg) hg').trans
        (nsmul_le_nsmul_left (norm_nonneg g) ?_)
    exact Nat.le_of_dvd (addOrderOf_pos_iff.mpr hu) (addOrderOf_dvd_of_mem_zmultiples hg)
  · -- `∀ (g : G), QuasiMeasurePreserving (VAdd.vadd g) volume volume`
    exact fun g => quasiMeasurePreserving_add_left (G := AddCircle T) volume g
  · -- `volume univ ≤ ∑' (g : G), volume (g +ᵥ I)`

    replace hI := hI.trans closedBall_ae_eq_ball.symm
    haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples.to_subtype
    have hG_card : #(Finset.univ : Finset G) = n :=
      by
      change _ = addOrderOf u
      rw [← Nat.card_zmultiples, Nat.card_eq_fintype_card]; rfl
    simp_rw [measure_vadd]
    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]
    exact two_ne_zero

Похожие утверждения