CotangentHamiltonian.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The cotangent-coordinate calculation used by the geodesic measure argument: a Hamiltonian vector field has zero coordinate divergence. Only the four-dimensional position and momentum coordinates needed here are introduced.

abbrev OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates line 18
def OAI.PositiveEinsteinFour.Geometry.positionDirection line 20
def OAI.PositiveEinsteinFour.Geometry.momentumDirection line 21
def OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField line 23
def OAI.PositiveEinsteinFour.Geometry.cotangentDivergence line 29
Source documentation
Coordinate divergence in the position and momentum basis.
```
def cotangentDivergence (X : CotangentCoordinates → CotangentCoordinates)
    (z : CotangentCoordinates) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonian_energy_rate line 34
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_cotangentHamiltonian_energy line 57
Source documentation
A solution of Hamilton's equations has zero energy derivative.
```
theorem hasDerivAt_cotangentHamiltonian_energy
    (H : CotangentCoordinates → ℝ) (γ : ℝ → CotangentCoordinates) (t : ℝ)
    (hH : DifferentiableAt ℝ H (γ t))
    (hγ : HasDerivAt γ (cotangentHamiltonianField H (γ t)) t) :
    HasDerivAt (fun s => H (γ s)) 0 t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField
theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonian_energy_constant line 65
theorem OAI.PositiveEinsteinFour.Geometry.hamiltonian_partial_derivative line 75
theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonian_divergence_zero line 88
Source documentation
The two mixed derivatives cancel in each position--momentum pair. This proves the local divergence statement; flow Jacobians and restriction to the unit-energy shell are separate geometric steps.
```
theorem cotangentHamiltonian_divergence_zero
    (H : CotangentCoordinates → ℝ) (z : CotangentCoordinates)
    (hH : ContDiffAt ℝ ∞ H z) :
    cotangentDivergence (cotangentHamiltonianField H) z = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.cotangentDivergence, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField