OAI/Geometry/TamingCompatibility/Charts/RadialCutoffSupported.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.RadialPotential.translatedCutoffLog line 19
  2. def OAI.TamingCompatibility.RadialPotential.translatedCutoffSqrt line 20
  3. lemma OAI.TamingCompatibility.RadialPotential.translatedCutoffLog_smooth line 23
  4. lemma OAI.TamingCompatibility.RadialPotential.translatedCutoffSqrt_smooth line 27
  5. lemma OAI.TamingCompatibility.RadialPotential.translatedCutoffLog_support line 31
  6. lemma OAI.TamingCompatibility.RadialPotential.translatedCutoffSqrt_support line 35
  7. lemma OAI.TamingCompatibility.RadialPotential.translatedCutoffLog_compact line 39
  8. lemma OAI.TamingCompatibility.RadialPotential.translatedCutoffSqrt_compact line 43
  9. lemma OAI.TamingCompatibility.RadialPotential.firstOrderSource_translatedCutoffLog line 49
  10. lemma OAI.TamingCompatibility.RadialPotential.firstOrderSource_translatedCutoffSqrt line 58
  11. def OAI.TamingCompatibility.RadialPotential.logCutoffSourceSupported line 69
  12. def OAI.TamingCompatibility.RadialPotential.sqrtCutoffSourceSupported line 77
  13. lemma OAI.TamingCompatibility.RadialPotential.logCutoffSourceSupported_eq line 86
  14. lemma OAI.TamingCompatibility.RadialPotential.sqrtCutoffSourceSupported_eq line 93
  15. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_cutoffLog_estimate line 134
  16. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_cutoffSqrt_estimate line 179