OAI/Analysis/MumfordShah/ExteriorPotential.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah exterior potential.

  1. lemma OAI.MumfordShah.sq_integral_mul_le line 87
  2. lemma OAI.MumfordShah.radialBump_integral_scale line 100
  3. lemma OAI.MumfordShah.radialBump_sq_integral_scale line 105
  4. lemma OAI.MumfordShah.continuous_extension_closedBall line 110
  5. lemma OAI.MumfordShah.radialBump_local_mean line 118
  6. lemma OAI.MumfordShah.harmonic_l2_point_bound line 154
  7. lemma OAI.MumfordShah.integral_square_tail_tendsto_zero line 186
  8. lemma OAI.MumfordShah.integral_ball_translate line 202
  9. lemma OAI.MumfordShah.harmonic_l2_exterior_little_o line 211
  10. lemma OAI.MumfordShah.holomorphic_l2_exterior_little_o line 260
  11. lemma OAI.MumfordShah.exterior_holomorphic_double_zero line 275
  12. lemma OAI.MumfordShah.fderiv_eq_re_complexPartial line 309
  13. lemma OAI.MumfordShah.real_fderiv_of_hasDerivAt line 317
  14. lemma OAI.MumfordShah.punctured_ball_preconnected line 322
  15. lemma OAI.MumfordShah.harmonic_inversion_analytic_representation line 341
  16. lemma OAI.MumfordShah.complexPartial_eq_conj_gradient line 395
  17. theorem OAI.MumfordShah.finite_energy_harmonic_exterior_representation line 407
  18. lemma OAI.MumfordShah.eventually_nhds_of_cocompact line 444
  19. lemma OAI.MumfordShah.inverted_analytic_iteratedDeriv line 452
  20. lemma OAI.MumfordShah.inverted_analytic_derivative_decay line 480
  21. lemma OAI.MumfordShah.real_part_inverse_derivative_decay line 494
  22. lemma OAI.MumfordShah.eventual_representation_derivative_decay line 519
  23. theorem OAI.MumfordShah.projection_has_normalized_exterior_potential line 530
  24. theorem OAI.MumfordShah.compact_projection_sobolev line 556
  25. theorem OAI.MumfordShah.projection_has_testable_normalized_exterior_potential line 636