OAI/NumberTheory/PiExponent/Geometry/AdmissibleCurveWeights.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.AdmissibleParameters.curveDegreeWeights line 11
2. def OAI.PiExponent.AdmissibleParameters.curveJetWeights line 14
3. lemma OAI.PiExponent.AdmissibleParameters.curveDegreeWeights_zero line 17
4. lemma OAI.PiExponent.AdmissibleParameters.curveDegreeWeights_succ line 18
5. lemma OAI.PiExponent.AdmissibleParameters.curveJetWeights_zero line 20
6. lemma OAI.PiExponent.AdmissibleParameters.curveJetWeights_succ line 21
7. lemma OAI.PiExponent.AdmissibleParameters.curveDegreeWeights_pos line 24
8. lemma OAI.PiExponent.AdmissibleParameters.curveJetWeights_pos line 29
9. lemma OAI.PiExponent.AdmissibleParameters.curveDegreeWeights_cast line 34
10. lemma OAI.PiExponent.AdmissibleParameters.curveJetWeights_cast line 40
11. lemma OAI.PiExponent.AdmissibleParameters.curve_fibre_product_ratio line 46
12. lemma OAI.PiExponent.AdmissibleParameters.curve_product_ratio line 55
13. lemma OAI.PiExponent.AdmissibleParameters.curve_volume line 62
14. lemma OAI.PiExponent.AdmissibleParameters.curve_fibre_volume line 75
15. lemma OAI.PiExponent.AdmissibleParameters.curve_coordinate_ratio line 87
16. lemma OAI.PiExponent.AdmissibleParameters.curve_separated_weight_products line 95