OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianShiftedSources.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HermitianRadial.shiftedLogSource line 14
  2. def OAI.TamingCompatibility.HermitianRadial.shiftedSqrtSource line 16
  3. def OAI.TamingCompatibility.HermitianRadial.shiftedLogShell line 19
  4. def OAI.TamingCompatibility.HermitianRadial.shiftedSqrtShell line 21
  5. def OAI.TamingCompatibility.HermitianRadial.shiftedLogInner line 24
  6. def OAI.TamingCompatibility.HermitianRadial.shiftedSqrtInner line 26
  7. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogSource_smooth line 30
  8. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtSource_smooth line 44
  9. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogShell_smooth line 58
  10. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtShell_smooth line 64
  11. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogInner_smooth line 70
  12. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtInner_smooth line 76
  13. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogShell_weight line 83
  14. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtShell_weight line 90
  15. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogInner_weight line 97
  16. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtInner_weight line 104
  17. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogShell_derivatives_bounded line 111
  18. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtShell_derivatives_bounded line 121
  19. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogInner_derivatives_bounded line 131
  20. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtInner_derivatives_bounded line 141