J

formal source

  78/-- The fundamental cost J(x) = ½(x + 1/x) - 1.
  79
  80    This is the unique cost satisfying d'Alembert + normalization + calibration (T5). -/
  81noncomputable def J (x : ℝ) : ℝ := (1/2) * (x + x⁻¹) - 1
  82
  83/-- J is non-negative for positive arguments. -/
  84lemma J_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J x := by
  85  unfold J
  86  have hx_ne : x ≠ 0 := hx.ne'
  87  have h_rewrite : (1:ℝ)/2 * (x + x⁻¹) - 1 = (x - 1)^2 / (2 * x) := by field_simp; ring
  88  rw [h_rewrite]
  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)