xHessianEntry_zero_cost

formal source

  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  ]
  76
  77/-- The actual `2 × 2` `x`-coordinate Hessian, with `R` specialized to the
  78weighted aggregate. -/
  79noncomputable def xHessianMatrix2 (a b x y : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  80  xHessianMatrix2OfR a b x y (aggregate (vec2 a b) (vec2 x y))
  81
  82theorem xHessianMatrix2_eq_general (a b x y : ℝ) :
  83    xHessianMatrix2 a b x y
  84      = fun i j => xHessianEntry (vec2 a b) (vec2 x y) i j := by
  85  ext i j