OAI/Geometry/TamingCompatibility/Hodge/HodgeFrozenEnergy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HodgeFrozenEnergy.directionalGradient line 18
  2. lemma OAI.TamingCompatibility.HodgeFrozenEnergy.directionalGradient_integrable line 20
  3. lemma OAI.TamingCompatibility.HodgeFrozenEnergy.directionalGradient_integral line 24
  4. lemma OAI.TamingCompatibility.HodgeFrozenEnergy.gradient_basis_control line 36
  5. lemma OAI.TamingCompatibility.HodgeFrozenEnergy.directionDeriv_expansion line 59
  6. def OAI.TamingCompatibility.HodgeFrozenEnergy.coefficient line 68
  7. def OAI.TamingCompatibility.HodgeFrozenEnergy.flatSystem line 70
  8. lemma OAI.TamingCompatibility.HodgeFrozenEnergy.frozen_system line 78
  9. lemma OAI.TamingCompatibility.HodgeFrozenEnergy.flatSystem_integral line 86
  10. theorem OAI.TamingCompatibility.HodgeFrozenEnergy.frozen_energy line 102
  11. def OAI.TamingCompatibility.HodgeFrame.coordinates line 127
  12. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_apply line 130
  13. def OAI.TamingCompatibility.HodgeFrame.basisForm line 133
  14. lemma OAI.TamingCompatibility.HodgeFrame.basisForm_apply line 135
  15. def OAI.TamingCompatibility.HodgeFrame.reconstruct line 140
  16. lemma OAI.TamingCompatibility.HodgeFrame.reconstruct_apply line 142
  17. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_basisForm line 146
  18. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_reconstruct line 153
  19. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_injective line 164
  20. lemma OAI.TamingCompatibility.HodgeFrame.reconstruct_coordinates line 179
  21. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_pairing line 185
  22. lemma OAI.TamingCompatibility.HodgeFrame.basisForm_smooth line 191
  23. lemma OAI.TamingCompatibility.HodgeFrame.coordinates_model line 205