xHessianEntry_diag

formal source

  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]
  62  · simp [hij]
  63
  64/-- Two-component vectors written in coordinate order. -/
  65abbrev vec2 (u v : ℝ) : Vec 2 := ![u, v]
  66
  67/-- The `2 × 2` positive-coordinate Hessian with an explicit aggregate
  68parameter `R`. -/
  69noncomputable def xHessianMatrix2OfR (a b x y R : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  70  !![
  71    (a / (2 * x ^ 2)) * (((a - 1) * R) + ((a + 1) * R⁻¹)),
  72    ((a * b) / (2 * x * y)) * (R + R⁻¹);
  73    ((a * b) / (2 * x * y)) * (R + R⁻¹),
  74    (b / (2 * y ^ 2)) * (((b - 1) * R) + ((b + 1) * R⁻¹))
  75  ]