OAI/Topology/TorusCompression/Boundary.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Boundary restoration, bundle rank bounds and elementary torus compression.

  1. abbrev OAI.TorusCompression.Slot line 14
  2. abbrev OAI.TorusCompression.Slots line 15
  3. def OAI.TorusCompression.cubeSet line 17
  4. abbrev OAI.TorusCompression.Cube line 18
  5. def OAI.TorusCompression.OnBoundary line 20
  6. lemma OAI.TorusCompression.slot_unit_ball line 22
  7. lemma OAI.TorusCompression.onBoundary_iff_frontier line 29
  8. def OAI.TorusCompression.support line 34
  9. def OAI.TorusCompression.Sparse line 37
  10. def OAI.TorusCompression.sparseParameters line 39
  11. def OAI.TorusCompression.boundarySlots line 42
  12. lemma OAI.TorusCompression.mem_support line 45
  13. lemma OAI.TorusCompression.mem_boundarySlots line 48
  14. lemma OAI.TorusCompression.support_zero line 51
  15. lemma OAI.TorusCompression.sparse_nonempty line 55
  16. lemma OAI.TorusCompression.sparse_eq_union line 58
  17. lemma OAI.TorusCompression.isClosed_sparse line 75
  18. lemma OAI.TorusCompression.sparseParameters_eq_empty line 84
  19. lemma OAI.TorusCompression.sparseParameters_eq_inter line 91
  20. lemma OAI.TorusCompression.isCompact_sparseParameters line 99
  21. lemma OAI.TorusCompression.sparseParameters_eq_parameterCube line 107
  22. def OAI.TorusCompression.restorationRadius line 115
  23. lemma OAI.TorusCompression.continuous_restorationRadius line 118
  24. lemma OAI.TorusCompression.restorationRadius_pos line 123
  25. lemma OAI.TorusCompression.restorationRadius_le_half line 128
  26. lemma OAI.TorusCompression.restorationRadius_lt_infDist line 131
  27. lemma OAI.TorusCompression.many_large_slots line 136
  28. def OAI.TorusCompression.radial line 160
  29. lemma OAI.TorusCompression.norm_radial_le_one line 163
  30. lemma OAI.TorusCompression.radial_boundary line 170
  31. lemma OAI.TorusCompression.radial_fixes_boundary line 175
  32. def OAI.TorusCompression.cutoff line 179
  33. def OAI.TorusCompression.blend line 181
  34. lemma OAI.TorusCompression.cutoff_range line 184
  35. lemma OAI.TorusCompression.blend_sub line 189
  36. lemma OAI.TorusCompression.norm_blend_sub_le line 194
  37. lemma OAI.TorusCompression.blend_nonzero line 200
  38. lemma OAI.TorusCompression.blend_fixes_boundary line 213
  39. lemma OAI.TorusCompression.continuous_blend line 218
  40. lemma OAI.TorusCompression.continuous_blend_of line 222
  41. theorem OAI.TorusCompression.boundary_restoration line 229
  42. theorem OAI.TorusCompression.boundary_restoration_of_sparseParameters line 278
  43. def OAI.TorusCompression.torusLocus line 298
  44. abbrev OAI.TorusCompression.TorusLocus line 302
  45. def OAI.TorusCompression.locusDifference line 305
  46. lemma OAI.TorusCompression.isClosed_torusLocus line 309
  47. lemma OAI.TorusCompression.isCompact_sparse_torusLocus line 323
  48. lemma OAI.TorusCompression.continuous_locusDifference line 331
  49. def OAI.TorusCompression.slotBundleFiber line 345
  50. lemma OAI.TorusCompression.mem_slotBundleFiber line 351
  51. def OAI.TorusCompression.EmbeddedTotal line 357
  52. instance OAI.TorusCompression.(instance at line 360) line 360
  53. structure OAI.TorusCompression.BundleMono line 364
  54. def OAI.TorusCompression.slotBundleFiberEquiv line 370
  55. lemma OAI.TorusCompression.finrank_slotBundleFiber line 382
  56. lemma OAI.TorusCompression.BundleMono.finrank_le line 389
  57. theorem OAI.TorusCompression.rank_le_target_of_nonempty_locus line 395
  58. def OAI.TorusCompression.slotIndex line 404
  59. lemma OAI.TorusCompression.slotIndex_val line 407
  60. def OAI.TorusCompression.powerMap line 411
  61. lemma OAI.TorusCompression.continuous_powerMap line 414
  62. def OAI.TorusCompression.concatenate line 418
  63. lemma OAI.TorusCompression.concatenate_slot line 423
  64. lemma OAI.TorusCompression.boundarySlots_concatenate_sum line 428
  65. lemma OAI.TorusCompression.continuous_concatenate line 440
  66. def OAI.TorusCompression.IsCompression line 448
  67. def OAI.TorusCompression.ArbitrarilyCompresses line 455
  68. theorem OAI.TorusCompression.compression_pullback line 460
  69. theorem OAI.TorusCompression.arbitrarily_compresses_pullback line 472
  70. theorem OAI.TorusCompression.arbitrarily_compresses_of_isEmpty line 481
  71. lemma OAI.TorusCompression.repeated_compression line 491
  72. theorem OAI.TorusCompression.arbitrarily_compresses_of_empty_locus line 508
  73. lemma OAI.TorusCompression.floor_batch_lower_bound line 551
  74. theorem OAI.TorusCompression.padding_boundary_fraction line 556