OAI/Analysis/MumfordShah/SobolevAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah sobolev algebra.

  1. lemma OAI.MumfordShah.test_deriv_integral_eq_zero line 43
  2. lemma OAI.MumfordShah.SobolevOn.sub_const line 56
  3. lemma OAI.MumfordShah.SobolevOn.sub line 77
  4. lemma OAI.MumfordShah.SobolevOn.mono line 97
  5. lemma OAI.MumfordShah.SobolevOn.congr_gradient line 113
  6. lemma OAI.MumfordShah.weak_gradient_zero_on line 124
  7. lemma OAI.MumfordShah.SobolevOn.mul_smooth line 160
  8. lemma OAI.MumfordShah.SobolevOn.translate line 211
  9. lemma OAI.MumfordShah.Rectifiable.mono line 241
  10. lemma OAI.MumfordShah.Rectifiable.union line 246
  11. lemma OAI.MumfordShah.Rectifiable.translate line 275
  12. lemma OAI.MumfordShah.translate_set_eq_preimage line 301
  13. lemma OAI.MumfordShah.translated_length line 310