OAI/Geometry/IsometricImmersion/Darboux/QResidualActive.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.HighEquation.QActiveComponents line 13
2. theorem OAI.SmoothLocal.HighEquation.q_state_factor_eq_zero_of_spatial_inactive line 16
3. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainProduct_eq_zero_of_inactive line 28
4. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainTerm_slice_eLpNorm_two_active line 47
5. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainSum_slice_eLpNorm_two_active line 88
6. theorem OAI.SmoothLocal.HighEquation.actualQHighRemainder_slice_eLpNorm_two_active line 116