OAI/Geometry/TamingCompatibility/Elliptic/DirectionH1.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.EuclideanEnergy.direction_norm_sq_bound line 17
2. lemma OAI.TamingCompatibility.EuclideanEnergy.direction_integral_bound line 34
3. lemma OAI.TamingCompatibility.GeometricChart.localizedLinear_support line 65
4. lemma OAI.TamingCompatibility.GeometricChart.schwartz_l2_norm_sq line 76
5. theorem OAI.TamingCompatibility.GeometricChart.localized_jet_bound line 87