OAI/Geometry/TamingCompatibility/Charts/HermitianCutoffProfiles.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TamingCompatibility.HermitianRadial.cutoffLogPotentialline 15 - def
OAI.TamingCompatibility.HermitianRadial.cutoffSqrtPotentialline 18 - lemma
OAI.TamingCompatibility.HermitianRadial.cutoffLogPotential_smoothline 21 - lemma
OAI.TamingCompatibility.HermitianRadial.cutoffSqrtPotential_smoothline 25 - lemma
OAI.TamingCompatibility.HermitianRadial.cutoffLogPotential_tsupportline 29 - lemma
OAI.TamingCompatibility.HermitianRadial.cutoffSqrtPotential_tsupportline 33 - lemma
OAI.TamingCompatibility.HermitianRadial.firstOrderSource_cutoffLogline 37 - lemma
OAI.TamingCompatibility.HermitianRadial.firstOrderSource_cutoffSqrtline 48 - lemma
OAI.TamingCompatibility.HermitianRadial.firstOrderSource_cutoffLog_compactline 59 - lemma
OAI.TamingCompatibility.HermitianRadial.firstOrderSource_cutoffSqrt_compactline 65