IndisputableMonolith.Cost.Ndim.Metric

   1import IndisputableMonolith.Cost.Ndim.Hessian
   2
   3/-!
   4# Cost metric in log coordinates
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Cost
   9namespace Ndim
  10
  11/-- Hessian-derived metric entry for `JlogN` in log coordinates. -/
  12noncomputable def metricEntry {n : ℕ} (α t : Vec n) (i j : Fin n) : ℝ :=
  13  hessianEntry α t i j
  14
  15@[simp] theorem metricEntry_zero {n : ℕ} (α : Vec n) (i j : Fin n) :
  16    metricEntry α (fun _ => 0) i j = α i * α j := by
  17  have hdot : dot α (fun _ => 0) = 0 := by
  18    unfold dot
  19    simp
  20  simp [metricEntry, hessianEntry, hdot]
  21
  22/-- The metric at equilibrium coincides with the outer-product Hessian model. -/
  23theorem metric_at_equilibrium_eq_hessian {n : ℕ} (α : Vec n) :
  24    metricEntry α (fun _ => 0) = hessianMatrix α := by
  25  funext i j
  26  simp [hessianMatrix]
  27
  28end Ndim
  29end Cost
  30end IndisputableMonolith
  31