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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform endpoint and mean estimates for larger widths.

  1. lemma OAI.GeneralMahler.SCal.SE.segR line 12
  2. lemma OAI.GeneralMahler.SCal.SE.plusR line 24
  3. lemma OAI.GeneralMahler.SCal.SE.ik_neg line 42
  4. lemma OAI.GeneralMahler.SCal.SE.avK line 48
  5. def OAI.GeneralMahler.SCal.SE.Yval line 86

    Source comment

    convex endpoint budget bound
    def Yval (x y z:ℝ):=
…
  6. lemma OAI.GeneralMahler.SCal.SE.EK_eq line 88
  7. lemma OAI.GeneralMahler.SCal.SE.Yconv line 90
  8. lemma OAI.GeneralMahler.SCal.SE.Ybound line 98