OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianVariableProfiles.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.HermitianRadial.variableLogProfile line 17
2. lemma OAI.TamingCompatibility.HermitianRadial.variableLogProfile_smooth line 21
3. lemma OAI.TamingCompatibility.HermitianRadial.variableLogProfile_derivatives_bounded line 50
4. def OAI.TamingCompatibility.HermitianRadial.variableSqrtProfile line 63
5. lemma OAI.TamingCompatibility.HermitianRadial.variableSqrtProfile_smooth line 67
6. lemma OAI.TamingCompatibility.HermitianRadial.variableSqrtProfile_derivatives_bounded line 96
7. lemma OAI.TamingCompatibility.HermitianRadial.variableLogProfile_shell_scale line 110
8. lemma OAI.TamingCompatibility.HermitianRadial.variableSqrtProfile_shell_scale line 122
9. lemma OAI.TamingCompatibility.HermitianRadial.innerLogProfile_smooth line 144
10. lemma OAI.TamingCompatibility.HermitianRadial.innerSqrtProfile_smooth line 165
11. lemma OAI.TamingCompatibility.HermitianRadial.innerLogProfile_derivatives_bounded line 187
12. lemma OAI.TamingCompatibility.HermitianRadial.innerSqrtProfile_derivatives_bounded line 198
13. lemma OAI.TamingCompatibility.HermitianRadial.variableLogProfile_inner_scale line 210
14. lemma OAI.TamingCompatibility.HermitianRadial.variableSqrtProfile_inner_scale line 224