JacobiPreconjugate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

From uniform preconjugate approximation to positive curvature matrices.

theorem OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet_eventually_posDef_of_approximation line 18

Source documentation

The exact Wronskian, uniform inverse bounds and endpoint normalization give positivity of the full discrete curvature matrix on a fine mesh.

theorem curvatureDirichlet_eventually_posDef_of_approximation
    {t : ℝ} (ht : 0 < t) (R : ℕ → ℕ → NormalMatrix)
    (hR : ∀ N i, (R N i)ᵀ = R N i)
    {B V : ℝ → NormalMatrix}
    (hB : ContinuousOn B (Set.Icc 0 t)) (hV : ContinuousOn V (Set.Icc 0 t))
    (hB0 : B 0 = 1) (hV0 : V 0 = 1)
    (hunit : ∀ s ∈ Set.Icc 0 t, IsUnit (B s))
    {eB eV : ℕ → ℝ} (heB : Tendsto eB atTop (nhds 0)) (heV : Tendsto eV atTop (nhds 0))
    (hb : ∀ᶠ N : ℕ in atTop, ∀ i : ℕ, i ≤ N + 1 →
      ‖relativeDiscretePosition (R N) (t / (N + 1)) i -
        B ((i : ℝ) * (t / (N + 1)))‖ ≤ eB N)
    (hv : ∀ᶠ N : ℕ in atTop, ∀ i : ℕ, i ≤ N →
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.relativeDiscretePosition