Jlog_eq_zero_iff

formal source

 293    -- So: x^2 + 1 - 2x = 2xy
 294    linarith [h_quad]
 295
 296lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by
 297  constructor
 298  · intro h
 299    have hxpos : 0 < Real.exp t := Real.exp_pos t
 300    have hxne : Real.exp t ≠ 0 := ne_of_gt hxpos
 301    have hrepr := Jcost_eq_sq hxne
 302    rw [Jlog, hrepr] at h
 303    have hden_pos : 0 < 2 * Real.exp t := by
 304      apply mul_pos
 305      · norm_num
 306      · exact hxpos
 307    have hden_ne : 2 * Real.exp t ≠ 0 := ne_of_gt hden_pos
 308    rw [div_eq_zero_iff] at h
 309    cases h with
 310    | inl h_num =>
 311      have hexp1 : Real.exp t - 1 = 0 := by nlinarith [sq_nonneg (Real.exp t - 1)]
 312      have hexp_eq : Real.exp t = 1 := by linarith
 313      rw [Real.exp_eq_one_iff] at hexp_eq
 314      exact hexp_eq
 315    | inr h_den =>
 316      exact absurd h_den hden_ne
 317  · intro h
 318    rw [h]
 319    exact Jlog_zero
 320
 321
 322theorem EL_stationary_at_zero : deriv Jlog 0 = 0 := by
 323  simp
 324
 325theorem EL_global_min (t : ℝ) : Jlog 0 ≤ Jlog t := by
 326  simpa [Jlog_zero] using Jlog_nonneg t