Jcost_surjective_on_nonneg

proof body

Tactic-mode proof.

 259  intro y hy
 260  -- J(x) = (x + 1/x)/2 - 1
 261  -- Solve (x + 1/x)/2 - 1 = y => x + 1/x = 2(y+1)
 262  -- x^2 - 2(y+1)x + 1 = 0
 263  -- x = [(2(y+1)) + sqrt(4(y+1)^2 - 4)] / 2 = (y+1) + sqrt((y+1)^2 - 1)
 264  let x := (y + 1) + Real.sqrt ((y + 1) ^ 2 - 1)
 265  use x
 266  have h_y1_ge_1 : 1 ≤ y + 1 := by linarith
 267  have h_sq_ge_0 : 0 ≤ (y + 1) ^ 2 - 1 := by nlinarith
 268  constructor
 269  · have : 0 ≤ Real.sqrt ((y + 1) ^ 2 - 1) := Real.sqrt_nonneg _
 270    linarith
 271  · unfold Jcost
 272    have hx_pos : 0 < x := by
 273      have : 0 ≤ Real.sqrt ((y + 1) ^ 2 - 1) := Real.sqrt_nonneg _
 274      linarith
 275    field_simp [hx_pos.ne']
 276    -- Goal after field_simp: x^2 + 1 - x*2 = x*2*y
 277    -- Since x = y+1 + sqrt((y+1)^2 - 1), we have x^2 - 2(y+1)x + 1 = 0
 278    -- Thus x^2 + 1 = 2(y+1)x = 2x + 2xy, so x^2 + 1 - 2x = 2xy
 279    let s := Real.sqrt ((y + 1) ^ 2 - 1)
 280    have hs_sq : s ^ 2 = (y + 1) ^ 2 - 1 := Real.sq_sqrt h_sq_ge_0
 281    have hx_eq : x = y + 1 + s := rfl
 282    -- Key equation: x^2 - 2(y+1)x + 1 = 0
 283    have h_quad : x ^ 2 - 2 * (y + 1) * x + 1 = 0 := by
 284      have h1 : x ^ 2 = (y + 1 + s) ^ 2 := by rw [hx_eq]
 285      have h2 : (y + 1 + s) ^ 2 = (y + 1) ^ 2 + 2 * (y + 1) * s + s ^ 2 := by ring
 286      have h3 : s ^ 2 = (y + 1) ^ 2 - 1 := hs_sq
 287      calc x ^ 2 - 2 * (y + 1) * x + 1
 288          = (y + 1 + s) ^ 2 - 2 * (y + 1) * (y + 1 + s) + 1 := by simp only [hx_eq]
 289        _ = ((y + 1) ^ 2 + 2 * (y + 1) * s + s ^ 2) - 2 * (y + 1) * (y + 1 + s) + 1 := by rw [h2]
 290        _ = ((y + 1) ^ 2 + 2 * (y + 1) * s + ((y + 1) ^ 2 - 1)) - 2 * (y + 1) * (y + 1 + s) + 1 := by rw [h3]
 291        _ = 0 := by ring
 292    -- From h_quad: x^2 + 1 = 2(y+1)x = 2x(y+1) = 2x + 2xy
 293    -- So: x^2 + 1 - 2x = 2xy
 294    linarith [h_quad]
 295