OAI/Analysis/MatrixSigning/Potential/Energy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.State.eta_rank_one line 16
2. lemma OAI.CurrentKS.State.inner_eta_rank_one line 24
3. def OAI.CurrentKS.State.energy line 33
4. lemma OAI.CurrentKS.State.energy_nonneg line 37
5. lemma OAI.CurrentKS.State.energy_stationary_bound line 42