OAI/Geometry/SplitTangent/LeafPolynomialGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Leaf Polynomial Growth.

  1. def OAI.SplitTangent.RationalCurveFrames.leafPolynomialKernel line 28
  2. abbrev OAI.SplitTangent.RationalCurveFrames.LeafPolynomialGerms line 45
  3. def OAI.SplitTangent.RationalCurveFrames.coefficientQuotient line 48
  4. lemma OAI.SplitTangent.RationalCurveFrames.coefficientQuotient_surjective line 57
  5. def OAI.SplitTangent.RationalCurveFrames.sectionGermMap line 63
  6. lemma OAI.SplitTangent.RationalCurveFrames.sectionGermMap_ker_le line 67
  7. theorem OAI.SplitTangent.RationalCurveFrames.leaf_polynomial_finite_and_bound line 80
  8. theorem OAI.SplitTangent.RationalCurveFrames.leaf_polynomial_growth line 110