OAI/Geometry/TamingCompatibility/Charts/HermitianBundleSources.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogShell_support line 15
  2. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtShell_support line 20
  3. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogInner_support line 25
  4. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtInner_support line 30
  5. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogSource_support line 36
  6. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtSource_support line 41
  7. def OAI.TamingCompatibility.HermitianRadial.logShellSchwartz line 48
  8. def OAI.TamingCompatibility.HermitianRadial.sqrtShellSchwartz line 53
  9. def OAI.TamingCompatibility.HermitianRadial.logInnerSchwartz line 58
  10. def OAI.TamingCompatibility.HermitianRadial.sqrtInnerSchwartz line 63
  11. lemma OAI.TamingCompatibility.HermitianRadial.logShellSchwartz_compact line 69
  12. lemma OAI.TamingCompatibility.HermitianRadial.sqrtShellSchwartz_compact line 73
  13. lemma OAI.TamingCompatibility.HermitianRadial.logInnerSchwartz_compact line 77
  14. lemma OAI.TamingCompatibility.HermitianRadial.sqrtInnerSchwartz_compact line 81
  15. lemma OAI.TamingCompatibility.HermitianRadial.logShellSchwartz_fixedSupport line 86
  16. lemma OAI.TamingCompatibility.HermitianRadial.logInnerSchwartz_fixedSupport line 91
  17. lemma OAI.TamingCompatibility.HermitianRadial.sqrtShellSchwartz_fixedSupport line 96
  18. lemma OAI.TamingCompatibility.HermitianRadial.sqrtInnerSchwartz_fixedSupport line 101