OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianUniformInputs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HermitianRadial.logShellSchwartz_uniform_inputs line 22
2. lemma OAI.TamingCompatibility.HermitianRadial.logInnerSchwartz_uniform_inputs line 51
3. lemma OAI.TamingCompatibility.HermitianRadial.sqrtShellSchwartz_uniform_inputs line 80
4. lemma OAI.TamingCompatibility.HermitianRadial.sqrtInnerSchwartz_uniform_inputs line 109
5. theorem OAI.TamingCompatibility.GeometricHilbert.Hermitian.scalarCorrection_logShell_estimates line 169
6. theorem OAI.TamingCompatibility.GeometricHilbert.Hermitian.scalarCorrection_logInner_estimates line 214
7. theorem OAI.TamingCompatibility.GeometricHilbert.Hermitian.scalarCorrection_sqrtShell_estimates line 259
8. theorem OAI.TamingCompatibility.GeometricHilbert.Hermitian.scalarCorrection_sqrtInner_estimates line 301