OAI/Geometry/TamingCompatibility/Hodge/HodgeFrameDifferential.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HodgeFrame.wedgeBy line 18
  2. lemma OAI.TamingCompatibility.HodgeFrame.wedgeBy_apply line 20
  3. def OAI.TamingCompatibility.HodgeFrame.combine line 23
  4. lemma OAI.TamingCompatibility.HodgeFrame.combine_apply line 25
  5. def OAI.TamingCompatibility.HodgeFrame.combineThree line 29
  6. lemma OAI.TamingCompatibility.HodgeFrame.combineThree_apply line 31
  7. lemma OAI.TamingCompatibility.HodgeFrame.extDeriv_sum line 35
  8. lemma OAI.TamingCompatibility.HodgeFrame.extDeriv_frame line 43
  9. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_star line 86
  10. lemma OAI.TamingCompatibility.HodgeFrame.star_wedge_coordinate line 107
  11. lemma OAI.TamingCompatibility.HodgeFrame.star_wedge_star_coordinate line 119
  12. def OAI.TamingCompatibility.HodgeNormalOperator.join line 137
  13. def OAI.TamingCompatibility.HodgeNormalOperator.joinCLM line 138
  14. lemma OAI.TamingCompatibility.HodgeNormalOperator.joinCLM_apply line 142
  15. def OAI.TamingCompatibility.HodgeNormalOperator.left line 144
  16. def OAI.TamingCompatibility.HodgeNormalOperator.right line 146
  17. lemma OAI.TamingCompatibility.HodgeNormalOperator.left_apply line 148
  18. lemma OAI.TamingCompatibility.HodgeNormalOperator.right_apply line 150
  19. lemma OAI.TamingCompatibility.HodgeNormalOperator.join_norm_sq line 152
  20. lemma OAI.TamingCompatibility.HodgeNormalOperator.left_add_right line 155
  21. lemma OAI.TamingCompatibility.HodgeNormalOperator.output_norm line 158
  22. def OAI.TamingCompatibility.HodgeNormalOperator.rawPrincipal line 166
  23. def OAI.TamingCompatibility.HodgeNormalOperator.lower line 171
  24. lemma OAI.TamingCompatibility.HodgeNormalOperator.combine_basis line 176
  25. def OAI.TamingCompatibility.HodgeNormalOperator.starCLM line 178
  26. lemma OAI.TamingCompatibility.HodgeNormalOperator.starCLM_apply line 181
  27. lemma OAI.TamingCompatibility.HodgeNormalOperator.combine_star_basis line 184
  28. lemma OAI.TamingCompatibility.HodgeNormalOperator.rawPrincipal_eq line 191
  29. lemma OAI.TamingCompatibility.HodgeNormalOperator.operator_expansion line 213