distZ_eq_zero_iff

formal source

  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⟩
  75    rw [hn, Int.fract_intCast]
  76    simp
  77
  78/-! ### The reduced phase potential -/
  79
  80/-- The reduced phase potential: J̃(lam, δ) = cosh(lam · d_ℤ(δ)) − 1.
  81    Here lam = ln b for the base b of the discrete quotient. -/
  82noncomputable def Jtilde (lam : ℝ) (δ : ℝ) : ℝ :=
  83  cosh (lam * distZ δ) - 1
  84
  85/-- J̃ ≥ 0. -/
  86theorem Jtilde_nonneg (lam : ℝ) (δ : ℝ) : 0 ≤ Jtilde lam δ := by
  87  unfold Jtilde
  88  linarith [one_le_cosh (lam * distZ δ)]
  89
  90/-- J̃ is 1-periodic in δ. -/
  91theorem Jtilde_periodic (lam : ℝ) (δ : ℝ) : Jtilde lam (δ + 1) = Jtilde lam δ := by
  92  unfold Jtilde
  93  rw [distZ_periodic]