OAI/Analysis/AffineBernstein/FlatFCalculus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.dirDeriv_sub line 16
2. lemma OAI.AffineBernstein.second_dirDeriv_sub line 23
3. lemma OAI.AffineBernstein.flatInverseTrace_sub line 38
4. lemma OAI.AffineBernstein.flatInversePair_symm line 47
5. lemma OAI.AffineBernstein.flatInversePair_sub_self line 60
6. lemma OAI.AffineBernstein.flatInversePair_sub_right line 79
7. lemma OAI.AffineBernstein.matrix_inverse_contraction_self line 88
8. lemma OAI.AffineBernstein.log_second_identity line 95
9. lemma OAI.AffineBernstein.flat_log_hessian_trace line 110