ForwardConeTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Forward transport of the homotopy cone

theorem OAI.DefocusingNLS.forwardProduct_mul_backwardProduct line 11
theorem OAI.DefocusingNLS.forward_backward_apply line 32
theorem OAI.DefocusingNLS.forward_matchingHomotopyColumn line 38

theorem OAI.DefocusingNLS.forward_matchingHomotopyColumn_cone line 46

Source documentation

The finite forward image of every homotopy column has nonpositive cone. This is the input used by the counting-boundary Hermitian form.

theorem forward_matchingHomotopyColumn_cone (σ : ℝ) (ℓ K : ℕ) (q s : ℂ) (ρ : ℝ)
    (hσ : -(1 / 32 : ℝ) ≤ σ) (hK : 3 ≤ K)
    (hq : q.re = σ + (ℓ : ℝ) / 2) (hsre : s.re = 0) (hsim : s.im ≠ 0)
    (hρ : 0 ≤ ρ) (hρ1 : ρ ≤ 1) :
    coneForm ((ℓ : ℝ) + 5) s
      ((forwardProduct (ℓ + 5) s q K *ᵥ matchingHomotopyColumn (ℓ + 5) K s ρ q) 0)
      ((forwardProduct (ℓ + 5) s q K *ᵥ matchingHomotopyColumn (ℓ + 5) K s ρ q) 1) ≤ 0 := by
…

Mentions: OAI.DefocusingNLS.coneForm, OAI.DefocusingNLS.forwardProduct, OAI.DefocusingNLS.matchingHomotopyColumn

theorem OAI.DefocusingNLS.matchingHomotopyColumn_ne_zero_of_factors line 66
Source documentation
Avoiding the explicit forward/backward factors excludes a zero column, without any assumption about the determinant of the two-channel problem.
```
theorem matchingHomotopyColumn_ne_zero_of_factors (M K : ℕ) (s q : ℂ) (ρ : ℝ)
    (h₁ : (ascPochhammer ℂ K).eval q ≠ 0)
    (h₂ : (ascPochhammer ℂ K).eval (q - M) ≠ 0) :
    matchingHomotopyColumn M K s ρ q ≠ 0 := by
…
```
Mentions: OAI.DefocusingNLS.matchingHomotopyColumn