OAI/Geometry/TamingCompatibility/DifferentialForms/RadialShiftedSources.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

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