OAI/Analysis/MatrixSigning/Matrices/RetractH.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Hermitian.retractH line 26
2. lemma OAI.CurrentKS.Hermitian.retractH_coe line 28
3. lemma OAI.CurrentKS.Hermitian.invH_retract line 31
4. lemma OAI.CurrentKS.Hermitian.contDiffAt_invH line 35
5. lemma OAI.CurrentKS.Hermitian.hasFDerivAt_invH line 46
6. lemma OAI.CurrentKS.Hermitian.contDiff_sandwich line 69
7. lemma OAI.CurrentKS.Hermitian.hasFDerivAt_invSandwich line 81
8. lemma OAI.CurrentKS.Hermitian.contDiffAt_invSandwich line 115