OAI/Analysis/MumfordShah/Variations.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah variations.

  1. lemma OAI.MumfordShah.integrable_mul_compact_of_continuousOn line 42
  2. lemma OAI.MumfordShah.sobolevOn_of_contDiffOn line 50
  3. lemma OAI.MumfordShah.volume_eq_zero_of_finite_length line 74
  4. lemma OAI.MumfordShah.volume_eq_zero_of_locally_finite_length line 89
  5. lemma OAI.MumfordShah.SobolevOn.add line 104
  6. lemma OAI.MumfordShah.SobolevOn.const_smul line 124
  7. lemma OAI.MumfordShah.essentialSupport_subset_tsupport line 132
  8. lemma OAI.MumfordShah.smooth_variation_admissible line 140
  9. lemma OAI.MumfordShah.smooth_variation_comparison line 152
  10. lemma OAI.MumfordShah.restrict_diff_null_set line 165
  11. lemma OAI.MumfordShah.global_minimizer_smooth_energy line 173
  12. lemma OAI.MumfordShah.linear_coefficient_eq_zero line 202
  13. theorem OAI.MumfordShah.global_minimizer_divergence_free line 210
  14. lemma OAI.MumfordShah.sobolev_bounded_cutoff_of_product_tests line 246
  15. lemma OAI.MumfordShah.SobolevOn.congr_restrict line 294
  16. lemma OAI.MumfordShah.SobolevOn.mul_smooth_bounded_extend line 310
  17. lemma OAI.MumfordShah.cutoff_sobolev_decomposition line 360