J_at_one

formal source

  89  apply div_nonneg (sq_nonneg _) (by linarith : 0 ≤ 2 * x)
  90
  91/-- J(1) = 0 (the identity has zero cost). -/
  92lemma J_at_one : J 1 = 0 := by unfold J; norm_num
  93
  94/-- J(x) = 0 iff x = 1 (for positive x). -/
  95lemma J_zero_iff_one {x : ℝ} (hx : 0 < x) : J x = 0 ↔ x = 1 := by
  96  constructor
  97  · intro h
  98    unfold J at h
  99    have hx_ne : x ≠ 0 := hx.ne'
 100    have h1 : x + x⁻¹ = 2 := by linarith
 101    have h2 : x * (x + x⁻¹) = x * 2 := by rw [h1]
 102    have h3 : x^2 + 1 = 2 * x := by field_simp at h2; linarith
 103    nlinarith [sq_nonneg (x - 1)]
 104  · intro h; rw [h]; exact J_at_one
 105
 106/-- J is positive for x ≠ 1. -/
 107lemma J_pos_of_ne_one {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) : 0 < J x := by
 108  have h := J_nonneg hx
 109  cases' h.lt_or_eq with hlt heq
 110  · exact hlt
 111  · exfalso; exact hne ((J_zero_iff_one hx).mp heq.symm)
 112
 113/-! ## Transition Cost -/
 114
 115/-- The cost of transitioning from configuration x to configuration y.
 116
 117    This is the "action" for a direct transition, defined as the average
 118    cost along the transition weighted by the magnitude of change.
 119
 120    J_transition(x,y) = |ln(y/x)| · (J(x) + J(y)) / 2
 121
 122    Key properties: