OAI/Geometry/TamingCompatibility/DifferentialForms/PlaneFirstVariation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.PlaneVariation.detInner_comm line 15
2. lemma OAI.TamingCompatibility.PlaneVariation.detInner_le_one line 19
3. lemma OAI.TamingCompatibility.PlaneVariation.skew_error_norm line 29
4. lemma OAI.TamingCompatibility.PlaneVariation.transverse_add line 38
5. lemma OAI.TamingCompatibility.PlaneVariation.transverse_skew line 43
6. lemma OAI.TamingCompatibility.PlaneVariation.norm_transverse_comparison line 50
7. lemma OAI.TamingCompatibility.PlaneVariation.first_variation_source_bound line 89
8. lemma OAI.TamingCompatibility.UnitaryFrame.first_variation_wedge_bound line 105
9. lemma OAI.TamingCompatibility.Concentration.cutKernel_plane_variation_bound line 133
10. lemma OAI.TamingCompatibility.Concentration.sqrt_angular_transverse line 153