OAI/Analysis/AffineBernstein/LogDetGradientEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.gradientEnergy line 17

   Source documentation

   Half the squared Euclidean gradient, expressed in the frozen orthonormal coordinates.

   def gradientEnergy {n : ℕ} (u : Space n → ℝ) (x : Space n) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

2. lemma OAI.AffineBernstein.contDiffOn_gradientEnergy line 20
3. lemma OAI.AffineBernstein.dirDeriv_gradientEnergy line 25
4. lemma OAI.AffineBernstein.inverseHessian_pair_gradient line 45
5. lemma OAI.AffineBernstein.inverseHessianTrace_gradientEnergy line 60