OAI/Analysis/MatrixSigning/Potential/NormTCoord.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Variational.norm_tCoord_le line 32
2. lemma OAI.CurrentKS.Variational.norm_uCoord_le line 37
3. lemma OAI.CurrentKS.Variational.norm_pCoord_le line 42
4. lemma OAI.CurrentKS.Variational.norm_xCoord_le line 47
5. lemma OAI.CurrentKS.Variational.norm_yCoord_le line 53
6. lemma OAI.CurrentKS.Variational.norm_mCoord_le line 59
7. lemma OAI.CurrentKS.Variational.norm_nCoord_le line 65
8. lemma OAI.CurrentKS.Variational.norm_pairEquiv_symm_le line 72
9. lemma OAI.CurrentKS.Variational.norm_one_le_dimension line 81
10. lemma OAI.CurrentKS.Variational.norm_identityPair_le_dimension line 86