JacobiDeterminant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing the discrete Jacobi comparison to its determinant limit.

theorem OAI.PositiveEinsteinFour.Jacobi.scaled_determinant_limit line 18

Source documentation

The position error estimate gives the exact cubic determinant scaling for a three-dimensional normal Jacobi matrix.

theorem scaled_determinant_limit {Y : ℕ → Matrix (Fin 3) (Fin 3) ℝ}
    {J : Matrix (Fin 3) (Fin 3) ℝ} {t C : ℝ}
    (herror : ∀ᶠ (N : ℕ) in atTop, ‖(t / N) • Y N - J‖ ≤ C / N) :
    Tendsto (fun N => (t / N) ^ 3 * (Y N).det) atTop (nhds J.det) := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.compression_comparison_limit line 35

Source documentation

A finite determinant compression remains valid in the limit, including when the limiting three-dimensional compression is singular.

theorem compression_comparison_limit
    {a b : ℕ → ℝ} {P : ℕ → Matrix (Fin 3) (Fin 3) ℝ}
    {D d : ℝ} {Q : Matrix (Fin 3) (Fin 3) ℝ}
    (hd : 0 < d) (ha : Tendsto a atTop (nhds D)) (hb : Tendsto b atTop (nhds d))
    (hP : Tendsto P atTop (nhds Q))
    (hcomp : ∀ᶠ (N : ℕ) in atTop, a N / b N ≤ (P N).det) :
    D ≤ d * Q.det := by
…