JacobiRatioLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform convergence of the normalized velocity gives positivity of all discrete Jacobi ratios, including the first nodes next to zero.

theorem OAI.PositiveEinsteinFour.Jacobi.inverse_product_error line 14

theorem OAI.PositiveEinsteinFour.Jacobi.uniform_inverse_product_approximation line 34

Source documentation

Uniform approximation survives multiplication by the inverse on a compact interval of invertible reference matrices.

theorem uniform_inverse_product_approximation
    {R : Type*} [NormedRing R] [HasSummableGeomSeries R] [Nontrivial R]
    {B V : ℝ → R} {t : ℝ}
    (hB : ContinuousOn B (Set.Icc 0 t)) (hV : ContinuousOn V (Set.Icc 0 t))
    (hunit : ∀ s ∈ Set.Icc 0 t, IsUnit (B s))
    {b v : ℕ → ℝ → R} {e : ℕ → ℝ}
    (he : Tendsto e atTop (nhds 0)) (hepos : ∀ N, 0 ≤ e N)
    (hb : ∀ᶠ N in atTop, ∀ s ∈ Set.Icc 0 t, ‖b N s - B s‖ ≤ e N)
    (hv : ∀ᶠ N in atTop, ∀ s ∈ Set.Icc 0 t, ‖v N s - V s‖ ≤ e N) :
    ∃ D : ℝ, 0 < D ∧ ∀ᶠ N in atTop, ∀ s ∈ Set.Icc 0 t,
      IsUnit (b N s) ∧
        ‖v N s * Ring.inverse (b N s) - V s * Ring.inverse (B s)‖ ≤ D * e N := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.eventually_mesh_ratio_positive line 69

Source documentation

Uniform convergence to a continuous coefficient whose initial value is the identity gives a single mesh threshold for every positive node.

theorem eventually_mesh_ratio_positive
    {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    {t : ℝ} (ht : 0 < t) {C : ℝ → F →L[ℝ] F}
    (hC : ContinuousOn C (Set.Icc 0 t)) (hC0 : C 0 = ContinuousLinearMap.id ℝ F)
    {P : ℕ → ℕ → F →L[ℝ] F} {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) :
    ∀ᶠ N : ℕ in atTop, ∀ i : ℕ, 0 < i → i ≤ N → ∀ x : F, x ≠ 0 →
      0 < inner ℝ ((ContinuousLinearMap.id ℝ F + ((1 : ℝ) / i) • P N i) x) x := by
…