OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileCentralEnclosures.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.ProfileCertificate.norm_toComplex_lt_of_sq line 12
2. theorem OAI.DefocusingNLS.ProfileCertificate.norm_toComplex_lt_mul line 20
3. def OAI.DefocusingNLS.ProfileCertificate.centralM line 30
4. theorem OAI.DefocusingNLS.ProfileCertificate.centralM_bounds line 32
5. theorem OAI.DefocusingNLS.ProfileCertificate.centralM_ne_zero line 40
6. theorem OAI.DefocusingNLS.ProfileCertificate.central_derivative_entries line 44

   Source documentation

   Every computed derivative entry has the required size relative to m0.

   theorem central_derivative_entries :
       (∀ v ∈ [result.derivB.a, result.derivB.b, result.derivB.c, result.derivB.d,
         result.derivZ.a, result.derivZ.b, result.derivZ.c, result.derivZ.d],
         ‖toComplex v‖ < 20*‖centralM‖) := by
   …

   Mentions: OAI.DefocusingNLS.ProfileCertificate.centralM

7. theorem OAI.DefocusingNLS.ProfileCertificate.central_error_entries line 55

   Source documentation

   Every entry of E is below the prescribed 50000 |m0| bound.

   theorem central_error_entries :
       ∀ e ∈ [result.error.a, result.error.b, result.error.c, result.error.d],
         0 ≤ (e : ℝ) ∧ (e : ℝ) < 50000*‖centralM‖ := by
   …

   Mentions: OAI.DefocusingNLS.ProfileCertificate.centralM