OAI/Analysis/MumfordShah/CompactExclusion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah compact exclusion.

  1. instance OAI.MumfordShah.compactExclusionGradientCompleteSpace line 147
  2. lemma OAI.MumfordShah.connected_complement_of_null_subset line 151
  3. lemma OAI.MumfordShah.affine_gradient_ae line 158
  4. lemma OAI.MumfordShah.gradient_zero_of_affine_decomposition line 170
  5. theorem OAI.MumfordShah.minimizer_gradient_zero_of_compact_piece line 208
  6. instance OAI.MumfordShah.compactExclusionConstantCompleteSpace line 243
  7. lemma OAI.MumfordShah.global_admissible_constant_of_gradient_zero line 247
  8. lemma OAI.MumfordShah.sobolevOn_constant line 292
  9. theorem OAI.MumfordShah.no_compact_piece_of_gradient_zero line 299
  10. theorem OAI.MumfordShah.compactPieceExclusion line 354