OAI/Analysis/MumfordShah/TranslatedCompetitor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah translated competitor.

  1. lemma OAI.MumfordShah.ae_zero_compl_essentialSupport line 52
  2. lemma OAI.MumfordShah.isClosed_essentialSupport line 69
  3. lemma OAI.MumfordShah.compact_support_weak_gradient line 84
  4. lemma OAI.MumfordShah.local_sobolev_translate line 98
  5. def OAI.MumfordShah.translatedCompetitor line 119
  6. lemma OAI.MumfordShah.translated_competitor_sobolev line 128
  7. lemma OAI.MumfordShah.compact_piece_length_finite line 151
  8. theorem OAI.MumfordShah.translated_competitor_admissible line 159
  9. lemma OAI.MumfordShah.essentialSupport_subset_closed_of_ae_zero line 185
  10. lemma OAI.MumfordShah.ae_zero_outside_essentialSupport line 196
  11. lemma OAI.MumfordShah.translated_competitor_compact_comparison line 201
  12. lemma OAI.MumfordShah.translated_length_cancel line 240
  13. lemma OAI.MumfordShah.global_minimizer_equal_length_energy line 250
  14. theorem OAI.MumfordShah.translated_comparison_limit line 276