OAI/Combinatorics/Progressions/Lattices/AllocatedCertifiedAffinePhysicalSlowBound.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.globalChart line 47
  2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.slowChart line 51
  3. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.commonDenominator line 56
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.globalChart_support line 58
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.slowChart_support line 62
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.globalChart_top line 68
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.slowChart_top line 73
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.globalChart_top_mem line 81
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.commonDenominator_pos line 93
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.commonDenominator_bound line 96
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.globalChart_top_grid line 106
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCertifiedAffineFamilyReset line 140
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCertifiedAffineGlobalTerminal line 311
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.projection_fixes_original line 452
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.slowChart_mass line 460
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.slowChart_mass_sides line 483
  17. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetCompareExponent line 520
  18. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetFactorExponent line 523
  19. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetLiftExponent line 526
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineReset_exponents_ge_two line 530
  21. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetLogBudget line 538
  22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.slowChart_physical_abs_le line 583