ProfileLinearMap.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The real-linear map certified at the free profile center.

def OAI.DefocusingNLS.ProfileCertificate.realLinearMap line 10
theorem OAI.DefocusingNLS.ProfileCertificate.realLinearMap_apply line 13

theorem OAI.DefocusingNLS.ProfileCertificate.realLinearMap_minimum_stretch line 18

Source documentation

The two strict rational Gram inequalities give the Euclidean lower bound.

theorem realLinearMap_minimum_stretch (x y : ℂ) (c : ℝ) (hc : 0 ≤ c)
    (hx : c^2 < Complex.normSq x)
    (hgram : (Complex.normSq x-c^2)*(Complex.normSq y-c^2) >
      (x.re*y.re+x.im*y.im)^2) (z : ℂ) :
    c*‖z‖ ≤ ‖realLinearMap x y z‖ := by
…

Mentions: OAI.DefocusingNLS.ProfileCertificate.realLinearMap

def OAI.DefocusingNLS.ProfileCertificate.centralX line 42
def OAI.DefocusingNLS.ProfileCertificate.centralY line 44
theorem OAI.DefocusingNLS.ProfileCertificate.central_minimum_stretch line 48
Source documentation
The concrete map has the precise lower bound needed in the degree argument.
```
theorem central_minimum_stretch (z : ℂ) :
    (48/1000 : ℝ)*‖z‖ ≤ ‖realLinearMap centralX centralY z‖ := by
…
```
Mentions: OAI.DefocusingNLS.ProfileCertificate.realLinearMap, OAI.DefocusingNLS.ProfileCertificate.centralX, OAI.DefocusingNLS.ProfileCertificate.centralY
theorem OAI.DefocusingNLS.ProfileCertificate.central_linear_orientation line 63