OAI/Combinatorics/Progressions/Geometry/BoundedCertifiedFullChartMajorIteration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory line 15
  2. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.outer line 69
  3. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.initial line 74
  4. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.mono_bound line 99
  5. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.outer_mono_bound line 116
  6. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.mono_bound_K line 120
  7. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.invariant_outer line 123
  8. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.toUncertified line 132
  9. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.outer_toUncertified line 147
  10. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.toUncertified_K line 152
  11. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_step line 154
  12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_certified_full_chart_grade_correction_of_major_correlation line 244
  13. theorem OAI.Erdos3.NilpotentLieFiltration.exists_certified_full_chart_grade_correction_of_major_correlation_witness line 290
  14. def OAI.Erdos3.NilpotentLieFiltration.CertifiedBundledFullChartControlledCorrelationSourceStages line 323
  15. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_certified_full_chart_major_iteration line 363