OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianPhysicalJets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.HermitianRadial.logSingularSource line 14
2. def OAI.TamingCompatibility.HermitianRadial.sqrtSingularSource line 16
3. lemma OAI.TamingCompatibility.HermitianRadial.logShell_eq_normalized line 20
4. lemma OAI.TamingCompatibility.HermitianRadial.sqrtShell_eq_normalized line 30
5. lemma OAI.TamingCompatibility.HermitianRadial.logInner_eq_normalized line 38
6. lemma OAI.TamingCompatibility.HermitianRadial.sqrtInner_eq_normalized line 48
7. lemma OAI.TamingCompatibility.HermitianRadial.logShell_derivatives_bounded line 55
8. lemma OAI.TamingCompatibility.HermitianRadial.sqrtShell_derivatives_bounded line 82
9. lemma OAI.TamingCompatibility.HermitianRadial.logInner_derivatives_bounded line 103
10. lemma OAI.TamingCompatibility.HermitianRadial.sqrtInner_derivatives_bounded line 128