CotangentKineticEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual kinetic Hamiltonian of the metric in one chart, and the unit-energy normalization of the cotangent lift of an orthonormal frame.

def OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian line 19
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_contDiffAt line 23
def OAI.PositiveEinsteinFour.Geometry.frameCotangentMomentum line 39
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_frame_eq_half line 45
Source documentation
Lowering the first chosen frame vector with the metric places it on the kinetic-energy shell H = 1/2.
```
theorem kineticHamiltonian_frame_eq_half (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target)
    (E : Mat4) (hE : Eᵀ * metricInChart g c x * E = 1) (k : Fin 4) :
    kineticHamiltonian g c (x, frameCotangentMomentum g c x E k) = 1 / 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian, OAI.PositiveEinsteinFour.Geometry.frameCotangentMomentum