xHessianEntry

formal source

  28  if i = j then α i / (x i) ^ 2 else 0
  29
  30/-- The `x`-coordinate Hessian entry of `JcostN`. -/
  31noncomputable def xHessianEntry {n : ℕ} (α x : Vec n) (i j : Fin n) : ℝ :=
  32  ((aggregate α x + (aggregate α x)⁻¹) / 2) * xDirection α x i * xDirection α x j
  33    - ((aggregate α x - (aggregate α x)⁻¹) / 2) * xDiagonalCorrection α x i j
  34
  35/-- The full `x`-coordinate Hessian matrix. -/
  36noncomputable def xHessianMatrix {n : ℕ} (α x : Vec n) : Fin n → Fin n → ℝ :=
  37  fun i j => xHessianEntry α x i j
  38
  39theorem xHessianEntry_offDiag {n : ℕ} (α x : Vec n) {i j : Fin n} (hij : i ≠ j) :
  40    xHessianEntry α x i j
  41      = ((aggregate α x + (aggregate α x)⁻¹) / 2) * xDirection α x i * xDirection α x j := by
  42  unfold xHessianEntry xDiagonalCorrection
  43  simp [hij]
  44
  45theorem xHessianEntry_diag {n : ℕ} (α x : Vec n) (i : Fin n) :
  46    xHessianEntry α x i i
  47      = (α i / (2 * (x i) ^ 2))
  48          * (((α i - 1) * aggregate α x) + ((α i + 1) * (aggregate α x)⁻¹)) := by
  49  unfold xHessianEntry xDirection xDiagonalCorrection
  50  simp
  51  ring
  52
  53/-- On the zero-cost locus `aggregate α x = 1`, the `x`-Hessian collapses to
  54the rank-one outer product of the active direction with itself. -/
  55theorem xHessianEntry_zero_cost {n : ℕ} (α x : Vec n) {i j : Fin n}
  56    (hR : aggregate α x = 1) :
  57    xHessianEntry α x i j = xDirection α x i * xDirection α x j := by
  58  unfold xHessianEntry xDirection xDiagonalCorrection
  59  rw [hR]
  60  by_cases hij : i = j
  61  · simp [hij]