OAI/Geometry/EinsteinFour/ReferenceCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Applying the finite comparison to the actual scalar Dirichlet reference.

  1. def OAI.PositiveEinsteinFour.Jacobi.referenceMatrix line 15
  2. def OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet line 18
  3. theorem OAI.PositiveEinsteinFour.Jacobi.reference_determinant_comparison line 24

    Source documentation

    The scalar normalizer and its sine eigenmode are fully instantiated. Only positivity of the actual curvature Dirichlet matrix remains here.

    theorem reference_determinant_comparison {N : ℕ} (hN : 0 < N) (t : ℝ)
    (A : Fin N → NormalMatrix) (hA : ∀ i, (A i).trace = 0)
    (hfirst : 0 < firstEigenvalue t N) (hK : (curvatureDirichlet t A).PosDef) :
    (curvatureDirichlet t A).det / (referenceMatrix t N).det ^ 3 ≤
      ((1 : NormalMatrix) - ((t / (N + 1)) ^ 2 / firstEigenvalue t N) •
        (∑ i, unitFirstSineVector N i ^ 2 • A i)).det := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.firstEigenvalue, OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet, OAI.PositiveEinsteinFour.Jacobi.referenceMatrix, OAI.PositiveEinsteinFour.Jacobi.unitFirstSineVector