OAI/Analysis/MumfordShah/EnergyLimits.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah energy limits.

  1. lemma OAI.MumfordShah.integral_norm_ball_geometric_bound line 36
  2. lemma OAI.MumfordShah.interaction_annulus_bound line 78
  3. theorem OAI.MumfordShah.integrable_interaction_of_growth_decay line 134
  4. lemma OAI.MumfordShah.integrable_local_scalar_inner_test line 167
  5. lemma OAI.MumfordShah.cutoff_boundary_interaction_bound line 181
  6. theorem OAI.MumfordShah.divergence_pairing_zero_of_decay line 248
  7. lemma OAI.MumfordShah.memLp_local_scalar_gradient_test line 296
  8. lemma OAI.MumfordShah.cutoff_boundary_L2_sq_bound line 311
  9. lemma OAI.MumfordShah.tendsto_L2_zero_of_integral_sq line 348
  10. theorem OAI.MumfordShah.cutoff_field_tendsto_L2 line 361
  11. lemma OAI.MumfordShah.cutoff_integral_tendsto line 441
  12. lemma OAI.MumfordShah.cutoff_mul_integrable line 463
  13. theorem OAI.MumfordShah.cutoff_field_interaction_limit line 472
  14. lemma OAI.MumfordShah.norm_sq_energy_difference line 518
  15. lemma OAI.MumfordShah.integral_finite_energy_difference line 523
  16. theorem OAI.MumfordShah.finite_energy_limit_inequality line 552