ProfileNonvanishing.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The computed denominator gap proves that the actual free slow profile is nonzero.

theorem OAI.DefocusingNLS.ProfileCertificate.actualZ_pos line 15
theorem OAI.DefocusingNLS.ProfileCertificate.profile_tail_disk line 22
Source documentation
The tail used in the finite product is the actual normalized analytic tail.
```
theorem profile_tail_disk (b z : ℝ) (hz : |z| ≤ (radius : ℝ)) :
    let q : ℂ := -Complex.I*(((centerB : ℝ)+b : ℝ) : ℂ)
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.centerB
theorem OAI.DefocusingNLS.ProfileCertificate.free_profile_nonzero line 46
Source documentation
No zero of H occurs anywhere in the certificate's full parameter square.
```
theorem free_profile_nonzero (b z : ℝ)
    (hb : |b| ≤ (radius : ℝ)) (hz : |z| ≤ (radius : ℝ)) :
    regularizedSlowSolution (-Complex.I*(((centerB : ℝ)+b : ℝ) : ℂ)) 6
      (-(Complex.I*(((centerZ : ℝ)+z : ℝ) : ℂ))) ≠ 0 := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.regularizedSlowSolution, OAI.DefocusingNLS.ProfileCertificate.centerB, OAI.DefocusingNLS.ProfileCertificate.centerZ