OAI/Geometry/TamingCompatibility/Concentration/RadialDefect.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.RadialPotential.hermitianDefect line 14
2. lemma OAI.TamingCompatibility.RadialPotential.hermitianDefect_nonneg line 19
3. lemma OAI.TamingCompatibility.RadialPotential.logPotential_trace_eq line 27
4. lemma OAI.TamingCompatibility.RadialPotential.hermitianLog_ddc_eq_defect line 39
5. lemma OAI.TamingCompatibility.RadialPotential.hermitianLog_variable_defect_lower line 54
6. lemma OAI.TamingCompatibility.RadialPotential.schwartz_hermitianLog_defect_lower line 73
7. lemma OAI.TamingCompatibility.HermitianRadial.cutoffLog_defect_lower line 98
8. lemma OAI.TamingCompatibility.GeometricChart.manifold_cutoffLog_defect_lower line 125
9. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.logForm_defect_lower line 168