OAI/Combinatorics/Progressions/Estimates/FormalInductionTerminal.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.basisPolynomialLift line 18
  2. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_basis line 22
  3. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_coefficients line 28
  4. theorem OAI.Erdos3.VectorPolynomial.realLinearPolynomial_mem_of_basis line 37
  5. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_mem line 50
  6. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_residual line 58
  7. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_shiftedGraded line 75
  8. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_coefficientBound line 89
  9. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_coefficientGrid line 113
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.PolynomialLiftSystemMod.extend_basis line 135
  11. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisPolynomialLift_adjoint line 152
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisPolynomialLift_adjoint_residual line 161
  13. theorem OAI.Erdos3.real_bracket_mem_of_basis line 173
  14. structure OAI.Erdos3.NilpotentLieFiltration.FormalInductionState line 198
  15. def OAI.Erdos3.NilpotentLieFiltration.FormalCorrectionProperty line 249
  16. structure OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun line 256
  17. def OAI.Erdos3.NilpotentLieFiltration.FormalInductionState.enlarge line 291
  18. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionState.enlarge_P line 300
  19. structure OAI.Erdos3.NilpotentLieFiltration.FormalStageGeometry line 317
  20. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionState.bracket_source line 345
  21. def OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.start line 379
  22. def OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.extend line 397
  23. theorem OAI.Erdos3.NilpotentLieFiltration.FormalCorrectionProperty.mul line 485
  24. theorem OAI.Erdos3.NilpotentLieFiltration.FormalCorrectionProperty.list_prod line 507
  25. theorem OAI.Erdos3.NilpotentLieFiltration.exists_formal_induction_run_product_controls line 525
  26. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.terminal_lower_log line 596
  27. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.terminal_lower_bracket line 602
  28. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.terminal_remainders line 609