OAI/Geometry/TamingCompatibility/Elliptic/ChartGarding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TamingCompatibility.GeometricChart.scalar_garding line 28
2. lemma OAI.TamingCompatibility.EuclideanEnergy.norm_add_sq_bound line 90
3. lemma OAI.TamingCompatibility.EuclideanEnergy.norm_smul_sq_bound line 95
4. lemma OAI.TamingCompatibility.EuclideanEnergy.two_frame_norm_bound line 100
5. lemma OAI.TamingCompatibility.EuclideanEnergy.two_frame_deriv_bound line 110
6. theorem OAI.TamingCompatibility.EuclideanEnergy.frame_h1_bound line 159