OAI/Geometry/TamingCompatibility/Hodge/HodgeSymbol.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TamingCompatibility.UnitaryFrame.hodge_principal_symbol line 14
  2. theorem OAI.TamingCompatibility.UnitaryFrame.hodge_symbol_energy line 20
  3. lemma OAI.TamingCompatibility.HermitianHodge.coords_add line 35
  4. theorem OAI.TamingCompatibility.HermitianHodge.hodge_principal_symbol line 40
  5. def OAI.TamingCompatibility.MetricHodge.metricSymbol line 55
  6. lemma OAI.TamingCompatibility.MetricHodge.metricSymbol_apply line 58
  7. theorem OAI.TamingCompatibility.MetricHodge.hodge_principal_symbol line 65
  8. def OAI.TamingCompatibility.HodgeFlatEnergy.pairing line 94
  9. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_add_left line 95
  10. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_add_right line 98
  11. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_neg_left line 101
  12. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_neg_right line 102
  13. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_sub_left line 103
  14. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_sub_right line 105
  15. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_comm line 107
  16. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_partial_swap line 108
  17. lemma OAI.TamingCompatibility.HodgeFlatEnergy.pairing_field_swap line 113
  18. lemma OAI.TamingCompatibility.HodgeFlatEnergy.directionDeriv_neg line 118
  19. def OAI.TamingCompatibility.HodgeFlatEnergy.delta line 123
  20. def OAI.TamingCompatibility.HodgeFlatEnergy.star line 128
  21. def OAI.TamingCompatibility.HodgeFlatEnergy.energy line 130
  22. def OAI.TamingCompatibility.HodgeFlatEnergy.gradientEnergy line 132
  23. theorem OAI.TamingCompatibility.HodgeFlatEnergy.energy_eq_gradient line 135