OAI/Geometry/TamingCompatibility/DifferentialForms/ConstantGeometricEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.MatrixEnergy.system line 18
2. lemma OAI.TamingCompatibility.MatrixEnergy.system_integrable line 22
3. def OAI.TamingCompatibility.MatrixEnergy.constantSystem line 45
4. lemma OAI.TamingCompatibility.MatrixEnergy.constantSystem_integrable line 47
5. lemma OAI.TamingCompatibility.DirectionalEnergy.codifferential_integrable_sq line 59
6. lemma OAI.TamingCompatibility.LocalMatrixOperator.frozen_geometric_energy line 71