OAI/Combinatorics/Progressions/Estimates/PhysicalJetCoverCancellation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetOutputScale_one_le line 21
  2. def OAI.Erdos3.VectorPolynomial.coefficientErrorCap line 29
  3. theorem OAI.Erdos3.VectorPolynomial.coefficientErrorCap_nonneg line 34
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredFixedFactor_bound line 49
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedRestrictedCoefficientError_bound line 72
  6. def OAI.Erdos3.VectorPolynomial.coefficientTailSpatialFactor line 110
  7. theorem OAI.Erdos3.VectorPolynomial.coefficientTailSpatialFactor_bound line 116
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceCoefficientTail_bound line 142
  9. def OAI.Erdos3.VectorPolynomial.allocatedErrorKernelCap line 245
  10. def OAI.Erdos3.VectorPolynomial.allocatedErrorKernelLip line 251
  11. def OAI.Erdos3.VectorPolynomial.allocatedErrorTorusKernel line 268
  12. def OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorMajorant line 271
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedErrorTorusKernel_bounds line 275
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientErrorMajorant_continuous line 290
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientError_le_majorant line 300
  16. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckPeriodCap_exp_bound line 367
  17. theorem OAI.Erdos3.VectorPolynomial.coefficientLatticeBasis_card_le line 389
  18. theorem OAI.Erdos3.VectorPolynomial.jetAmbientIndex_card_le line 400
  19. def OAI.Erdos3.VectorPolynomial.allocatedErrorKernelLog line 424
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedErrorKernelLog_nonneg line 427
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedErrorKernel_exp_bounds line 440
  22. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoveredSample_cover line 537
  23. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeEuclideanSample_cover line 548
  24. theorem OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus_nsmul line 563
  25. theorem OAI.Erdos3.BooleanCubeKernel.coveredJetAmbientTorus_sample line 579
  26. theorem OAI.Erdos3.BooleanCubeKernel.allocatedCoefficientErrorMajorant_sample line 588