OAI/Geometry/SmoothYau/Estimates/DerivExpSmulZero.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.hasDerivAt_exp_smul_zero line 14
2. lemma OAI.YauCounterexamples.exp_smul_apply_deriv_zero line 19
3. lemma OAI.YauCounterexamples.exp_pairing_first_variation line 24
4. lemma OAI.YauCounterexamples.clm_exp_fix_kernel line 32
5. lemma OAI.YauCounterexamples.clm_exp_selfAdjoint line 53
6. lemma OAI.YauCounterexamples.pinned_exp_pairing line 74