OAI/Geometry/SmoothYau/Smoothness/WeightedPair.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.weightedPair line 14
2. lemma OAI.YauCounterexamples.weightedPair_symm line 16
3. lemma OAI.YauCounterexamples.weightedPair_add_coeff line 20
4. lemma OAI.YauCounterexamples.weightedPair_smul_coeff line 23
5. lemma OAI.YauCounterexamples.weightedPair_sum_coeff line 26
6. lemma OAI.YauCounterexamples.weightedPair_add_left line 29
7. lemma OAI.YauCounterexamples.weightedPair_add_right line 32
8. lemma OAI.YauCounterexamples.weightedPair_sum_left line 35
9. lemma OAI.YauCounterexamples.weightedPair_sum_right line 39
10. lemma OAI.YauCounterexamples.weightedPair_mul line 43
11. lemma OAI.YauCounterexamples.weightedPair_derivative line 47
12. lemma OAI.YauCounterexamples.weightedPair_self_derivative line 51