OAI/Combinatorics/Progressions/Geometry/CertifiedFullChartBudgetedTreeBounds.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.stage_branch_numeric line 39
  2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_optional_stage_branch line 54
  3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_chart_finite_stage_branches line 87
  4. def OAI.Erdos3.finiteStageTreeLogBound line 149
  5. theorem OAI.Erdos3.finiteStageTreeLogBound_nonneg line 153
  6. theorem OAI.Erdos3.finiteStageTree_stage_log_le line 159
  7. theorem OAI.Erdos3.exists_finite_stage_tree_budget line 175
  8. def OAI.Erdos3.NilpotentLieFiltration.fullChartFiniteTreeLogBound line 199
  9. def OAI.Erdos3.NilpotentLieFiltration.fullChartFiniteTreeBranching line 202
  10. theorem OAI.Erdos3.NilpotentLieFiltration.fullChartFiniteTree_branch_count_le line 205
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fullChartFiniteTree_budget line 218
  12. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.AdmissibleChild line 260
  13. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.RepresentsCorrection line 266
  14. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_is_child line 277
  15. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_finite_children line 289
  16. structure OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree line 370
  17. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_finite_branch_tree line 386
  18. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.univInitialHistory line 416
  19. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.level line 423
  20. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.vertices line 429
  21. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.fullChartTreeBranchCap line 435
  22. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.card_children_le line 442
  23. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.card_level_le line 453
  24. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.card_vertices_le line 461
  25. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.exists_representative_child line 470
  26. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.AdmissibleChildAt line 516
  27. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.append_admissible_is_child_at line 525
  28. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_finite_children_at_budget line 538
  29. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.fullChartTreeExponent line 620
  30. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.fullChartTreeExponent_ge_two line 623
  31. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.card_children_le_uniform line 630
  32. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.FiniteBranchTree.card_vertices_le_exp line 641
  33. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_bounded_finite_branch_tree line 652
  34. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_reached_child_of_major_correlation_witness line 681
  35. structure OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.BudgetedBranchTree line 766
  36. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_budgeted_branch_tree line 782
  37. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.BudgetedBranchTree.level line 814
  38. def OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.BudgetedBranchTree.vertices line 820
  39. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.BudgetedBranchTree.exists_representative_child line 828
  40. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.BudgetedBranchTree.stage_bounds line 879
  41. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.BudgetedBranchTree.exists_reached_smaller_budget line 896