xDirection

formal source

  20open Matrix
  21
  22/-- The active `x`-coordinate direction `αᵢ / xᵢ`. -/
  23noncomputable def xDirection {n : ℕ} (α x : Vec n) : Vec n :=
  24  fun i => α i / x i
  25
  26/-- The diagonal correction term appearing in the `x`-coordinate Hessian. -/
  27noncomputable def xDiagonalCorrection {n : ℕ} (α x : Vec n) (i j : Fin n) : ℝ :=
  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