distZ

formal source

  34
  35/-- Distance to the nearest integer: d_ℤ(δ) = min(fract(δ), 1 − fract(δ)).
  36    This is in [0, 1/2] and vanishes exactly when δ is an integer. -/
  37noncomputable def distZ (δ : ℝ) : ℝ :=
  38  min (Int.fract δ) (1 - Int.fract δ)
  39
  40theorem distZ_nonneg (δ : ℝ) : 0 ≤ distZ δ := by
  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 δ