OAI/Geometry/TamingCompatibility/Charts/RadialBundleSources.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.RadialPotential.tsupport_translated_mul_subset line 15
  2. lemma OAI.TamingCompatibility.RadialPotential.shiftedLogShell_support line 25
  3. lemma OAI.TamingCompatibility.RadialPotential.shiftedSqrtShell_support line 30
  4. lemma OAI.TamingCompatibility.RadialPotential.shiftedLogInner_support line 35
  5. lemma OAI.TamingCompatibility.RadialPotential.shiftedSqrtInner_support line 40
  6. lemma OAI.TamingCompatibility.RadialPotential.shiftedLogSource_support line 46
  7. lemma OAI.TamingCompatibility.RadialPotential.shiftedSqrtSource_support line 51
  8. def OAI.TamingCompatibility.RadialPotential.logShellSchwartz line 58
  9. def OAI.TamingCompatibility.RadialPotential.sqrtShellSchwartz line 63
  10. def OAI.TamingCompatibility.RadialPotential.logInnerSchwartz line 68
  11. def OAI.TamingCompatibility.RadialPotential.sqrtInnerSchwartz line 73
  12. lemma OAI.TamingCompatibility.RadialPotential.logShellSchwartz_compact line 79
  13. lemma OAI.TamingCompatibility.RadialPotential.sqrtShellSchwartz_compact line 83
  14. lemma OAI.TamingCompatibility.RadialPotential.logInnerSchwartz_compact line 87
  15. lemma OAI.TamingCompatibility.RadialPotential.sqrtInnerSchwartz_compact line 91
  16. lemma OAI.TamingCompatibility.RadialPotential.logShellSchwartz_fixedSupport line 96
  17. lemma OAI.TamingCompatibility.RadialPotential.logInnerSchwartz_fixedSupport line 101
  18. lemma OAI.TamingCompatibility.RadialPotential.sqrtShellSchwartz_fixedSupport line 106
  19. lemma OAI.TamingCompatibility.RadialPotential.sqrtInnerSchwartz_fixedSupport line 111