OAI/Analysis/MumfordShah/WeakHarmonic.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah weak harmonic.

  1. instance OAI.MumfordShah.(instance at line 89) line 89
  2. instance OAI.MumfordShah.(instance at line 93) line 93
  3. def OAI.MumfordShah.WeakHarmonicOn line 97
  4. lemma OAI.MumfordShah.harmonic_angle_integral line 101
  5. lemma OAI.MumfordShah.polar_weight_integrable line 112
  6. lemma OAI.MumfordShah.radial_weighted_harmonic_mean line 136
  7. def OAI.MumfordShah.radialBump line 182
  8. lemma OAI.MumfordShah.radialBump_contDiff line 185
  9. lemma OAI.MumfordShah.radialBump_radial line 195
  10. lemma OAI.MumfordShah.radialBump_nonneg line 199
  11. lemma OAI.MumfordShah.radialBump_support line 202
  12. lemma OAI.MumfordShah.radialBump_compact line 210
  13. lemma OAI.MumfordShah.radialBump_integral_pos line 215
  14. def OAI.MumfordShah.radialMollifier line 222
  15. lemma OAI.MumfordShah.radialMollifier_contDiff line 225
  16. lemma OAI.MumfordShah.radialMollifier_radial line 228
  17. lemma OAI.MumfordShah.radialMollifier_compact line 232
  18. lemma OAI.MumfordShah.radialMollifier_integral line 237
  19. lemma OAI.MumfordShah.convolution_fderiv line 241
  20. lemma OAI.MumfordShah.convolution_fderiv_apply line 249
  21. lemma OAI.MumfordShah.smooth_directional line 258
  22. lemma OAI.MumfordShah.compact_directional line 262
  23. lemma OAI.MumfordShah.fderiv_directional line 266
  24. lemma OAI.MumfordShah.convolution_second_directional line 273
  25. lemma OAI.MumfordShah.integrable_second_component line 284
  26. lemma OAI.MumfordShah.laplacian_convolution line 292
  27. lemma OAI.MumfordShah.iteratedFDeriv_two_comp_neg line 307
  28. lemma OAI.MumfordShah.laplacian_comp_sub_left line 322
  29. lemma OAI.MumfordShah.convolution_assoc_compact line 332
  30. lemma OAI.MumfordShah.scalar_convolution_comm line 351
  31. lemma OAI.MumfordShah.convolution_exchange_compact line 361
  32. lemma OAI.MumfordShah.tsupport_sub_left line 369
  33. lemma OAI.MumfordShah.closedBall_subset_inner_ball line 377
  34. lemma OAI.MumfordShah.weak_harmonic_convolution_laplacian line 384
  35. lemma OAI.MumfordShah.weak_harmonic_convolution line 397
  36. lemma OAI.MumfordShah.radialMollifier_support line 408
  37. lemma OAI.MumfordShah.radialMollifier_reproduces line 414
  38. def OAI.MumfordShah.approxBump line 430
  39. lemma OAI.MumfordShah.approxBump_tendsto line 436
  40. lemma OAI.MumfordShah.ae_approxBump_convolution line 440
  41. lemma OAI.MumfordShah.approxBump_convolution_continuous line 448
  42. lemma OAI.MumfordShah.radialMollifier_tsupport line 454
  43. lemma OAI.MumfordShah.weak_harmonic_ae_eq_radialConvolution line 458
  44. lemma OAI.MumfordShah.convolution_local_congr line 489
  45. def OAI.MumfordShah.harmonicRepresentative line 502
  46. lemma OAI.MumfordShah.harmonicRepresentative_ae line 505
  47. lemma OAI.MumfordShah.harmonicRepresentative_eq_local line 510
  48. lemma OAI.MumfordShah.WeakHarmonicOn.mono line 525
  49. lemma OAI.MumfordShah.harmonicRepresentative_regular line 530
  50. theorem OAI.MumfordShah.weak_harmonic_regular line 553