OAI/Combinatorics/Progressions/Lattices/AllocatedLocalResidueReconstruction.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedResidueSpatialKernel line 31
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueSpatialKernel_norm_le line 43
  3. def OAI.Erdos3.VectorPolynomial.allocatedResidueSpatialWindowWeight line 81
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueSpatialWindowWeight_norm_le line 87
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedSpatialKernel_residue line 116
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedSpatialKernel_whole_residue line 128
  7. def OAI.Erdos3.VectorPolynomial.allocatedSpatialCoefficientCap line 157
  8. def OAI.Erdos3.VectorPolynomial.allocatedSpatialExpansionCoefficient line 180
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueSpatialKernel_expansion line 191
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialExpansionCoefficient_sum_le line 200
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueSpatialKernel_remesh line 268
  12. def OAI.Erdos3.VectorPolynomial.allocatedResidueWeightedProfileTerm line 398
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeProfileReferenceTerm_residue_weighted line 415
  14. def OAI.Erdos3.VectorPolynomial.allocatedWholeIdealReference line 427
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedIdealReference_residue_weighted line 436
  16. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedWholeResidueReference line 501
  17. def OAI.Erdos3.VectorPolynomial.allocatedReferenceTupleOfWhole line 525
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceTupleOfWhole_label line 531
  19. def OAI.Erdos3.VectorPolynomial.allocatedWholeResidueReconstruction line 540
  20. def OAI.Erdos3.VectorPolynomial.allocatedResidueReferenceShift line 547
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueReferenceShift_spec line 559
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueReferenceShift_normalized line 593
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueReferenceShift_spec_at line 653
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueReferenceShift_normalized_at line 687