IndisputableMonolith.Foundation.Hamiltonian

declarations in this module (14)

• abbrev RRF L15
• structure MetricTensor L18
• abbrev BilinearForm L22
• def partialDeriv_v2 L25
• def metric_det L28
• def inverse_metric L31
• def HamiltonianDensity L37
• def TotalHamiltonian L49
• def StressEnergyTensor L64
• def IsTimeTranslationInvariant L80
• def H_EnergyConservation L92
• theorem energy_conservation L99
• def H_HamiltonianEquivalence L110
• theorem hamiltonian_equivalence L118