OAI/Combinatorics/Progressions/Linear/JointFrameCoefficientCoverSample.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.VectorPolynomial.substitute_translate_joint_frameline 12 - theorem
OAI.Erdos3.VectorPolynomial.affineSampleCoefficientArray_joint_frameline 28 - theorem
OAI.Erdos3.VectorPolynomial.affineSampleCoefficientTorus_joint_frameline 41 - theorem
OAI.Erdos3.VectorPolynomial.jointSelectedPhysicalDensity_functionline 62 - theorem
OAI.Erdos3.VectorPolynomial.jointSelectedPhysicalDensity_eq_allocatedline 72 - theorem
OAI.Erdos3.VectorPolynomial.affineCoefficientCoverSample_joint_frameline 100