OAI/Topology/CoarseAssembly/FilledDisc.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual filled hexagonal discs

The compact polygon is contracted by radial scaling. The triangular-lattice hat functions give a continuous map of this polygon into the scale-one Rips realization of its lattice vertices. Thus the filling is constructed, not assumed as an analytic vanishing premise.

  1. theorem OAI.CoarseAssembly.realLatticeRadius_nonneg line 22
  2. theorem OAI.CoarseAssembly.realLatticeRadius_smul line 25
  3. def OAI.CoarseAssembly.FilledDisc line 30
  4. instance OAI.CoarseAssembly.(instance at line 32) line 32
  5. instance OAI.CoarseAssembly.(instance at line 35) line 35
  6. instance OAI.CoarseAssembly.(instance at line 38) line 38
  7. def OAI.CoarseAssembly.filledDiscCenter line 48
  8. def OAI.CoarseAssembly.filledDiscContraction line 51
  9. def OAI.CoarseAssembly.discHatWeights line 69
  10. theorem OAI.CoarseAssembly.discHatWeights_apply line 72
  11. theorem OAI.CoarseAssembly.latticeHatWeights_disc_support line 75
  12. theorem OAI.CoarseAssembly.discHatWeights_total line 83
  13. def OAI.CoarseAssembly.filledToRipsPoint line 96
  14. def OAI.CoarseAssembly.filledToRips line 112