OAI/Geometry/Convex/GeneralMahler/Scalar/HBox.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GeneralMahler.SCal.Qpol line 10

   Source comment

   coefficient taylor

   noncomputable def Qpol (i n:ℕ) (u:ℝ):=
   …

2. lemma OAI.GeneralMahler.SCal.Qh_est line 12
3. def OAI.GeneralMahler.SCal.cB line 59
4. lemma OAI.GeneralMahler.SCal.mcb line 60
5. def OAI.GeneralMahler.SCal.bsumH line 62
6. lemma OAI.GeneralMahler.SCal.mbsumH line 67
7. def OAI.GeneralMahler.SCal.hBox line 75

   Source comment

   hBox assumes real u in the designated range

   def hBox (U:IV) (i n:Nat):IV :=
   …

8. lemma OAI.GeneralMahler.SCal.mhBox line 78