OAI/Geometry/RCD/Transport/PointedHopfMinimizer.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual source minimizers are approximate Euclidean minimizers

  1. def OAI.RegularPointCoordinates.pointedHopfError line 13
  2. theorem OAI.RegularPointCoordinates.pointedHopfError_nonneg line 16
  3. theorem OAI.RegularPointCoordinates.pointed_hopf_minimizer_cost line 23