Jlog_nonneg

formal source

 231@[simp] lemma Jlog_zero : Jlog 0 = 0 := by
 232  simp [Jlog, Jcost]
 233
 234lemma Jlog_nonneg (t : ℝ) : 0 ≤ Jlog t :=
 235  Jcost_nonneg (Real.exp_pos t)
 236
 237/-- J(x) > 0 for x ≠ 1 and x > 0. -/
 238lemma Jcost_pos_of_ne_one (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) : 0 < Jcost x := by
 239  have hx0 : x ≠ 0 := ne_of_gt hx
 240  rw [Jcost_eq_sq hx0]
 241  apply div_pos
 242  · have hne : (x - 1) ≠ 0 := sub_ne_zero.mpr hx1
 243    exact sq_pos_of_ne_zero hne
 244  · have h2 : (0 : ℝ) < 2 := by norm_num
 245    exact mul_pos h2 hx
 246
 247/-- J(x) = 0 iff x = 1, for positive x. -/
 248lemma Jcost_eq_zero_iff (x : ℝ) (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
 249  constructor
 250  · intro h
 251    by_contra h1
 252    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx h1))
 253  · intro h
 254    rw [h]
 255    exact Jcost_unit0
 256
 257/-- **THEOREM**: Jcost is surjective onto [0, ∞). -/
 258theorem Jcost_surjective_on_nonneg : ∀ y : ℝ, 0 ≤ y → ∃ x : ℝ, 1 ≤ x ∧ Jcost x = y := by
 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)