OAI/Geometry/TamingCompatibility/Hodge/HodgeGeometricCoefficients.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HodgeGeometricCoefficients.baseSymbol line 18
  2. def OAI.TamingCompatibility.HodgeGeometricCoefficients.frame line 27
  3. def OAI.TamingCompatibility.HodgeGeometricCoefficients.starFrame line 29
  4. def OAI.TamingCompatibility.HodgeGeometricCoefficients.principal line 32
  5. def OAI.TamingCompatibility.HodgeGeometricCoefficients.lower line 34
  6. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.principal_smooth line 38
  7. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.frame_smooth line 49
  8. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.frameVector_smooth line 54
  9. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.derivative_smooth line 64
  10. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.starFrame_smooth line 78
  11. lemma OAI.TamingCompatibility.HodgeGeometricCoefficients.lower_smooth line 81
  12. def OAI.TamingCompatibility.HodgeMatrixEnergy.patchPrincipal line 117
  13. def OAI.TamingCompatibility.HodgeMatrixEnergy.patchLower line 121
  14. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.patchPrincipal_continuous line 124
  15. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.patchPrincipal_bound line 130
  16. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.system_patch_eq line 137
  17. theorem OAI.TamingCompatibility.HodgeMatrixEnergy.local_garding line 156