OAI/Analysis/PlanarPacking/BernsteinSign.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpPlanar.bernsteinWeightline 11 - def
OAI.SharpPlanar.powerToBernsteinline 13 - lemma
OAI.SharpPlanar.choose_ratio_identityline 16 - lemma
OAI.SharpPlanar.monomial_bernsteinline 26 - lemma
OAI.SharpPlanar.bernstein_identityline 44 - lemma
OAI.SharpPlanar.bernsteinWeight_nonnegline 61 - lemma
OAI.SharpPlanar.sum_bernsteinWeightline 67 - lemma
OAI.SharpPlanar.bernstein_lowerline 78