RootDiskApplication.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Applying the rational certificates to the separator polynomials

theorem OAI.DefocusingNLS.SeparatorArithmetic.scaledSeparatorPolynomial_degree line 15
theorem OAI.DefocusingNLS.SeparatorArithmetic.eval_degree_fifteen line 21
theorem OAI.DefocusingNLS.SeparatorArithmetic.diskErrorBound_eq_sum line 32
theorem OAI.DefocusingNLS.SeparatorArithmetic.complex_taylor_coeff line 42
theorem OAI.DefocusingNLS.SeparatorArithmetic.root_in_certified_disk line 49
Source documentation
Every certified disk contains an actual zero of the translated, scaled separator polynomial.
```
theorem root_in_certified_disk (ℓ : Fin 4) (j : Fin 15) :
    ∃ z : ℂ, ‖z - (diskCenters ℓ j : ℂ)‖ ≤ 100 ∧
      ((scaledSeparatorPolynomial ℓ).map GaussianInt.toComplex).IsRoot z := by
…
```
Mentions: OAI.DefocusingNLS.SeparatorArithmetic.diskCenters, OAI.DefocusingNLS.SeparatorArithmetic.scaledSeparatorPolynomial
theorem OAI.DefocusingNLS.SeparatorArithmetic.scaledSeparatorPolynomial_complex_ne_zero line 80
theorem OAI.DefocusingNLS.SeparatorArithmetic.complex_disk_centers_separated line 87
theorem OAI.DefocusingNLS.SeparatorArithmetic.zero_tail_no_axis_zero line 103
theorem OAI.DefocusingNLS.SeparatorArithmetic.zero_tail_positive_root_count line 121
Source documentation
The zero-tail polynomial has exactly two, one, zero, zero roots in the open right half-plane, for angular modes zero through three respectively.
```
theorem zero_tail_positive_root_count (ℓ : Fin 4) :
    (((scaledSeparatorPolynomial ℓ).map GaussianInt.toComplex).roots.toFinset.filter
      (fun z => 0 < z.re)).card = positiveRootCount ℓ := by
…
```
Mentions: OAI.DefocusingNLS.SeparatorArithmetic.scaledSeparatorPolynomial, OAI.DefocusingNLS.SeparatorArithmetic.positiveRootCount
theorem OAI.DefocusingNLS.SeparatorArithmetic.zero_tail_closed_half_plane_count line 141