OAI/Combinatorics/Progressions/Lattices/CertifiedAffineCutoffCost.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_weighted_common_real_grid_vector line 14
  2. theorem OAI.Erdos3.exists_weighted_common_coordinate_grid_vector line 39
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_quotient_bound line 96
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFrozenFullChart_anchor_bound line 146
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenIntegerFullChart_anchor_grid line 185
  6. theorem OAI.Erdos3.le_monomialScale_of_coordinate line 218
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_mixed_long_coeff line 248
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_frozen_coeff line 308
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_frozen_affine_range line 335
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_certified_frozen_affine_range line 387
  11. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.tagAnchor line 487
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.fixed_abs_le_box line 491
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.tagAnchor_quotient_bound line 497
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.tagAnchor_quotient_grid line 509
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_common_affine_anchor_refinement line 523
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.tag_values_sub_anchor_mem line 621
  17. theorem OAI.Erdos3.VectorPolynomial.retained_tag_le_of_product_constraint line 644
  18. def OAI.Erdos3.VectorPolynomial.certifiedAffineCenterBudget line 673
  19. theorem OAI.Erdos3.VectorPolynomial.affineCenterBudget_arithmetic line 677
  20. theorem OAI.Erdos3.VectorPolynomial.affineCenterBudget_exp line 687
  21. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement line 720
  22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_certifiedAffineRefinement line 750
  23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.actual_chart_product line 904
  24. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.actual_chart_native_conditions line 915
  25. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedAffineRefinement.actual_chart_right_grid line 930
  26. theorem OAI.Erdos3.VectorPolynomial.exists_certifiedAffineCenterBudget_power line 951
  27. theorem OAI.Erdos3.VectorPolynomial.candidateSideCutoffCost_exp_bound line 974
  28. theorem OAI.Erdos3.VectorPolynomial.candidateSideCutoffCost_canonical_affine line 989