OAI/Analysis/MumfordShah/GradientProjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah gradient projection.

  1. abbrev OAI.MumfordShah.PlaneL2 line 24
  2. lemma OAI.MumfordShah.continuous_gradient_of_smooth line 26
  3. lemma OAI.MumfordShah.compactSupport_gradient line 31
  4. lemma OAI.MumfordShah.memLp_gradient_of_test line 35
  5. def OAI.MumfordShah.smoothGradientSpace line 40
  6. def OAI.MumfordShah.compactGradientClosure line 63
  7. instance OAI.MumfordShah.(instance at line 66) line 66
  8. def OAI.MumfordShah.compactGradientProjection line 70
  9. def OAI.MumfordShah.compactJumpField line 73
  10. lemma OAI.MumfordShah.testGradient_mem_closure line 76
  11. theorem OAI.MumfordShah.compactJumpField_divergence_free line 82
  12. theorem OAI.MumfordShah.compactJumpField_orthogonal line 93
  13. theorem OAI.MumfordShah.compactJumpField_memLp line 97