OAI/Geometry/SmoothYau/Limits/RestrictedPinningPencil.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.MetricIntegralAtlas.mean_add line 22
2. def OAI.YauCounterexamples.pinningEnergyBilin line 32
3. lemma OAI.YauCounterexamples.pinningEnergyBilin_apply line 79
4. def OAI.YauCounterexamples.pinningEnergyPencil line 84
5. lemma OAI.YauCounterexamples.pinningEnergyPencil_symmetric line 104
6. def OAI.YauCounterexamples.restrictedPinningPencil line 118
7. theorem OAI.YauCounterexamples.annular_nondegenerate_pinning_tensor line 138