OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/ParameterBoxHomotopy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite zero-tail count throughout the certified parameter box

  1. def OAI.DefocusingNLS.certifiedParameterSegment line 14
  2. theorem OAI.DefocusingNLS.certifiedParameterSegment_zero line 17
  3. theorem OAI.DefocusingNLS.certifiedParameterSegment_one line 20
  4. theorem OAI.DefocusingNLS.certifiedParameterSegment_bound line 23
  5. theorem OAI.DefocusingNLS.continuous_zeroTail_parameterSegment line 38
  6. theorem OAI.DefocusingNLS.exists_zeroTail_parameter_count line 51

    Source documentation

    The certified boundary stays zero-free along the straight parameter segment. Only the published rectangle Rouché input is assumed.

    theorem exists_zeroTail_parameter_count (hR : RectangleRouche) (ell : Fin 4) :
    ∃ V : ℝ, 0 < V ∧ ∀ W : ℝ, V < W → ∀ b Z : ℝ,
      |100000000 * b - 33477607| ≤ 2 → |100000000 * Z - 270506819| ≤ 2 →
      rectangleZeroCount W
          (spectralHomotopyDeterminant ell (33477607 / 100000000)
            (270506819 / 100000000) 0) =
        rectangleZeroCount W (spectralHomotopyDeterminant ell b Z 0) := by
…

    Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.rectangleZeroCount, OAI.DefocusingNLS.spectralHomotopyDeterminant