JacobiNormalized.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Removing the zero of the Jacobi matrix at its initial endpoint.

def OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi line 14
theorem OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi_zero line 16
theorem OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi_pos line 20
theorem OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi_continuousOn line 24
theorem OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi_isUnit line 35
Source documentation
Preconjugacy gives invertibility of the normalized curve on the closed interval, including its value one at the initial endpoint.
```
theorem normalizedJacobi_isUnit {J : ℝ → R} {t : ℝ}
    (hJ0 : J 0 = 0) (hJ : HasDerivAt J 1 0)
    (hpre : ∀ s, 0 < s → s ≤ t → IsUnit (J s)) :
    ∀ s ∈ Set.Icc 0 t, IsUnit (normalizedJacobi J s) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi

theorem OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi_inverse_neighborhood line 53

Source documentation

Uniform inverse control applies through zero without a lower time cutoff. The actual Jacobi matrix itself vanishes at zero.

theorem normalizedJacobi_inverse_neighborhood {J : ℝ → R} {t : ℝ}
    (hc : ContinuousOn J (Set.Icc 0 t)) (hJ0 : J 0 = 0) (hJ : HasDerivAt J 1 0)
    (hpre : ∀ s, 0 < s → s ≤ t → IsUnit (J s)) :
    ∃ K : ℝ, 0 < K ∧ ∀ s ∈ Set.Icc 0 t, ∀ A : R,
      ‖A - normalizedJacobi J s‖ ≤ 1 / (2 * K) →
      IsUnit A ∧ ‖Ring.inverse A‖ ≤ 2 * K ∧
        ‖Ring.inverse A - Ring.inverse (normalizedJacobi J s)‖ ≤
          2 * K ^ 2 * ‖A - normalizedJacobi J s‖ :=
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.normalizedJacobi