ProfileTailError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Propagation of the strict tail disk to the actual free-profile quotient.

theorem OAI.DefocusingNLS.ProfileCertificate.normalized_profile_determinant_bound line 14
theorem OAI.DefocusingNLS.ProfileCertificate.actual_tail_error line 32
theorem OAI.DefocusingNLS.ProfileCertificate.free_profile_linear_error line 84
Source documentation
The certified small error applies to the genuine logarithmic derivative.
```
theorem free_profile_linear_error (b z : ℝ)
    (hb : |b| ≤ (radius : ℝ)) (hz : |z| ≤ (radius : ℝ)) :
    ‖freeProfileJ ((centerB : ℝ)+b) ((centerZ : ℝ)+z)-
      ((b : ℂ)*centralX+(z : ℂ)*centralY)‖ < (25/1000000000000 : ℝ) := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.freeProfileJ, OAI.DefocusingNLS.ProfileCertificate.centerB, OAI.DefocusingNLS.ProfileCertificate.centerZ, OAI.DefocusingNLS.ProfileCertificate.centralX, OAI.DefocusingNLS.ProfileCertificate.centralY