OAI/Geometry/IsometricImmersion/Calculus/AffineTensorJetBounds.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.affineTensorCongruenceValue line 14
  2. theorem OAI.SmoothLocal.Geometry.affineTensorCongruenceValue_add line 17
  3. theorem OAI.SmoothLocal.Geometry.affineTensorCongruenceValue_smul line 23
  4. def OAI.SmoothLocal.Geometry.affineTensorCongruence line 28
  5. theorem OAI.SmoothLocal.Geometry.affineTensorCongruence_apply line 35
  6. theorem OAI.SmoothLocal.Geometry.iteratedFDeriv_comp_affineInverse line 38
  7. theorem OAI.SmoothLocal.Geometry.iteratedFDeriv_affinePushforwardMetric line 56
  8. theorem OAI.SmoothLocal.Geometry.iteratedFDeriv_affinePushforwardMetric_apply line 79
  9. def OAI.SmoothLocal.Geometry.affineTensorJetFactor line 89
  10. theorem OAI.SmoothLocal.Geometry.affineTensorJetFactor_nonneg line 92
  11. theorem OAI.SmoothLocal.Geometry.norm_iteratedFDeriv_affinePushforwardMetric_le line 97
  12. theorem OAI.SmoothLocal.Geometry.affinePushforwardMetric_jet_bound_on line 119
  13. theorem OAI.SmoothLocal.Geometry.supported_affine_tensor_jet_le_seminorm line 130
  14. def OAI.SmoothLocal.Geometry.affineTensorOrderFactor line 140
  15. theorem OAI.SmoothLocal.Geometry.affineTensorOrderFactor_pos line 143
  16. theorem OAI.SmoothLocal.Geometry.affineTensorJetFactor_le_orderFactor line 148
  17. theorem OAI.SmoothLocal.Geometry.supported_affine_tensor_finite_jet_le line 159
  18. def OAI.SmoothLocal.Geometry.affineTensorEntry line 169
  19. theorem OAI.SmoothLocal.Geometry.affineTensorEntry_norm_le line 173
  20. theorem OAI.SmoothLocal.Geometry.norm_iteratedFDeriv_affinePushforwardCoefficient_le line 180
  21. theorem OAI.SmoothLocal.Geometry.supported_affine_tensor_coefficient_jet_le_seminorm line 198