OAI/Analysis/MumfordShah/TestablePotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah testable potential.

  1. lemma OAI.MumfordShah.local_memLp_on_bounded line 25
  2. lemma OAI.MumfordShah.memLp_local_test_smul line 31
  3. lemma OAI.MumfordShah.memLp_inner_test line 46
  4. lemma OAI.MumfordShah.integrable_inner_memLp_measure line 54
  5. lemma OAI.MumfordShah.gradient_mul_smooth line 62
  6. def OAI.MumfordShah.CompactDivergenceTestable line 68
  7. lemma OAI.MumfordShah.compact_divergence_testable_of_approximation line 77
  8. theorem OAI.MumfordShah.gradient_closure_has_testable_local_potential line 155
  9. lemma OAI.MumfordShah.CompactDivergenceTestable.congr_ae line 201
  10. lemma OAI.MumfordShah.CompactDivergenceTestable.sub_const line 211