OAI/Geometry/TamingCompatibility/DifferentialForms/JetBasis.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.JetOperator.BasisJet line 17
  2. def OAI.TamingCompatibility.JetOperator.basisValue line 18
  3. def OAI.TamingCompatibility.JetOperator.basisProjZero line 20
  4. def OAI.TamingCompatibility.JetOperator.basisProjOne line 21
  5. def OAI.TamingCompatibility.JetOperator.basisProjTwo line 23
  6. lemma OAI.TamingCompatibility.JetOperator.schwartz_direction_any_basis line 28
  7. def OAI.TamingCompatibility.JetOperator.basisDirectionOne line 33
  8. def OAI.TamingCompatibility.JetOperator.basisDirectionTwo line 35
  9. lemma OAI.TamingCompatibility.JetOperator.basisDirectionOne_value line 37
  10. lemma OAI.TamingCompatibility.JetOperator.basisDirectionTwo_value line 43
  11. def OAI.TamingCompatibility.JetOperator.basisToCoordinate line 51
  12. lemma OAI.TamingCompatibility.JetOperator.basisToCoordinate_value line 55
  13. lemma OAI.TamingCompatibility.JetOperator.basisValue_norm line 64
  14. lemma OAI.TamingCompatibility.JetOperator.basis_linear_output_scaled_bound line 93
  15. lemma OAI.TamingCompatibility.GeometricChart.ddstar_scaled_basis_jet_bound line 136