phiCost_zero

formal source

  43noncomputable def phiCost (u : ℝ) : ℝ := Real.cosh (Real.log phi * u) - 1
  44
  45/-- phiCost(0) = 0: zero phase increment has zero cost. -/
  46theorem phiCost_zero : phiCost 0 = 0 := by
  47  simp [phiCost, Real.cosh_zero]
  48
  49/-- phiCost is symmetric: f(u) = f(−u). -/
  50theorem phiCost_symm (u : ℝ) : phiCost u = phiCost (-u) := by
  51  simp [phiCost, Real.cosh_neg, mul_neg]
  52
  53/-- phiCost is nonneg: f(u) ≥ 0 for all u. -/
  54theorem phiCost_nonneg (u : ℝ) : 0 ≤ phiCost u := by
  55  unfold phiCost
  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)