OAI/Analysis/MumfordShah/DecayComparison.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

MumfordShah decay comparison.

  1. lemma OAI.MumfordShah.eventually_cocompact_to_norm_radius line 59
  2. lemma OAI.MumfordShah.decay_to_radius line 68
  3. lemma OAI.MumfordShah.norm_sub_lower_half line 80
  4. lemma OAI.MumfordShah.translate_inverse_decay line 85
  5. lemma OAI.MumfordShah.inverse_decay_add line 102
  6. lemma OAI.MumfordShah.inverse_decay_smul line 114
  7. def OAI.MumfordShah.HasInversePowerDecay line 127
  8. lemma OAI.MumfordShah.HasInversePowerDecay.congr_ae line 130
  9. lemma OAI.MumfordShah.HasInversePowerDecay.add line 138
  10. lemma OAI.MumfordShah.HasInversePowerDecay.neg line 145
  11. lemma OAI.MumfordShah.HasInversePowerDecay.sub line 151
  12. lemma OAI.MumfordShah.HasInversePowerDecay.smul line 156
  13. lemma OAI.MumfordShah.HasInversePowerDecay.translate line 162
  14. lemma OAI.MumfordShah.hasInversePowerDecay_of_compact_support_ae line 169
  15. lemma OAI.MumfordShah.hasInversePowerDecay_of_eventual line 177
  16. lemma OAI.MumfordShah.normalized_potential_decay line 184
  17. lemma OAI.MumfordShah.normalized_potential_gradient_decay line 190
  18. lemma OAI.MumfordShah.memLp_plane_translate line 210
  19. lemma OAI.MumfordShah.HasInversePowerDecay.integrable_inner line 215
  20. lemma OAI.MumfordShah.integrate_translated_quadratic line 225
  21. theorem OAI.MumfordShah.translated_quadratic_comparison line 241