HermitianBoundaryForm.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the two-dimensional Hermitian boundary form

def OAI.DefocusingNLS.hermitianPairForm line 10
theorem OAI.DefocusingNLS.hermitianPairForm_square line 13

theorem OAI.DefocusingNLS.hermitianPairForm_pos line 22

Source documentation

The elementary two-dimensional positive-definiteness criterion.

theorem hermitianPairForm_pos (a d : ℝ) (c u v : ℂ) (ha : 0 < a)
    (hdet : 0 < a * d - Complex.normSq c) (huv : u ≠ 0 ∨ v ≠ 0) :
    0 < hermitianPairForm a d c u v := by
…

Mentions: OAI.DefocusingNLS.hermitianPairForm

theorem OAI.DefocusingNLS.positive_leading_coefficient_of_det line 37
Source documentation
A positive determinant prevents the leading coefficient from crossing zero. A single positive value therefore determines the sign on the whole line.
```
theorem positive_leading_coefficient_of_det (a d : ℝ → ℝ) (c : ℝ → ℂ)
    (ha : Continuous a) (hdet : ∀ t, 0 < a t * d t - Complex.normSq (c t))
    (t₀ : ℝ) (h₀ : 0 < a t₀) : ∀ t, 0 < a t := by
…
```
theorem OAI.DefocusingNLS.hermitianPairForm_pos_on_line line 48