OAI/Geometry/HypersurfaceGerms/InnerGeometry.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Balancing, collapsed circles and singular homology of conic blocks.

  1. def OAI.AmbientMultiplicity.InnerGeometry.scaleTo line 12
  2. lemma OAI.AmbientMultiplicity.InnerGeometry.scaleTo_zero line 14
  3. lemma OAI.AmbientMultiplicity.InnerGeometry.norm_scaleTo line 17
  4. lemma OAI.AmbientMultiplicity.InnerGeometry.norm_scaleTo_le line 21
  5. lemma OAI.AmbientMultiplicity.InnerGeometry.scaleTo_norm line 26
  6. lemma OAI.AmbientMultiplicity.InnerGeometry.continuous_scaleTo line 33
  7. def OAI.AmbientMultiplicity.InnerGeometry.discriminant line 49
  8. def OAI.AmbientMultiplicity.InnerGeometry.mass line 53
  9. lemma OAI.AmbientMultiplicity.InnerGeometry.discriminant_swap line 56
  10. lemma OAI.AmbientMultiplicity.InnerGeometry.discriminant_sq line 61
  11. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_nonneg line 66
  12. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_difference line 75
  13. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_product line 81
  14. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_at_zero line 88
  15. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_at_one line 93
  16. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_zero_left line 103
  17. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_same line 109
  18. lemma OAI.AmbientMultiplicity.InnerGeometry.discriminant_le_add line 115
  19. lemma OAI.AmbientMultiplicity.InnerGeometry.mass_le_max line 123
  20. def OAI.AmbientMultiplicity.InnerGeometry.radius line 138
  21. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_nonneg line 140
  22. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_sq line 142
  23. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_at_zero line 145
  24. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_same line 148
  25. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_zero_left line 151
  26. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_product line 155
  27. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_at_one_swap line 161
  28. lemma OAI.AmbientMultiplicity.InnerGeometry.radius_le_max line 164
  29. lemma OAI.AmbientMultiplicity.InnerGeometry.continuous_radius line 173
  30. def OAI.AmbientMultiplicity.InnerGeometry.balance line 180
  31. lemma OAI.AmbientMultiplicity.InnerGeometry.balance_zero line 184
  32. lemma OAI.AmbientMultiplicity.InnerGeometry.norm_balance_fst line 187
  33. lemma OAI.AmbientMultiplicity.InnerGeometry.norm_balance_snd line 194
  34. lemma OAI.AmbientMultiplicity.InnerGeometry.balance_one_equal_norms line 201
  35. lemma OAI.AmbientMultiplicity.InnerGeometry.balance_fixed line 206
  36. lemma OAI.AmbientMultiplicity.InnerGeometry.balance_product line 213
  37. lemma OAI.AmbientMultiplicity.InnerGeometry.balance_bound line 229
  38. lemma OAI.AmbientMultiplicity.InnerGeometry.continuous_balance line 238
  39. def OAI.AmbientMultiplicity.InnerGeometry.coreCoords line 256
  40. lemma OAI.AmbientMultiplicity.InnerGeometry.coreCoords_zero line 259
  41. lemma OAI.AmbientMultiplicity.InnerGeometry.coreCoords_norm_fst line 262
  42. lemma OAI.AmbientMultiplicity.InnerGeometry.coreCoords_norm_snd line 267
  43. lemma OAI.AmbientMultiplicity.InnerGeometry.coreCoords_product line 274
  44. lemma OAI.AmbientMultiplicity.InnerGeometry.continuous_coreCoords line 286
  45. lemma OAI.AmbientMultiplicity.InnerGeometry.coreCoords_eq_iff line 295
  46. lemma OAI.AmbientMultiplicity.InnerGeometry.coreCoords_surj line 312
  47. abbrev OAI.AmbientMultiplicity.InnerGeometry.ConicBlock line 338
  48. abbrev OAI.AmbientMultiplicity.InnerGeometry.BalancedBlock line 341
  49. def OAI.AmbientMultiplicity.InnerGeometry.balanceBlock line 346
  50. lemma OAI.AmbientMultiplicity.InnerGeometry.continuous_balanceBlock line 351
  51. lemma OAI.AmbientMultiplicity.InnerGeometry.balanceBlock_zero line 361
  52. lemma OAI.AmbientMultiplicity.InnerGeometry.balanceBlock_fixed line 367
  53. def OAI.AmbientMultiplicity.InnerGeometry.coreInclusion line 374
  54. def OAI.AmbientMultiplicity.InnerGeometry.coreRetraction line 378
  55. lemma OAI.AmbientMultiplicity.InnerGeometry.coreRetraction_inclusion line 383
  56. def OAI.AmbientMultiplicity.InnerGeometry.blockHomotopy line 389
  57. lemma OAI.AmbientMultiplicity.InnerGeometry.blockHomotopy_fixed line 398
  58. def OAI.AmbientMultiplicity.InnerGeometry.blockCoreHomotopyEquiv line 403
  59. def OAI.AmbientMultiplicity.InnerGeometry.collapseSetoid line 417
  60. abbrev OAI.AmbientMultiplicity.InnerGeometry.CircleCollapse line 436
  61. def OAI.AmbientMultiplicity.InnerGeometry.coreParam line 441
  62. lemma OAI.AmbientMultiplicity.InnerGeometry.continuous_coreParam line 448
  63. lemma OAI.AmbientMultiplicity.InnerGeometry.coreParam_eq_iff line 455
  64. lemma OAI.AmbientMultiplicity.InnerGeometry.coreParam_surjective line 475
  65. def OAI.AmbientMultiplicity.InnerGeometry.collapseToCore line 484
  66. lemma OAI.AmbientMultiplicity.InnerGeometry.continuous_collapseToCore line 488
  67. lemma OAI.AmbientMultiplicity.InnerGeometry.collapseToCore_bijective line 493
  68. def OAI.AmbientMultiplicity.InnerGeometry.collapseCoreHomeomorph line 506
  69. def OAI.AmbientMultiplicity.InnerGeometry.blockCollapseHomotopyEquiv line 514
  70. abbrev OAI.AmbientMultiplicity.InnerGeometry.WeightedConicBlock line 519
  71. def OAI.AmbientMultiplicity.InnerGeometry.normalizeBlock line 525
  72. def OAI.AmbientMultiplicity.InnerGeometry.weightedBlockCollapseHomotopyEquiv line 564
  73. abbrev OAI.AmbientMultiplicity.InnerGeometry.integralHomologyFunctor line 577
  74. abbrev OAI.AmbientMultiplicity.InnerGeometry.IntegralHomology line 580
  75. lemma OAI.AmbientMultiplicity.InnerGeometry.integralHomologyMap_eq_of_homotopic line 583
  76. def OAI.AmbientMultiplicity.InnerGeometry.integralHomologyIso line 594
  77. def OAI.AmbientMultiplicity.InnerGeometry.weightedBlockHomologyIso line 612