CotangentJacobian.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The eight-coordinate Jacobian calculation for the cotangent flow. The variational equation is kept explicit here; it will be supplied by the derivative of the actual flow with respect to its initial value.

abbrev OAI.PositiveEinsteinFour.Geometry.CotangentIndex line 19
abbrev OAI.PositiveEinsteinFour.Geometry.CotangentMatrix line 20
def OAI.PositiveEinsteinFour.Geometry.cotangentComponent line 22
def OAI.PositiveEinsteinFour.Geometry.cotangentDirection line 25
def OAI.PositiveEinsteinFour.Geometry.cotangentBasis line 28
theorem OAI.PositiveEinsteinFour.Geometry.cotangentBasis_apply line 31
theorem OAI.PositiveEinsteinFour.Geometry.cotangentBasis_repr line 37
def OAI.PositiveEinsteinFour.Geometry.cotangentProjection line 41
theorem OAI.PositiveEinsteinFour.Geometry.cotangentProjection_apply line 45
def OAI.PositiveEinsteinFour.Geometry.cotangentJacobian line 50
theorem OAI.PositiveEinsteinFour.Geometry.cotangentJacobian_eq_toMatrix line 55
theorem OAI.PositiveEinsteinFour.Geometry.cotangentJacobian_det line 76
theorem OAI.PositiveEinsteinFour.Geometry.cotangentJacobian_trace line 83
theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonian_jacobian_trace line 90
def OAI.PositiveEinsteinFour.Geometry.indexDeterminantForm line 97
def OAI.PositiveEinsteinFour.Geometry.indexDeterminantDifferential line 103
theorem OAI.PositiveEinsteinFour.Geometry.indexDeterminantDifferential_left line 107
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_indexDeterminant line 126
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_cotangentDeterminant line 139
Source documentation
Liouville's determinant identity in exactly the eight coordinates needed for the cotangent bundle. No inverse of the Jacobian is needed.
```
theorem hasDerivAt_cotangentDeterminant (J : ℝ → CotangentMatrix)
    (A : CotangentMatrix) (t : ℝ)
    (hJ : ∀ i j, HasDerivAt (fun s => J s i j) ((A * J t) i j) t) :
    HasDerivAt (fun s => (J s).det) (A.trace * (J t).det) t :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentMatrix

theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonian_variational_det line 147

Source documentation

Once the actual flow derivative satisfies its variational equation, the Hamiltonian mixed-derivative identity makes its determinant constant.

theorem cotangentHamiltonian_variational_det
    (H : CotangentCoordinates → ℝ) (γ : ℝ → CotangentCoordinates)
    (J : ℝ → CotangentMatrix) (a b s t : ℝ)
    (hs : s ∈ Set.Ioo a b) (ht : t ∈ Set.Ioo a b)
    (hH : ∀ r ∈ Set.Ioo a b, ContDiffAt ℝ ∞ H (γ r))
    (hJ : ∀ r ∈ Set.Ioo a b, ∀ i j,
      HasDerivAt (fun u => J u i j)
        ((cotangentJacobian (cotangentHamiltonianField H) (γ r) * J r) i j) r) :
    (J s).det = (J t).det := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.CotangentMatrix, OAI.PositiveEinsteinFour.Geometry.cotangentJacobian, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField

theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonian_variational_det_one line 169

Source documentation

The derivative with respect to the initial point starts at the identity matrix, so the constant Jacobian determinant is exactly one.

theorem cotangentHamiltonian_variational_det_one
    (H : CotangentCoordinates → ℝ) (γ : ℝ → CotangentCoordinates)
    (J : ℝ → CotangentMatrix) (a b t : ℝ)
    (hzero : 0 ∈ Set.Ioo a b) (ht : t ∈ Set.Ioo a b)
    (hH : ∀ r ∈ Set.Ioo a b, ContDiffAt ℝ ∞ H (γ r))
    (hJ : ∀ r ∈ Set.Ioo a b, ∀ i j,
      HasDerivAt (fun u => J u i j)
        ((cotangentJacobian (cotangentHamiltonianField H) (γ r) * J r) i j) r)
    (hinit : J 0 = 1) : (J t).det = 1 := by
…