OAI/Analysis/AffineBernstein/ParametricSmoothness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.contDiffAt_inverse_matrix_entry_param line 11
2. def OAI.AffineBernstein.graphVariationJacobian line 20
3. def OAI.AffineBernstein.graphVariationSecond line 23
4. lemma OAI.AffineBernstein.contDiffAt_graphVariationJacobian line 29
5. lemma OAI.AffineBernstein.contDiffAt_graphVariationSecond line 39
6. def OAI.AffineBernstein.graphVariationRegular line 67
7. lemma OAI.AffineBernstein.isOpen_graphVariationRegular line 71
8. lemma OAI.AffineBernstein.contDiffOn_graphVariationArea line 88
9. lemma OAI.AffineBernstein.zero_mem_graphVariationRegular line 104