OAI/Geometry/TamingCompatibility/Elliptic/HermitianDerivativeNorms.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.RadialPotential.linear_pullback_fderiv_norm line 15
2. lemma OAI.TamingCompatibility.RadialPotential.linear_pullback_hessian_norm line 21
3. lemma OAI.TamingCompatibility.RadialPotential.hermitianGraph_norm_ge line 37
4. lemma OAI.TamingCompatibility.RadialPotential.norm_hermitianGraph_le line 41
5. lemma OAI.TamingCompatibility.RadialPotential.norm_hermitianLog_gradient line 54
6. lemma OAI.TamingCompatibility.RadialPotential.norm_hermitianLog_hessian line 68
7. lemma OAI.TamingCompatibility.RadialPotential.norm_hermitianSqrt_gradient line 84
8. lemma OAI.TamingCompatibility.RadialPotential.norm_hermitianSqrt_hessian line 95