OAI/Analysis/MumfordShah/HarmonicAnalysis.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah harmonic analysis.

  1. def OAI.MumfordShah.complexPartial line 76
  2. lemma OAI.MumfordShah.directional_eq_re_mul_complexPartial line 79
  3. theorem OAI.MumfordShah.harmonic_fderiv_eq_of_directional_constant line 91
  4. theorem OAI.MumfordShah.harmonic_affine_of_directional_constant line 120
  5. theorem OAI.MumfordShah.harmonic_eq_of_minimum_on_ball line 137
  6. theorem OAI.MumfordShah.translated_energy_forces_constant_interactions line 164
  7. theorem OAI.MumfordShah.continuous_eq_zero_of_smooth_tests line 182
  8. theorem OAI.MumfordShah.harmonic_affine_of_jump_tests line 195
  9. theorem OAI.MumfordShah.constant_field_eq_zero_of_linear_energy_growth line 235
  10. lemma OAI.MumfordShah.integrableOn_mul_continuousOn_compact line 270
  11. theorem OAI.MumfordShah.analytic_compact_translation_integral line 280
  12. theorem OAI.MumfordShah.harmonic_compact_gradient_interaction line 316
  13. lemma OAI.MumfordShah.weak_gradient_zero_off_compact_support line 341
  14. lemma OAI.MumfordShah.compact_tube_inside line 350
  15. theorem OAI.MumfordShah.harmonic_translated_compact_source line 359
  16. lemma OAI.MumfordShah.testable_inverse_decay_pairing_zero line 384
  17. lemma OAI.MumfordShah.remove_testable_projection_interaction line 403