OAI/Analysis/MumfordShah/LocalPotential.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah local potential.

  1. lemma OAI.MumfordShah.lp_norm_sq_integral line 26
  2. def OAI.MumfordShah.unitMean line 32
  3. def OAI.MumfordShah.normalizedPotential line 34
  4. lemma OAI.MumfordShah.memLp_normalizedPotential line 36
  5. def OAI.MumfordShah.smoothPotentialLp line 42
  6. lemma OAI.MumfordShah.normalizedPotential_sub line 46
  7. lemma OAI.MumfordShah.smoothPotentialLp_sub line 54
  8. lemma OAI.MumfordShah.smoothPotentialLp_sq_bound line 67
  9. lemma OAI.MumfordShah.smoothPotentialLp_bound line 91
  10. lemma OAI.MumfordShah.gradient_sub_smooth line 104
  11. lemma OAI.MumfordShah.smoothPotentialLp_dist_bound line 111
  12. lemma OAI.MumfordShah.cauchySeq_smoothPotentialLp line 126
  13. lemma OAI.MumfordShah.gradient_closure_approximation line 141
  14. lemma OAI.MumfordShah.exists_localLp_limit_of_gradient_limit line 152
  15. def OAI.MumfordShah.restrictLp line 160
  16. lemma OAI.MumfordShah.restrictLp_ae line 166
  17. lemma OAI.MumfordShah.complexSquare_mono line 171
  18. lemma OAI.MumfordShah.restrict_smoothPotentialLp line 175
  19. lemma OAI.MumfordShah.localLp_limits_compatible line 185
  20. lemma OAI.MumfordShah.mem_complexSquare_of_norm_le line 201
  21. lemma OAI.MumfordShah.complexSquare_nat_cover line 206
  22. lemma OAI.MumfordShah.bounded_subset_complexSquare line 210
  23. lemma OAI.MumfordShah.glue_localLp line 219
  24. lemma OAI.MumfordShah.continuous_test_deriv line 252
  25. lemma OAI.MumfordShah.smooth_normalized_ibp line 256
  26. lemma OAI.MumfordShah.memLp_test_deriv line 286
  27. lemma OAI.MumfordShah.memLp_test_vector line 291
  28. lemma OAI.MumfordShah.lp_inner_real_test line 296
  29. lemma OAI.MumfordShah.lp_inner_vector_test line 305
  30. lemma OAI.MumfordShah.localLp_limit_weak_gradient line 315
  31. theorem OAI.MumfordShah.gradient_closure_has_local_potential line 358