OAI/Probability/SKGap/Localization/LocalVolumeEnergy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.continuous_vectorNorm line 12
  2. lemma OAI.SKGap.continuous_tapField line 16
  3. lemma OAI.SKGap.tap_remainder_sq_integrable line 20
  4. theorem OAI.SKGap.localGaussian_remainder_cond line 34
  5. lemma OAI.SKGap.vectorNorm_add_sq_young line 62
  6. theorem OAI.SKGap.local_energy_pointwise line 72
  7. lemma OAI.SKGap.localGaussianBall_compact line 119
  8. lemma OAI.SKGap.localGaussian_cond_integrable line 131
  9. def OAI.SKGap.localExponent line 136
  10. lemma OAI.SKGap.localExponent_continuous line 140
  11. lemma OAI.SKGap.localGaussian_displacement line 149
  12. lemma OAI.SKGap.localGaussian_variance_change line 163
  13. theorem OAI.SKGap.localGaussian_exponent_bound line 175
  14. theorem OAI.SKGap.localGaussian_jensen line 241