OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateFrozenNativeFactors.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.adaptedRebase line 47
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.adaptedRebase_orbit line 51
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.adaptedRebase_value line 54
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.adaptedRebase_siteValue line 57
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.adaptedRebase_score line 60
  6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase line 73
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_productive line 86
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_chart line 89
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_localLaw line 92
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_centerLift line 95
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_candidate_orbit line 98
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_candidate_value line 101
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_candidate_score line 105
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_ambientScore line 109
  15. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_adaptedRebase line 115
  16. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_adaptedRebase line 130
  17. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusionAdaptedRebaseEquiv line 145
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_adaptedRebase_ambient line 153
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_adaptedRebase_retained line 157
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.model_commonFactors_iff line 178
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.commonFactors_model line 184
  22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.hasCommonRefilteredOrbitFactors_withKeep line 229
  23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.withKeep_commonFactors line 285
  24. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.adaptedRebase_withKeep_commonFactors line 305
  25. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.axisVariableEquiv line 363
  26. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.hasCommonRefilteredOrbitFactors_axisPolynomial line 371
  27. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.hasCommonRefilteredOrbitFactors_freezeAxes line 428
  28. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_nativeFactors line 458
  29. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.withKeep_nativeFactors line 475