OAI/Analysis/MumfordShah/Model.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah model.

  1. abbrev OAI.MumfordShah.Plane line 16
  2. abbrev OAI.MumfordShah.lengthMeasure line 18
  3. def OAI.MumfordShah.CompactlyContained line 20
  4. def OAI.MumfordShah.essentialSupport line 23
  5. def OAI.MumfordShah.HasWeakGradientOn line 26
  6. def OAI.MumfordShah.SobolevOn line 32
  7. structure OAI.MumfordShah.Pair line 36
  8. def OAI.MumfordShah.Admissible line 41
  9. def OAI.MumfordShah.fidelityEnergy line 46
  10. def OAI.MumfordShah.IsCompactComparison line 51
  11. def OAI.MumfordShah.AbsoluteMinimizer line 55
  12. def OAI.MumfordShah.Reduced line 61
  13. def OAI.MumfordShah.Rectifiable line 65
  14. def OAI.MumfordShah.GlobalAdmissible line 69
  15. def OAI.MumfordShah.homogeneousEnergy line 75
  16. def OAI.MumfordShah.GlobalAbsoluteMinimizer line 78
  17. def OAI.MumfordShah.PositivelySeparated line 84
  18. def OAI.MumfordShah.ContainsOpenC1Arc line 87
  19. def OAI.MumfordShah.CompactPieceExclusion line 95
  20. def OAI.MumfordShah.BoundedLipschitzDomain line 103
  21. def OAI.MumfordShah.RegularHolderArc line 110
  22. def OAI.MumfordShah.InteriorArcModel line 118
  23. def OAI.MumfordShah.EndpointArcModel line 122
  24. def OAI.MumfordShah.TripleJunctionModel line 126
  25. def OAI.MumfordShah.InteriorLocalModels line 136
  26. def OAI.MumfordShah.ComponentsMeeting line 142
  27. def OAI.MumfordShah.InteriorRegularity line 145