OAI/Geometry/TamingCompatibility/Charts/HermitianCutoffSupported.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HermitianRadial.translatedCutoffLog line 21
  2. def OAI.TamingCompatibility.HermitianRadial.translatedCutoffSqrt line 22
  3. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffLog_smooth line 25
  4. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffSqrt_smooth line 29
  5. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffLog_support line 33
  6. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffSqrt_support line 37
  7. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffLog_compact line 41
  8. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffSqrt_compact line 45
  9. lemma OAI.TamingCompatibility.HermitianRadial.firstOrderSource_translatedCutoffLog line 51
  10. lemma OAI.TamingCompatibility.HermitianRadial.firstOrderSource_translatedCutoffSqrt line 60
  11. def OAI.TamingCompatibility.HermitianRadial.logCutoffSourceSupported line 71
  12. def OAI.TamingCompatibility.HermitianRadial.sqrtCutoffSourceSupported line 79
  13. lemma OAI.TamingCompatibility.HermitianRadial.logCutoffSourceSupported_eq line 88
  14. lemma OAI.TamingCompatibility.HermitianRadial.sqrtCutoffSourceSupported_eq line 95
  15. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffLog_germ line 117
  16. lemma OAI.TamingCompatibility.HermitianRadial.translatedCutoffSqrt_germ line 126
  17. lemma OAI.TamingCompatibility.HermitianRadial.cutoffLog_trace_lower line 135
  18. lemma OAI.TamingCompatibility.HermitianRadial.cutoffSqrt_trace_lower line 147