JacobiMeshInverse.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform inverse control at every node of a preconjugate mesh.

theorem OAI.PositiveEinsteinFour.Jacobi.isUnit_of_divided_time line 13

theorem OAI.PositiveEinsteinFour.Jacobi.eventually_mesh_inverse_bounds line 22

Source documentation

Invertibility is uniform on the whole closed preconjugate interval; the error threshold is independent of the mesh node.

theorem eventually_mesh_inverse_bounds
    {R : Type*} [NormedRing R] [HasSummableGeomSeries R] [Nontrivial R]
    {t : ℝ} (ht : 0 ≤ t) {B : ℝ → R}
    (hB : ContinuousOn B (Set.Icc 0 t)) (hunit : ∀ s ∈ Set.Icc 0 t, IsUnit (B s))
    {b : ℕ → ℕ → R} {e : ℕ → ℝ} (he : Tendsto e atTop (nhds 0))
    (herror : ∀ᶠ N : ℕ in atTop, ∀ i : ℕ, i ≤ N + 1 →
      ‖b N i - B ((i : ℝ) * (t / (N + 1)))‖ ≤ e N) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ N : ℕ in atTop, ∀ i : ℕ, i ≤ N + 1 →
      IsUnit (b N i) ∧ ‖Ring.inverse (b N i)‖ ≤ 2 * K ∧
        ‖Ring.inverse (b N i) - Ring.inverse (B ((i : ℝ) * (t / (N + 1))))‖ ≤
          2 * K ^ 2 * e N := by
…