ProfileEntryBounds.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform entrywise bounds for the actual K=34 free matching product.

theorem OAI.DefocusingNLS.ProfileCertificate.derivativeB_entry line 13
theorem OAI.DefocusingNLS.ProfileCertificate.derivativeZ_entry line 17
theorem OAI.DefocusingNLS.ProfileCertificate.error_entry line 21
theorem OAI.DefocusingNLS.ProfileCertificate.profile_entry_remainder line 26
Source documentation
The entrywise complex Taylor remainder in free:profile-enclosures.
```
theorem profile_entry_remainder (b z : ℝ)
    (hb : |b| ≤ (radius : ℝ)) (hz : |z| ≤ (radius : ℝ)) (i j : Fin 2) :
    ‖profileProduct ((centerB : ℝ)+b) ((centerZ : ℝ)+z) 34 i j-
      complexMatrix result.value i j-
      (b : ℂ)*complexMatrix result.derivB i j-
      (z : ℂ)*complexMatrix result.derivZ i j‖ <
        50000*‖centralM‖*(radius : ℝ)^2 := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.profileProduct, OAI.DefocusingNLS.ProfileCertificate.centerB, OAI.DefocusingNLS.ProfileCertificate.centerZ, OAI.DefocusingNLS.ProfileCertificate.complexMatrix, OAI.DefocusingNLS.ProfileCertificate.centralM
theorem OAI.DefocusingNLS.ProfileCertificate.profile_entry_variation line 50
Source documentation
The entire matrix varies by less than chi times the central denominator.
```
theorem profile_entry_variation (b z : ℝ)
    (hb : |b| ≤ (radius : ℝ)) (hz : |z| ≤ (radius : ℝ)) (i j : Fin 2) :
    ‖profileProduct ((centerB : ℝ)+b) ((centerZ : ℝ)+z) 34 i j-
      complexMatrix result.value i j‖ < (changeBound : ℝ)*‖centralM‖ := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.profileProduct, OAI.DefocusingNLS.ProfileCertificate.centerB, OAI.DefocusingNLS.ProfileCertificate.centerZ, OAI.DefocusingNLS.ProfileCertificate.complexMatrix, OAI.DefocusingNLS.ProfileCertificate.changeBound, OAI.DefocusingNLS.ProfileCertificate.centralM
def OAI.DefocusingNLS.ProfileCertificate.normalizedProfile line 76
def OAI.DefocusingNLS.ProfileCertificate.centralNormalized line 79
theorem OAI.DefocusingNLS.ProfileCertificate.normalizedProfile_variation line 82
theorem OAI.DefocusingNLS.ProfileCertificate.centralNormalized_zero_one line 89