J_log_quadratic_approx

formal source

 283
 284/-- **THEOREM (GROUNDED)**: Quadratic approximation of J_log.
 285    For small perturbations, the cost is approximately quadratic in the log-ratio. -/
 286theorem J_log_quadratic_approx (ε : ℝ) (hε : |ε| < 1) :
 287    |J_log ε - ε^2 / 2| ≤ |ε|^4 / 20 := by
 288  -- J_log ε = Jcost (exp ε) = Real.cosh ε - 1
 289  have h_cosh : J_log ε = Real.cosh ε - 1 := by
 290    simp [J_log, Real.cosh_eq, Real.exp_neg]
 291  rw [h_cosh]
 292
 293
 294  have h_abs : |ε|^4 = ε^4 := by
 295    calc |ε|^4 = (|ε|^2)^2 := by ring
 296      _ = (ε^2)^2 := by rw [sq_abs]
 297      _ = ε^4 := by ring
 298  rw [h_abs]
 299  exact cosh_quadratic_bound ε hε
 300
 301
 302
 303
 304
 305
 306
 307
 308
 309/-! ## Instability in Continuous Spaces -/
 310
 311/-- A configuration is "stable" if it's a strict local minimum of J.
 312    This means there's a neighborhood where it's the unique minimizer. -/
 313def IsStable (x : ℝ) : Prop :=
 314  ∃ ε > 0, ∀ y : ℝ, y ≠ x → |y - x| < ε → defect x < defect y
 315
 316/-- In a path-connected space with continuous J, there are no isolated stable points.