OAI/Analysis/MumfordShah/ProjectionPairing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah projection pairing.

  1. instance OAI.MumfordShah.instCompleteSpaceCompactGradientClosureProjectionPairing line 72
  2. instance OAI.MumfordShah.instCompleteSpaceCompactGradientClosureProjectionPairingAux line 77
  3. lemma OAI.MumfordShah.local_memLp_add_right line 82
  4. lemma OAI.MumfordShah.gradient_comp_add_right line 100
  5. lemma OAI.MumfordShah.divergence_free_add_right line 104
  6. lemma OAI.MumfordShah.linear_growth_add_right line 116
  7. theorem OAI.MumfordShah.translated_projection_pairing_zero line 136