OAI/Geometry/TamingCompatibility/DifferentialForms/RadialVariableProfiles.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.RadialPotential.variableLogProfile line 18
2. def OAI.TamingCompatibility.RadialPotential.variableSqrtProfile line 21
3. lemma OAI.TamingCompatibility.RadialPotential.variableLogProfile_smooth line 24
4. lemma OAI.TamingCompatibility.RadialPotential.variableSqrtProfile_smooth line 46
5. lemma OAI.TamingCompatibility.RadialPotential.variableLogProfile_derivatives_bounded line 68
6. lemma OAI.TamingCompatibility.RadialPotential.variableSqrtProfile_derivatives_bounded line 81
7. lemma OAI.TamingCompatibility.RadialPotential.shellCutoff_origin_not_tsupport line 95
8. lemma OAI.TamingCompatibility.RadialPotential.variableLogProfile_shell_scale line 100
9. lemma OAI.TamingCompatibility.RadialPotential.variableSqrtProfile_shell_scale line 112
10. lemma OAI.TamingCompatibility.RadialPotential.innerLogProfile_smooth line 133
11. lemma OAI.TamingCompatibility.RadialPotential.innerSqrtProfile_smooth line 147
12. lemma OAI.TamingCompatibility.RadialPotential.innerLogProfile_derivatives_bounded line 162
13. lemma OAI.TamingCompatibility.RadialPotential.innerSqrtProfile_derivatives_bounded line 173
14. lemma OAI.TamingCompatibility.RadialPotential.variableLogProfile_inner_scale line 185
15. lemma OAI.TamingCompatibility.RadialPotential.variableSqrtProfile_inner_scale line 199