OAI/Geometry/Convex/GeneralMahler/Normalize.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous normalization on two spectral boxes using scalar endpoint and gap inequalities.

  1. lemma OAI.GeneralMahler.Param.cont_ll line 16
  2. lemma OAI.GeneralMahler.Param.cont_expL line 22
  3. lemma OAI.GeneralMahler.param_fixed line 61
  4. theorem OAI.GeneralMahler.simultaneous line 82

    Source documentation

    For a field q0 supplying the original cone with a normalized pair, a positive coordinate transform and companion field exist.

    theorem simultaneous (q:ProjField m) {c k:ℝ→ℝ}
    (hck:UpdatesOK c k) :
    ∃ R≥(2:ℝ), ∃ hr : 0<R, ∃ x:Param m R,
      let q' := x.instanceQ hr q
…

    Mentions: OAI.GeneralMahler.ProjField, OAI.GeneralMahler.UpdatesOK, OAI.GeneralMahler.Param