OAI/Geometry/EinsteinFour/MatrixRatioPositivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Jacobi.matrix_posDef_of_quadratic line 16
2. theorem OAI.PositiveEinsteinFour.Jacobi.eventually_matrix_ratio_posDef line 33

   Source documentation

   A symmetric matrix ratio is eventually positive at every mesh node once its coefficient converges uniformly to the normalized Jacobi curve.

   theorem eventually_matrix_ratio_posDef {n : Type*} [Fintype n] [DecidableEq n]
       {t : ℝ} (ht : 0 < t) {C : ℝ → Matrix n n ℝ}
       (hC : ContinuousOn C (Set.Icc 0 t)) (hC0 : C 0 = 1)
       {P : ℕ → ℕ → Matrix n n ℝ} {e : ℕ → ℝ}
       (he : Tendsto e atTop (nhds 0))
       (happrox : ∀ᶠ N : ℕ in atTop, ∀ i : ℕ, 0 < i → i ≤ N →
         ‖P N i - C ((i : ℝ) * (t / (N + 1)))‖ ≤ e N)
       (hsym : ∀ N i : ℕ, ((1 : Matrix n n ℝ) + ((1 : ℝ) / i) • P N i)ᵀ =
         1 + ((1 : ℝ) / i) • P N i) :
       ∀ᶠ N : ℕ in atTop, ∀ i : ℕ, 0 < i → i ≤ N →
         ((1 : Matrix n n ℝ) + ((1 : ℝ) / i) • P N i).PosDef := by
   …