OAI/Analysis/MumfordShah/GraphCalculus.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah graph calculus.

  1. def OAI.MumfordShah.graphChart line 103
  2. def OAI.MumfordShah.graphSource line 105
  3. def OAI.MumfordShah.graphUpper line 107
  4. def OAI.MumfordShah.graphJump line 109
  5. def OAI.MumfordShah.graphJumpGradient line 111
  6. lemma OAI.MumfordShah.graphSource_contDiff line 114
  7. lemma OAI.MumfordShah.graphSource_compactSupport line 120
  8. lemma OAI.MumfordShah.graphJump_compactSupport line 134
  9. lemma OAI.MumfordShah.graphUpper_isOpen line 143
  10. lemma OAI.MumfordShah.graphJump_eventuallyEq line 146
  11. lemma OAI.MumfordShah.graphJump_contDiffOn line 174
  12. lemma OAI.MumfordShah.graphJump_gradient_eq line 183
  13. lemma OAI.MumfordShah.graphJump_sobolev line 191
  14. lemma OAI.MumfordShah.graphSource_fderiv line 221
  15. lemma OAI.MumfordShah.graphChart_hasDerivAt_left line 237
  16. lemma OAI.MumfordShah.graphChart_hasDerivAt_right line 245
  17. def OAI.MumfordShah.graphDS line 251
  18. def OAI.MumfordShah.graphDR line 255
  19. lemma OAI.MumfordShah.graphDS_hasDerivAt line 260
  20. lemma OAI.MumfordShah.graphDR_hasDerivAt line 267
  21. lemma OAI.MumfordShah.graphDS_add_graphDR line 277
  22. lemma OAI.MumfordShah.graphDS_continuous line 294
  23. lemma OAI.MumfordShah.graphDR_continuous line 306
  24. lemma OAI.MumfordShah.graphDS_support line 318
  25. lemma OAI.MumfordShah.graphDR_support line 327
  26. lemma OAI.MumfordShah.graphDS_integrable line 336
  27. lemma OAI.MumfordShah.graphDR_integrable line 343
  28. lemma OAI.MumfordShah.graphDS_integral_zero line 350
  29. lemma OAI.MumfordShah.graphDR_integral_Ioi line 365