distZ_le_half

formal source

  41  unfold distZ
  42  exact le_min (Int.fract_nonneg δ) (by linarith [Int.fract_lt_one δ])
  43
  44theorem distZ_le_half (δ : ℝ) : distZ δ ≤ 1 / 2 := by
  45  unfold distZ
  46  rcases le_or_gt (Int.fract δ) (1 / 2) with h | h
  47  · exact min_le_left _ _ |>.trans h
  48  · have : 1 - Int.fract δ ≤ 1 / 2 := by linarith
  49    exact min_le_right _ _ |>.trans this
  50
  51/-- d_ℤ is 1-periodic: d_ℤ(δ + n) = d_ℤ(δ) for integer n. -/
  52theorem distZ_add_int (δ : ℝ) (n : ℤ) : distZ (δ + ↑n) = distZ δ := by
  53  unfold distZ
  54  rw [Int.fract_add_intCast]
  55
  56/-- d_ℤ is 1-periodic (special case n = 1). -/
  57theorem distZ_periodic (δ : ℝ) : distZ (δ + 1) = distZ δ := by
  58  have h : δ + 1 = δ + ↑(1 : ℤ) := by push_cast; ring
  59  rw [h]
  60  exact distZ_add_int δ 1
  61
  62/-- d_ℤ(δ) = 0 iff δ is an integer. -/
  63theorem distZ_eq_zero_iff (δ : ℝ) : distZ δ = 0 ↔ ∃ n : ℤ, δ = ↑n := by
  64  unfold distZ
  65  constructor
  66  · intro h
  67    have hfrac_nonneg := Int.fract_nonneg δ
  68    have h1sub_pos : 0 < 1 - Int.fract δ := by linarith [Int.fract_lt_one δ]
  69    have hfrac_zero : Int.fract δ = 0 := by
  70      rcases le_or_gt (Int.fract δ) (1 - Int.fract δ) with h_le | h_lt
  71      · rwa [min_eq_left h_le] at h
  72      · rw [min_eq_right (le_of_lt h_lt)] at h; linarith
  73    exact ⟨⌊δ⌋, by linarith [Int.fract_add_floor δ]⟩
  74  · intro ⟨n, hn⟩