ProfileTaylorBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The computed K=34 majorant bounds the actual parameter-dependent product.

theorem OAI.DefocusingNLS.ProfileCertificate.prefix_remainder line 10
theorem OAI.DefocusingNLS.ProfileCertificate.profileProduct_remainder line 35
Source documentation
Parameter-uniform Taylor remainder with the precise certificate matrix E.
```
theorem profileProduct_remainder (b z : ℝ)
    (hb : |b| ≤ (radius : ℝ)) (hz : |z| ≤ (radius : ℝ)) :
    Dominates ((radius : ℝ)^2 • rationalMatrix result.error)
      (profileProduct ((centerB : ℝ)+b) ((centerZ : ℝ)+z) 34-
        linearModel (complexMatrix result.value) (complexMatrix result.derivB)
          (complexMatrix result.derivZ) b z) := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.Dominates, OAI.DefocusingNLS.ProfileCertificate.rationalMatrix, OAI.DefocusingNLS.ProfileCertificate.profileProduct, OAI.DefocusingNLS.ProfileCertificate.centerB, OAI.DefocusingNLS.ProfileCertificate.centerZ, OAI.DefocusingNLS.ProfileCertificate.linearModel, OAI.DefocusingNLS.ProfileCertificate.complexMatrix