JacobiSchemeRatios.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact normalized coefficient in a discrete Jacobi pivot.

def OAI.PositiveEinsteinFour.Jacobi.relativeDiscretePosition line 13
theorem OAI.PositiveEinsteinFour.Jacobi.relativeDiscretePosition_zero line 16
theorem OAI.PositiveEinsteinFour.Jacobi.relativeDiscretePosition_pos line 19
theorem OAI.PositiveEinsteinFour.Jacobi.matrix_inverse_divided_time line 24
theorem OAI.PositiveEinsteinFour.Jacobi.normalizedDiscrete_ratio line 30
Source documentation
Rescaling the discrete solution does not change any pivot ratio.
```
theorem normalizedDiscrete_ratio (R : ℕ → NormalMatrix) {h : ℝ} (hh : h ≠ 0)
    (i : ℕ) (hX : IsUnit (discretePosition R h i).det) :
    normalizedDiscrete R h (i + 1) * (normalizedDiscrete R h i)⁻¹ =
      discretePosition R h (i + 1) * (discretePosition R h i)⁻¹ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.discretePosition, OAI.PositiveEinsteinFour.Jacobi.normalizedDiscrete
theorem OAI.PositiveEinsteinFour.Jacobi.discretePosition_ratio line 40
Source documentation
The pivot is 1 + P/i, with P the discrete velocity times the inverse of position divided by time. This identity explains the uniform near-zero positivity criterion without introducing a time cutoff.
```
theorem discretePosition_ratio (R : ℕ → NormalMatrix) {h : ℝ} (hh : h ≠ 0)
    {i : ℕ} (hi : 0 < i) (hX : IsUnit (discretePosition R h i).det) :
    discretePosition R h (i + 1) * (discretePosition R h i)⁻¹ =
      1 + ((1 : ℝ) / i) • (discreteVelocity R h (i + 1) *
        (relativeDiscretePosition R h i)⁻¹) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.discretePosition, OAI.PositiveEinsteinFour.Jacobi.discreteVelocity, OAI.PositiveEinsteinFour.Jacobi.relativeDiscretePosition