OAI/Geometry/Convex/GeneralMahler/Segment/Disp.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

§08 Short-width budgets. Endpoint deviations.

  1. lemma OAI.GeneralMahler.SCal.SE.cLC line 12
  2. lemma OAI.GeneralMahler.SCal.SE.mean_cs line 14
  3. lemma OAI.GeneralMahler.SCal.SE.norm_cs line 25
  4. lemma OAI.GeneralMahler.SCal.SE.vge line 35
  5. lemma OAI.GeneralMahler.SCal.SE.bav_ex line 40

    Source comment

    Helpers optional zero test pair f+g²
    lemma bav_ex (m h:ℝ)(hf:TestF f):
    bav f (seg m h)=normE m h (fun x=>liftF f (loc m h x)):=bav_norm m h f hf.cont

    Mentions: OAI.GeneralMahler.TestF, OAI.GeneralMahler.bav, OAI.GeneralMahler.SCal.SE.seg, OAI.GeneralMahler.SCal.SE.normE, OAI.GeneralMahler.SCal.liftF, OAI.GeneralMahler.SCal.SE.loc, OAI.GeneralMahler.SCal.SE.bav_norm

  6. def OAI.GeneralMahler.SCal.SE.errorF line 42
  7. lemma OAI.GeneralMahler.SCal.SE.cEF line 43
  8. lemma OAI.GeneralMahler.SCal.SE.b_repr line 45
  9. lemma OAI.GeneralMahler.SCal.SE.efbound line 59
  10. lemma OAI.GeneralMahler.SCal.SE.cirLip line 93
  11. lemma OAI.GeneralMahler.SCal.SE.pa_short line 105
  12. lemma OAI.GeneralMahler.SCal.SE.qLip line 109
  13. lemma OAI.GeneralMahler.SCal.SE.ba_short line 119