AnalyticMatchingColumn.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The analytic boundary column and its normalized tail representation

def OAI.DefocusingNLS.slowBoundaryColumn line 13
Source documentation
The derivative-shift formula gives an explicitly analytic boundary column.
```
noncomputable def slowBoundaryColumn (q : ℂ) (m : ℕ) (s : ℂ) : Fin 2 → ℂ :=
…
```
theorem OAI.DefocusingNLS.slowBoundaryColumn_eq_jet line 16
theorem OAI.DefocusingNLS.differentiableAt_slowBoundaryColumn line 25
theorem OAI.DefocusingNLS.analyticOnNhd_slowBoundaryColumn line 42
theorem OAI.DefocusingNLS.slowBoundaryColumn_ne_zero line 49
theorem OAI.DefocusingNLS.normalizedMatching_tail_disk line 61

theorem OAI.DefocusingNLS.normalizedMatching_ratio_column line 80

Source documentation

The backward image of the ratio column differs from the true analytic boundary column by the explicit nonzero tail scalar.

theorem normalizedMatching_ratio_column (q : ℂ) (M K : ℕ) (s : ℂ)
    (hK : 0 < K) (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0)
    (hC : normalizedMatchingC q (M + 1) s K ≠ 0) :
    backwardProduct M s q K *ᵥ
      ![normalizedMatchingB q (M + 1) s K / normalizedMatchingC q (M + 1) s K, 1] =
        (normalizedMatchingC q (M + 1) s K)⁻¹ • slowBoundaryColumn q (M + 1) s := by
…

Mentions: OAI.DefocusingNLS.normalizedMatchingC, OAI.DefocusingNLS.backwardProduct, OAI.DefocusingNLS.normalizedMatchingB, OAI.DefocusingNLS.slowBoundaryColumn