MatchingBoundary.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A finite-dimensional criterion excluding matching zeros

Positivity of the sum of forward cone forms excludes two dependent nonzero matching columns with nonpositive individual forms.

theorem OAI.DefocusingNLS.matchingColumnDeterminant_eq_zero_imp_smul line 15
def OAI.DefocusingNLS.matrixCone line 39
theorem OAI.DefocusingNLS.matrixCone_smul line 42

theorem OAI.DefocusingNLS.matchingColumnDeterminant_ne_zero_of_forward_forms line 49

Source documentation

A positive sum of forward forms is incompatible with two dependent nonzero columns having nonpositive individual forms.

theorem matchingColumnDeterminant_ne_zero_of_forward_forms (M : ℝ) (s₁ s₂ : ℂ)
    (T₁ T₂ : Matrix (Fin 2) (Fin 2) ℂ) (u v : Fin 2 → ℂ)
    (hu : u ≠ 0) (hv : v ≠ 0)
    (h₁ : matrixCone M s₁ T₁ u ≤ 0) (h₂ : matrixCone M s₂ T₂ v ≤ 0)
    (hpos : ∀ w : Fin 2 → ℂ, w ≠ 0 → 0 < matrixCone M s₁ T₁ w + matrixCone M s₂ T₂ w) :
    matchingColumnDeterminant u v ≠ 0 := by
…

Mentions: OAI.DefocusingNLS.matrixCone, OAI.DefocusingNLS.matchingColumnDeterminant