OAI/Geometry/SmoothYau/Estimates/SphericalPinFormNorm.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.sphericalTensorSupport line 15
  2. abbrev OAI.YauCounterexamples.SphericalTensor line 19
  3. def OAI.YauCounterexamples.sphericalExterior line 20
  4. lemma OAI.YauCounterexamples.sphericalTensorSupport_image line 22
  5. lemma OAI.YauCounterexamples.sphericalExterior_support line 35
  6. def OAI.YauCounterexamples.sphericalTensorOf line 42
  7. lemma OAI.YauCounterexamples.sphericalExterior_mono line 46
  8. lemma OAI.YauCounterexamples.sphericalTensorOf_zero line 49
  9. lemma OAI.YauCounterexamples.sphericalRadius_sq_planar line 55
  10. lemma OAI.YauCounterexamples.spherical_regular_nonzero line 60
  11. def OAI.YauCounterexamples.SphericalSignAbove line 74
  12. def OAI.YauCounterexamples.SphericalRegular line 79
  13. def OAI.YauCounterexamples.SphericalSimple line 82
  14. def OAI.YauCounterexamples.SphericalLargeWitness line 86
  15. lemma OAI.YauCounterexamples.spherical_largeWitness_eventually line 90
  16. theorem OAI.YauCounterexamples.spherical_pin_near line 117