OAI/Combinatorics/Progressions/Geometry/FullChartHomogeneousCorrection.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.FullChartDetectedMajorGradeConclusion line 28
  2. theorem OAI.Erdos3.NilpotentLieFiltration.fullChartDetectedMajorGradeConclusion_of_fullTagged line 60
  3. def OAI.Erdos3.NilpotentLieFiltration.FullChartGradeCorrectionData line 104
  4. theorem OAI.Erdos3.NilpotentLieFiltration.fullChartGradeCorrectionData_of_detected line 125
  5. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartGradeCorrectionData line 200
  6. theorem OAI.Erdos3.NilpotentLieFiltration.certifiedFullChartGradeCorrectionData_of_detected line 222
  7. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartGradeCorrectionData.to_uncertified line 269
  8. structure OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory line 294
  9. def OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory.outer line 346
  10. def OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory.initial line 351
  11. def OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory.mono_bound line 375
  12. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory.outer_mono_bound line 391
  13. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory.mono_bound_K line 395
  14. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory.invariant_outer line 398
  15. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartFiniteHistory.exists_step line 407
  16. theorem OAI.Erdos3.NilpotentLieFiltration.certifiedFullChartGradeCorrectionData_of_representative line 515
  17. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartDetectedDecomposition line 580
  18. theorem OAI.Erdos3.NilpotentLieFiltration.fullChart_grade_quotient_of_low_value line 607
  19. theorem OAI.Erdos3.NilpotentLieFiltration.certifiedFullChartDetectedDecomposition_of_vector_detection line 660
  20. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartDetectedDecomposition.to_correctionData line 720
  21. theorem OAI.Erdos3.weightedHomogeneousComponent_totalDegree_le_of_positive line 739
  22. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_idempotent line 754
  23. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_coordinate_bound line 760
  24. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_coefficients_grid line 770
  25. theorem OAI.Erdos3.VectorPolynomial.weightedHomogeneousPart_coordinate_totalDegree_le line 783
  26. theorem OAI.Erdos3.NilpotentLieFiltration.restrictedMajorCorrection_weightedHomogeneousPart line 803
  27. theorem OAI.Erdos3.NilpotentLieFiltration.restrictedMajorCorrection_fullChart_homogeneous line 811
  28. theorem OAI.Erdos3.NilpotentLieFiltration.fullChart_quotient_identity_homogeneous line 824
  29. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartDetectedDecomposition.exists_homogeneous line 866