OAI/Combinatorics/Progressions/Lattices/CertifiedAffineNormalizedBudget.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.certifiedAffineLongSideBound line 14
  2. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement line 44
  3. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.problem line 54
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.long line 56
  5. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.conclusion line 62
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_certifiedThresholdAffineRefinement line 69
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_certifiedAffineRefinement_after_freezing line 92
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.common_keep line 149
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.nativeFactors line 215
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.nativeFactors line 238
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.withKeep_nativeFactors line 255
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.original_dense line 316
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.slice_length_gt line 325
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.nativeFactors_of_zero_restriction line 380
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.withKeep_nativeFactors_of_zero_restriction line 404
  16. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedThresholdAffineFamilyReset line 445
  17. theorem OAI.Erdos3.VectorPolynomial.affine_selection_budget_arithmetic line 585
  18. theorem OAI.Erdos3.VectorPolynomial.exists_certified_affine_normalized_budget line 598