ProfileExistence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A zero of the actual free-profile matching quotient in the certified disk.

theorem OAI.DefocusingNLS.ProfileCertificate.diskProfile_linear_error line 11
theorem OAI.DefocusingNLS.ProfileCertificate.diskProfile_bound line 17
theorem OAI.DefocusingNLS.ProfileCertificate.diskProfile_boundary_margin line 34
theorem OAI.DefocusingNLS.ProfileCertificate.exists_diskProfile_zero line 47
Source documentation
The certified error and Brouwer's theorem give an actual free matching root.
```
theorem exists_diskProfile_zero :
    ∃ w : Metric.closedBall (0 : ℂ) (radius : ℝ),
      ‖w.val‖ < (radius : ℝ) ∧ diskProfile w = 0 := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.diskProfile
theorem OAI.DefocusingNLS.ProfileCertificate.freeProfileJ_eq_log_derivative line 62
Source documentation
The free matching condition is the vanishing of the actual spatial derivative.
```
theorem freeProfileJ_eq_log_derivative (b Z : ℝ) (hZ : 0 < Z) :
    freeProfileJ b Z =
      -deriv (regularizedSlowSolution (-Complex.I*(b : ℂ)) 6) (-Complex.I*(Z : ℂ))/
        regularizedSlowSolution (-Complex.I*(b : ℂ)) 6 (-Complex.I*(Z : ℂ)) := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.freeProfileJ, OAI.DefocusingNLS.regularizedSlowSolution
theorem OAI.DefocusingNLS.ProfileCertificate.exists_free_profile_matching line 73