pith. machine review for the scientific record. sign in
theorem proved tactic proof

distZ_eq_zero_iff

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  63theorem distZ_eq_zero_iff (δ : ℝ) : distZ δ = 0 ↔ ∃ n : ℤ, δ = ↑n := by

proof body

Tactic-mode proof.

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.