OAI/MathematicalPhysics/DefocusingNLS/Certificates/PolynomialDisk.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite root certificate on a complex disk

Brouwer degree gives a root of a degree-fifteen polynomial in a prescribed disk when the constant and higher-order terms are bounded by the linear term.

  1. theorem OAI.DefocusingNLS.degree_fifteen_root_in_disk line 20

    Source documentation

    A degree-fifteen polynomial has a zero in a disk if its constant and higher-order terms are uniformly smaller than its linear term there.

    theorem degree_fifteen_root_in_disk (a b : ℂ) (c : Fin 14 → ℂ) (r : ℝ)
    (hr : 0 ≤ r) (hb : b ≠ 0)
    (hbound : ‖a‖ + ∑ i, ‖c i‖ * r ^ ((i : ℕ) + 2) ≤ ‖b‖ * r) :
    ∃ z : ℂ, ‖z‖ ≤ r ∧ a + b * z + ∑ i, c i * z ^ ((i : ℕ) + 2) = 0 := by
…