OAI/Geometry/SmoothYau/NodalMeasure/ExtrusionEquiv.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.YauCounterexamples.lowerSemicontinuous_measure_neg line 11
  2. theorem OAI.YauCounterexamples.gaussian_pi_open_pos line 35
  3. def OAI.YauCounterexamples.gaussianPairSignProduct line 42
  4. def OAI.YauCounterexamples.gaussianPairOppositeProbability line 45
  5. theorem OAI.YauCounterexamples.gaussianPairOppositeProbability_pos line 48
  6. theorem OAI.YauCounterexamples.lowerSemicontinuous_gaussianPairOppositeProbability line 63
  7. theorem OAI.YauCounterexamples.gaussian_opposite_uniform line 73
  8. def OAI.YauCounterexamples.SignTests.oppositeSet line 101
  9. def OAI.YauCounterexamples.SignTests.signMass line 104
  10. theorem OAI.YauCounterexamples.SignTests.oppositeSet_pos_mul line 108
  11. theorem OAI.YauCounterexamples.SignTests.oppositeSet_const_mul line 119
  12. theorem OAI.YauCounterexamples.SignTests.lowerSemicontinuous_measure_neg line 128
  13. theorem OAI.YauCounterexamples.SignTests.lowerSemicontinuous_signMass line 152
  14. def OAI.YauCounterexamples.SignTests.swept line 174
  15. theorem OAI.YauCounterexamples.SignTests.swept_empty line 177
  16. theorem OAI.YauCounterexamples.SignTests.swept_mono line 180
  17. theorem OAI.YauCounterexamples.SignTests.swept_iUnion line 185
  18. def OAI.YauCounterexamples.SignTests.sweptVolume line 191
  19. theorem OAI.YauCounterexamples.SignTests.swept_subset_box line 198
  20. lemma OAI.YauCounterexamples.SignTests.prod_one_special line 224
  21. lemma OAI.YauCounterexamples.SignTests.swept_box_volume line 239
  22. theorem OAI.YauCounterexamples.SignTests.sweptVolume_le_of_ediam_le line 250
  23. theorem OAI.YauCounterexamples.SignTests.sweptVolume_le_hausdorff line 283
  24. theorem OAI.YauCounterexamples.SignTests.oppositeSet_subset_swept line 308
  25. theorem OAI.YauCounterexamples.SignTests.signMass_le_hausdorff line 331
  26. def OAI.YauCounterexamples.SignTests.signCertificate line 341
  27. theorem OAI.YauCounterexamples.SignTests.lowerSemicontinuous_signCertificate line 347
  28. theorem OAI.YauCounterexamples.SignTests.signCertificate_le_hausdorff_on_union line 365
  29. theorem OAI.YauCounterexamples.SignTests.signCertificate_pos_mul line 431
  30. theorem OAI.YauCounterexamples.SignTests.signCertificate_const_mul line 439
  31. theorem OAI.YauCounterexamples.SignTests.signCertificate_le_volume line 447
  32. theorem OAI.YauCounterexamples.SignTests.signCertificate_le_hausdorff line 465
  33. theorem OAI.YauCounterexamples.SignTests.signCertificate_le_ambient_hausdorff line 477
  34. lemma OAI.YauCounterexamples.normalWaveEquiv_axis_shift line 514
  35. def OAI.YauCounterexamples.coordinateRegionMeasure line 525
  36. lemma OAI.YauCounterexamples.coordinateRegionMeasure_sign_le line 528
  37. lemma OAI.YauCounterexamples.coordinateRegionMeasure_univ line 543
  38. lemma OAI.YauCounterexamples.coordinateRegionMeasure_ae line 548
  39. instance OAI.YauCounterexamples.coordinateRegionMeasure_finite line 558
  40. theorem OAI.YauCounterexamples.coordinate_region_score_le_certificate line 562
  41. theorem OAI.YauCounterexamples.coordinate_region_score_le_nodal line 589
  42. abbrev OAI.YauCounterexamples.SignTests.extrusionEquiv line 613
  43. lemma OAI.YauCounterexamples.SignTests.extrusionEquiv_apply line 615
  44. def OAI.YauCounterexamples.SignTests.extrudeSet line 618
  45. lemma OAI.YauCounterexamples.SignTests.extrudeSet_volume line 620
  46. lemma OAI.YauCounterexamples.SignTests.tail_shift_succ line 627
  47. lemma OAI.YauCounterexamples.SignTests.head_shift_succ line 631
  48. lemma OAI.YauCounterexamples.SignTests.tail_shift_zero line 633
  49. lemma OAI.YauCounterexamples.SignTests.signMass_extrude_succ line 637
  50. lemma OAI.YauCounterexamples.SignTests.signMass_extrude_zero line 652
  51. theorem OAI.YauCounterexamples.SignTests.signCertificate_extrude line 664