OAI/Combinatorics/Progressions/Dynamics/AllocatedExternalCandidatePrimitivePhysicalBudget.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.candidateGeneratedPhysicalGeometryParameter line 11
  2. structure OAI.Erdos3.VectorPolynomial.GeneratedPhysicalSuccessorScalarBounds line 15
  3. theorem OAI.Erdos3.VectorPolynomial.exists_generatedPhysicalSuccessorScalarBounds line 38
  4. def OAI.Erdos3.VectorPolynomial.candidateGeneratedPhysicalBudgetExponent line 84
  5. theorem OAI.Erdos3.VectorPolynomial.candidateGeneratedPhysicalBudgetExponent_ge_two line 87
  6. theorem OAI.Erdos3.VectorPolynomial.candidateGeneratedPhysicalScalarBounds line 91
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_nativeMarkedFreezingPhysicalParameter_bound line 106
  8. def OAI.Erdos3.VectorPolynomial.candidateFreezingOuterExponent line 122
  9. theorem OAI.Erdos3.VectorPolynomial.candidateFreezingOuterExponent_ge_two line 126
  10. def OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysicalOuterParameter line 131
  11. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysicalOuterParameter_bound line 134
  12. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysicalOuterParameter_nonneg line 140
  13. def OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysicalBudgetExponent line 145
  14. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysicalBudgetExponent_ge_two line 148
  15. def OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysicalGeometryParameter line 152
  16. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysicalScalarBounds line 155
  17. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysical_freezing_budget line 163
  18. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitivePhysical_input_budget line 171