ProfileQuotientAlgebra.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Denominator and quotient estimates used by the free profile certificate.

theorem OAI.DefocusingNLS.ProfileCertificate.matched_denominator_lower line 12
Source documentation
The tail disk turns a finite matrix gap into a lower bound for the first component of the matched column.
```
theorem matched_denominator_lower (A : Matrix (Fin 2) (Fin 2) ℂ)
    (r s : ℂ) (ρ : ℝ) (hr : ‖r+s‖ ≤ ρ) :
    ‖A 0 1-s*A 0 0‖-ρ*‖A 0 0‖ ≤ ‖A 0 0*r+A 0 1‖ := by
…
```
theorem OAI.DefocusingNLS.ProfileCertificate.matched_denominator_ne_zero line 22

theorem OAI.DefocusingNLS.ProfileCertificate.matched_quotient_identity line 31

Source documentation

The only change from the zero-tail quotient is a determinant term.

theorem matched_quotient_identity (A : Matrix (Fin 2) (Fin 2) ℂ) (r : ℂ)
    (hb : A 0 1 ≠ 0) (hd : A 0 0*r+A 0 1 ≠ 0) :
    (A 1 0*r+A 1 1)/(A 0 0*r+A 0 1)-A 1 1/A 0 1 =
      -(r*A.det)/(A 0 1*(A 0 0*r+A 0 1)) := by
…

theorem OAI.DefocusingNLS.ProfileCertificate.matched_quotient_bound line 41

Source documentation

Quantitative version after lower bounds for both denominators are known.

theorem matched_quotient_bound (A : Matrix (Fin 2) (Fin 2) ℂ) (r : ℂ)
    (B D : ℝ) (hB : 0 < B) (hD : 0 < D)
    (hb : B ≤ ‖A 0 1‖) (hd : D ≤ ‖A 0 0*r+A 0 1‖) :
    ‖(A 1 0*r+A 1 1)/(A 0 0*r+A 0 1)-A 1 1/A 0 1‖ ≤
      ‖r‖*‖A.det‖/(B*D) := by
…