Documentation

Lean 4 Proof

theorem coordinationGap_pos {J_high J_low ρ : ℝ}
    (hJl : 1 < J_low) (hJh : J_low < J_high) (hρ : ρ < 1) :
    0 < coordinationGap J_high J_low ρ := by
  simp only [coordinationGap, curvatureKReal]
  have h1ρ : 0 < 1 - ρ := by linarith
  have hJl_pos : 0 < J_low := by linarith
  have hJh_pos : 0 < J_high := by linarith
  rw [show (1 - ρ) * (J_high - 1) / J_high - (1 - ρ) * (J_low - 1) / J_low =
    (1 - ρ) * ((J_high - 1) / J_high - (J_low - 1) / J_low) from by ring]
  apply mul_pos h1ρ
  rw [div_sub_div _ _ (ne_of_gt hJh_pos) (ne_of_gt hJl_pos)]
  apply div_pos
  · nlinarith
  · exact mul_pos hJh_pos hJl_pos

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Defs.lean:127

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file