OAI/Analysis/AffineBernstein/DualHeightCalculus.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AffineBernstein.dualHeight line 20

    Source documentation

    Legendre tangent height pulled back by the actual gradient. No global Legendre transform or assumed dual regularity is needed for these identities.

    def dualHeight {n : ℕ} (u : Space n → ℝ) (x : Space n) : ℝ := tangentHeight u x 0

    Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.tangentHeight

  2. def OAI.AffineBernstein.positionEnergy line 22
  3. def OAI.AffineBernstein.positionSquared line 24
  4. lemma OAI.AffineBernstein.dualHeight_expansion line 26
  5. lemma OAI.AffineBernstein.contDiffOn_dualHeight line 33
  6. lemma OAI.AffineBernstein.dirDeriv_coordinate line 41
  7. lemma OAI.AffineBernstein.dirDeriv_dualHeight line 47
  8. lemma OAI.AffineBernstein.contDiff_positionEnergy line 75
  9. lemma OAI.AffineBernstein.dirDeriv_positionEnergy line 78
  10. lemma OAI.AffineBernstein.hessian_positionEnergy line 95
  11. lemma OAI.AffineBernstein.inverseHessianTrace_positionEnergy line 102
  12. lemma OAI.AffineBernstein.inverseHessianPair_dualHeight line 106
  13. lemma OAI.AffineBernstein.inverseHessianTrace_dualHeight line 120