OAI/Analysis/MumfordShah/HarmonicProjection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah harmonic projection.

  1. lemma OAI.MumfordShah.locallyIntegrable_of_local_sobolev line 87
  2. lemma OAI.MumfordShah.weak_gradient_global_integral line 96
  3. lemma OAI.MumfordShah.complex_real_inner_formula line 107
  4. lemma OAI.MumfordShah.inner_gradient_components line 114
  5. lemma OAI.MumfordShah.integrable_inner_memLp line 124
  6. lemma OAI.MumfordShah.integrable_local_mul_test line 130
  7. lemma OAI.MumfordShah.integral_laplacian_weak_gradient line 135
  8. lemma OAI.MumfordShah.projection_test_identity line 158
  9. lemma OAI.MumfordShah.SobolevOn.congr_ae line 175
  10. lemma OAI.MumfordShah.projected_potential_weak_harmonic line 184
  11. theorem OAI.MumfordShah.projection_has_harmonic_local_potential line 199
  12. lemma OAI.MumfordShah.local_smooth_weak_derivative_ae line 211
  13. lemma OAI.MumfordShah.local_smooth_weak_gradient_ae line 244
  14. theorem OAI.MumfordShah.projection_has_classical_harmonic_potential line 258