  56  linarith [Real.one_le_cosh (Real.log phi * u)]
  57
  58/-- The stiffness constant κ = (log φ)². -/
  59noncomputable def kappa : ℝ := (Real.log phi) ^ 2
  60
  61theorem kappa_pos : 0 < kappa := by
  62  unfold kappa
  63  have hlog_pos : 0 < Real.log phi := Real.log_pos one_lt_phi
  64  nlinarith
  65
  66/-- Quadratic lower bound: f(u) ≥ κ·u²/2.
  67    Follows from cosh(t) ≥ 1 + t²/2. -/
  68theorem phiCost_quadratic_lb (u : ℝ) :
  69    kappa * u ^ 2 / 2 ≤ phiCost u := by
  70  unfold kappa phiCost
  71  let t : ℝ := Real.log phi * u
  72  have ht : Real.log phi * u = t := rfl
  73  have hmain_nonneg : 0 ≤ t ^ 2 / 2 := by positivity
  74  by_cases htnonneg : 0 ≤ t
  75  · have hs : t / 2 ≤ Real.sinh (t / 2) :=
  76      (Real.self_le_sinh_iff).2 (by linarith)
  77    have hs_sq : (t / 2) ^ 2 ≤ Real.sinh (t / 2) ^ 2 := by
  78      nlinarith [hs, sq_nonneg (Real.sinh (t / 2))]
  79    have hformula : Real.cosh t - 1 = 2 * Real.sinh (t / 2) ^ 2 := by
  80      rw [show t = 2 * (t / 2) by ring, Real.cosh_two_mul, Real.cosh_sq]
  81      ring
  82    have hbound : t ^ 2 / 2 ≤ Real.cosh t - 1 := by
  83      rw [hformula]
  84      nlinarith
  85    simpa [t, mul_assoc, mul_left_comm, mul_comm, pow_two] using hbound
  86  · have hformula_neg : Real.cosh t - 1 = Real.cosh (-t) - 1 := by
  87      simp [Real.cosh_neg]
  88    have hsq_neg : t ^ 2 / 2 = (-t) ^ 2 / 2 := by ring
  89    have hpos_case :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.