IndisputableMonolith.Cost.JcostCore

   1import IndisputableMonolith.Cost
   2
   3/-!
   4# J-Cost Core Compatibility Surface
   5
   6The canonical J-cost definitions live in the root module
   7`IndisputableMonolith.Cost`.  Older Intelligence modules imported
   8`IndisputableMonolith.Cost.JcostCore`; this file now re-exports the root
   9surface and keeps the small set of additional instances/lemmas those modules
  10used.  It intentionally does not redefine `Jcost`, `AgreesOnExp`, or the other
  11root names, so importing both modules no longer creates environment conflicts.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Cost
  16
  17noncomputable section
  18
  19@[simp] theorem Jcost_agrees_on_exp : AgreesOnExp Jcost := by
  20  intro t
  21  rfl
  22
  23instance : AveragingAgree Jcost := ⟨Jcost_agrees_on_exp⟩
  24
  25instance : SymmUnit Jcost where
  26  symmetric := by
  27    intro x hx
  28    exact Jcost_symm hx
  29  unit0 := Jcost_unit0
  30
  31instance : AveragingDerivation Jcost where
  32  toSymmUnit := (inferInstance : SymmUnit Jcost)
  33  agrees := Jcost_agrees_on_exp
  34
  35instance : JensenSketch Jcost where
  36  toSymmUnit := (inferInstance : SymmUnit Jcost)
  37  axis_upper := by
  38    intro t
  39    exact le_rfl
  40  axis_lower := by
  41    intro t
  42    exact le_rfl
  43
  44/-- J-cost derivative: `d/dx J(x) = (1 - x⁻¹^2) / 2` away from zero. -/
  45lemma Jcost_deriv (x : ℝ) (hx : x ≠ 0) :
  46    deriv Jcost x = (1 - x⁻¹ ^ 2) / 2 := by
  47  unfold Jcost
  48  have h1 : HasDerivAt (fun y : ℝ => y) 1 x := hasDerivAt_id x
  49  have h2 : HasDerivAt (fun y : ℝ => y⁻¹) (-(x ^ 2)⁻¹) x :=
  50    hasDerivAt_inv hx
  51  have h3 : HasDerivAt (fun y : ℝ => y + y⁻¹) (1 + -(x ^ 2)⁻¹) x :=
  52    h1.add h2
  53  have h4 : HasDerivAt (fun y : ℝ => (y + y⁻¹) / 2)
  54      ((1 + -(x ^ 2)⁻¹) / 2) x :=
  55    h3.div_const 2
  56  have h5 : HasDerivAt (fun y : ℝ => (y + y⁻¹) / 2 - 1)
  57      ((1 + -(x ^ 2)⁻¹) / 2) x :=
  58    h4.sub_const 1
  59  rw [h5.deriv]
  60  field_simp [hx]
  61  ring
  62
  63end
  64
  65end Cost
  66end IndisputableMonolith
  67