OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateAdaptedOptionQuotientFactors.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.realQuotientPolynomialOrbit_mark line 20
  2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_marked_quotient_orbit_lift line 32
  3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_prescribed_marked_quotient_orbit_lift line 44
  4. def OAI.Erdos3.RationalFilteredNilmanifold.quotientOrbit line 90
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientOrbit_log line 95
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientOrbit_surjective line 100
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientOrbit_eval line 111
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientOrbit_realEval line 118
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientOrbit_mark line 144
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_prescribed_marked_quotientOrbit_lift line 154
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_external_marked_quotient_restoration line 210
  12. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.lieQuotient line 306
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.lieQuotient_orbit line 324
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.lieQuotient_value line 328
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.lieQuotient_score_eq line 336
  16. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.lieQuotientProblem line 364
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.lieQuotientProblem_productive line 381
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.lieQuotientProblem_ambientScore line 384
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_lieQuotient line 392
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientMap_mem_layer line 442
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotientOrbit_polynomialCoordinates line 447
  22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_withKeep_lieQuotientProblem_common_factors line 507
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionQuotientMap_mem_layer line 586
  24. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJoint_lieQuotient_log line 644
  25. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.optionJoint_lieQuotient_polynomialCoordinates line 657
  26. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionQuotient line 737
  27. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionQuotient_productive line 741
  28. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.optionQuotient_chart line 745
  29. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_optionQuotient line 749
  30. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_withKeep_optionQuotient_common_factors line 757
  31. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedOptionQuotient line 899
  32. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_adaptedOptionQuotient line 902
  33. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_withKeep_adaptedOptionQuotient_common_factors line 909