Jlog_eq_zero_iff

formal source

   7/-- Log-domain cost: Jcost composed with exp -/
   8noncomputable def Jlog (t : ℝ) : ℝ := Jcost (Real.exp t)
   9
  10lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by
  11  simp [Jlog, Jcost_unit0]
  12  have h : Real.exp t = 1 ↔ t = 0 := Real.exp_eq_one_iff
  13  exact h
  14
  15lemma Jlog_nonneg (t : ℝ) : 0 ≤ Jlog t := by
  16  simp [Jlog]
  17  -- Jcost is nonnegative: for x > 0, by AM-GM: x + 1/x ≥ 2, so 1/2(x + 1/x) - 1 ≥ 0
  18  have hx : 0 < Real.exp t := Real.exp_pos t
  19  have hamgm : Real.exp t + (Real.exp t)⁻¹ ≥ 2 := by
  20    have := Real.add_ge_two_mul_sqrt (Real.exp t) (Real.exp t)⁻¹
  21    · simp at this; exact this
  22    · exact hx
  23    · have : 0 < (Real.exp t)⁻¹ := inv_pos.mpr hx
  24      exact this
  25  calc
  26    Jcost (Real.exp t) = (1/2) * (Real.exp t + (Real.exp t)⁻¹) - 1 := rfl
  27    _ ≥ (1/2) * 2 - 1 := mul_le_mul_of_nonneg_left hamgm (by norm_num)
  28    _ = 0 := by norm_num
  29
  30lemma hasDerivAt_Jlog (t : ℝ) : HasDerivAt Jlog (Real.sinh t) t := by
  31  -- Jlog(t) = Jcost (exp t) = (exp t + exp (-t))/2 - 1 = cosh t - 1
  32  have hcosh : HasDerivAt Real.cosh (Real.sinh t) t := Real.hasDerivAt_cosh t
  33  have h : HasDerivAt (fun s => Real.cosh s - 1) (Real.sinh t) t := hcosh.sub_const 1
  34  -- Identify Jlog with cosh − 1 pointwise
  35  have heq : (fun s => Jlog s) = (fun s => Real.cosh s - 1) := by
  36    funext s
  37    unfold Jlog
  38    -- Jcost (exp s) = ((exp s) + (exp s)⁻¹)/2 - 1 and (exp s)⁻¹ = exp (−s)
  39    simp [Jcost, Real.cosh, Real.exp_neg]
  40  simpa [heq]