OAI/Geometry/TamingCompatibility/Functional/HermitianRadialProfiles.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.RadialPotential.hermitianGraph line 14
2. lemma OAI.TamingCompatibility.RadialPotential.hermitianGraph_apply line 18
3. lemma OAI.TamingCompatibility.RadialPotential.hermitianGraph_norm_sq line 21
4. lemma OAI.TamingCompatibility.RadialPotential.hermitianGraph_inner line 25
5. lemma OAI.TamingCompatibility.RadialPotential.hermitianGraph_complex_pair line 28
6. lemma OAI.TamingCompatibility.RadialPotential.linear_pullback_hessian line 39
7. def OAI.TamingCompatibility.RadialPotential.hermitianLogPotential line 52
8. def OAI.TamingCompatibility.RadialPotential.hermitianSqrtPotential line 55
9. lemma OAI.TamingCompatibility.RadialPotential.hermitianLogPotential_smooth line 58
10. lemma OAI.TamingCompatibility.RadialPotential.hermitianSqrtPotential_smooth line 62
11. lemma OAI.TamingCompatibility.RadialPotential.hermitianLog_ddc_lower line 66
12. lemma OAI.TamingCompatibility.RadialPotential.hermitianSqrt_ddc_lower line 83