OAI/Analysis/MumfordShah/Decomposition.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah decomposition.

  1. instance OAI.MumfordShah.decompositionCompleteSpaceCompactGradientClosure line 93
  2. lemma OAI.MumfordShah.weak_gradient_integral_on line 97
  3. lemma OAI.MumfordShah.laplacian_test_zero_off_support line 107
  4. lemma OAI.MumfordShah.local_sobolev_laplacian_identity line 118
  5. lemma OAI.MumfordShah.local_smooth_weak_derivative_ae_on line 149
  6. lemma OAI.MumfordShah.local_smooth_weak_gradient_ae_on line 185
  7. theorem OAI.MumfordShah.local_sobolev_divergence_free_regular line 199
  8. theorem OAI.MumfordShah.minimizer_harmonic_decomposition line 219
  9. theorem OAI.MumfordShah.testable_compact_projection_sobolev line 307
  10. theorem OAI.MumfordShah.minimizer_testable_harmonic_decomposition line 393