jcost_eq_zero_iff

formal source

  39theorem jcost_nonneg' {x : ℝ} (hx : 0 < x) : 0 ≤ Jcost x := Jcost_nonneg hx
  40
  41/-- **F1.1.3**: J(x) = 0 iff x = 1 (for x > 0) -/
  42theorem jcost_eq_zero_iff {x : ℝ} (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
  43  constructor
  44  · intro h
  45    have hne : x ≠ 0 := ne_of_gt hx
  46    rw [Jcost_eq_sq hne] at h
  47    have hden : 0 < 2 * x := by positivity
  48    have hsq : (x - 1) ^ 2 = 0 := by
  49      by_contra hne'
  50      have : 0 < (x - 1) ^ 2 := by positivity
  51      have := div_pos this hden
  52      linarith
  53    have := sq_eq_zero_iff.mp hsq
  54    linarith
  55  · intro h; subst h; exact Jcost_unit0
  56
  57/-- **F1.1.4**: J(x) = J(1/x) for x > 0 -/
  58theorem jcost_reciprocal {x : ℝ} (hx : 0 < x) : Jcost x = Jcost x⁻¹ :=
  59  Jcost_symm hx
  60
  61/-- **F1.1.5**: J''(x) = x⁻³ > 0 for x > 0 (strict convexity witness).
  62    We prove the consequence: J is strictly positive away from 1. -/
  63theorem jcost_pos_away_from_one {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
  64    0 < Jcost x := Jcost_pos_of_ne_one x hx hne
  65
  66/-- **F1.1.6**: J(1) = 0 and the second derivative at 1 gives unit curvature.
  67    We state this via the quadratic approximation. -/
  68theorem jcost_unit_curvature (ε : ℝ) (hε : |ε| ≤ 1/2) :
  69    ∃ c : ℝ, Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 ∧ |c| ≤ 2 :=
  70  Jcost_one_plus_eps_quadratic ε hε
  71
  72/-- **F1.1.7**: J(eᵋ) = (eᵋ + e⁻ᵋ)/2 − 1 = cosh(ε) − 1.