Jtilde

formal source

  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]
  94
  95/-- J̃ is 1-periodic for general integer shifts. -/
  96theorem Jtilde_add_int (lam : ℝ) (δ : ℝ) (n : ℤ) :
  97    Jtilde lam (δ + ↑n) = Jtilde lam δ := by
  98  unfold Jtilde
  99  rw [distZ_add_int]
 100
 101/-- cosh(t) = 1 iff t = 0. -/
 102private lemma cosh_eq_one_iff (t : ℝ) : cosh t = 1 ↔ t = 0 := by
 103  constructor
 104  · intro h
 105    by_contra hne
 106    exact absurd h (ne_of_gt ((one_lt_cosh).mpr hne))
 107  · intro h; rw [h, cosh_zero]
 108
 109/-- J̃(lam, δ) = 0 iff δ is an integer, for lam ≠ 0. -/
 110theorem Jtilde_zero_iff {lam : ℝ} (hlam : lam ≠ 0) (δ : ℝ) :
 111    Jtilde lam δ = 0 ↔ ∃ n : ℤ, δ = ↑n := by
 112  unfold Jtilde