OAI/Analysis/MumfordShah/LocalFlux.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah local flux.

  1. lemma OAI.MumfordShah.gradient_contDiffAt_of_two line 123
  2. lemma OAI.MumfordShah.riesz_re line 128
  3. lemma OAI.MumfordShah.riesz_im line 131
  4. lemma OAI.MumfordShah.gradient_divergence_eq_laplacian line 134
  5. lemma OAI.MumfordShah.harmonic_gradient_divergence line 147
  6. lemma OAI.MumfordShah.contDiffAt_compact_extension line 152
  7. lemma OAI.MumfordShah.harmonic_gradient_compact_extension line 173
  8. def OAI.MumfordShah.graphTube line 183
  9. lemma OAI.MumfordShah.graphTube_isCompact line 186
  10. lemma OAI.MumfordShah.graphSource_tsupport_subset line 192
  11. lemma OAI.MumfordShah.graphJumpGradient_zero_off_tube line 202
  12. lemma OAI.MumfordShah.local_graph_jump_flux line 210
  13. lemma OAI.MumfordShah.harmonic_graph_jump_flux line 240
  14. lemma OAI.MumfordShah.graph_jump_interaction_eq_flux line 264
  15. lemma OAI.MumfordShah.graph_flux_integrable line 284
  16. theorem OAI.MumfordShah.harmonic_affine_of_compact_jump_interactions line 308