OAI/Combinatorics/Progressions/Geometry/TerminalChartSlowEvaluation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.FullChartAdmissibleStageCorrection line 36
  2. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartDetectedDecomposition.exists_admissible_stage line 66
  3. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_append_admissible line 118
  4. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible line 211
  5. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_slow line 219
  6. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_rat line 230
  7. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_q line 241
  8. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_K line 252
  9. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_prefix line 262
  10. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_entry line 276
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fullChart_admissible_stage_branches line 313
  12. theorem OAI.Erdos3.NilpotentLieFiltration.FullChartAdmissibleStageCorrection.mono_budget line 348
  13. def OAI.Erdos3.NilpotentLieFiltration.fullChartStageCountConstant line 410
  14. theorem OAI.Erdos3.NilpotentLieFiltration.fullChartStageCountConstant_ge_two line 413
  15. theorem OAI.Erdos3.NilpotentLieFiltration.certified_basis_envelope line 417
  16. theorem OAI.Erdos3.NilpotentLieFiltration.vector_correction_cover_on_set line 430
  17. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_finite_stage_representatives line 457
  18. structure OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.StageBounds line 575
  19. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.StageBounds.initial line 582
  20. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.StageBounds.of_admissible_child line 593
  21. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.StageBounds.to_budget line 621
  22. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.StageBounds.to_budget_K line 641
  23. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.StageBounds.to_budget_outer line 645
  24. theorem OAI.Erdos3.NilpotentLieFiltration.exists_certified_full_chart_history_control line 673
  25. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.terminal_mem_fast line 732
  26. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.globalRestriction_terminal_mem_pointwise line 775
  27. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.nonempty_globalMarkedNativeFactors line 799
  28. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_terminal_globalMarkedNativeFactors line 837
  29. theorem OAI.Erdos3.realPolynomialMass_constant_specialization line 959
  30. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartHom_constantChart line 989
  31. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_constantChart_value line 1007
  32. theorem OAI.Erdos3.NilpotentLieFiltration.value_bound_of_terminal_chart_control line 1019