ForwardMatching.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Forward matching with its exact scalar factors

def OAI.DefocusingNLS.forwardMatrix line 12
Source documentation
The forward matrix before division by t-M.
```
noncomputable def forwardMatrix (M s t : ℂ) : Matrix (Fin 2) (Fin 2) ℂ :=
…
```
def OAI.DefocusingNLS.forwardProduct line 15
theorem OAI.DefocusingNLS.forwardMatrix_step line 19
theorem OAI.DefocusingNLS.forwardMatrix_mul_backwardMatrix line 30
Source documentation
Forward and backward matrices compose to precisely t(t-M) I.
```
theorem forwardMatrix_mul_backwardMatrix (M s t : ℂ) :
    forwardMatrix M s t * backwardMatrix M s t = (t * (t - M)) • (1 : Matrix (Fin 2) (Fin 2) ℂ) := by
…
```
Mentions: OAI.DefocusingNLS.forwardMatrix, OAI.DefocusingNLS.backwardMatrix
theorem OAI.DefocusingNLS.backwardMatrix_mul_forwardMatrix line 36
theorem OAI.DefocusingNLS.det_forwardMatrix line 42
theorem OAI.DefocusingNLS.det_backwardMatrix line 46

theorem OAI.DefocusingNLS.forwardProduct_apply line 51

Source documentation

Iterating forward multiplies the terminal pair by (q-M)_K.

theorem forwardProduct_apply (M s q : ℂ) (B C : ℕ → ℂ)
    (hB : ∀ n, (q + n - M) * B (n + 1) = (q + n) * B n + s * C n)
    (hC : ∀ n, C (n + 1) = C n - B (n + 1)) (K : ℕ) :
    forwardProduct M s q K *ᵥ ![B 0, C 0] =
      (ascPochhammer ℂ K).eval (q - M) • ![B K, C K] := by
…

Mentions: OAI.DefocusingNLS.forwardProduct