OAI/Geometry/Convex/GeneralMahler/Intervals/Chord.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Interpolation/range certificate through second derivatives.

  1. def OAI.GeneralMahler.Jet.mix line 9
  2. lemma OAI.GeneralMahler.Jet.convex_err_upper line 11
  3. lemma OAI.GeneralMahler.Jet.chord_error line 40
  4. lemma OAI.GeneralMahler.Jet.mix_exists line 49
  5. def OAI.GeneralMahler.Cert.IV.limK line 61

    Source comment

    largest norm limit as point
    def limK : IV→IV
  | unk=>unk
  | box a b=>let c:=max (-a) (max 0 b); box c c

    Mentions: OAI.GeneralMahler.Cert.IV, OAI.GeneralMahler.Cert.IV.c

  6. def OAI.GeneralMahler.Cert.IV.Radius line 64
  7. def OAI.GeneralMahler.Cert.IV.bcChord line 65
  8. lemma OAI.GeneralMahler.Cert.IV.box_mix line 69
  9. lemma OAI.GeneralMahler.Cert.IV.lk_pos line 79
  10. lemma OAI.GeneralMahler.Cert.IV.lk_e line 81
  11. lemma OAI.GeneralMahler.Cert.IV.mcChord line 89