OAI/Combinatorics/Progressions/Lattices/RoundedAffineLifts.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.jointIntegerFrame line 14
  2. theorem OAI.Erdos3.BooleanCubeKernel.integerAffineMap_jointIntegerFrame line 20
  3. theorem OAI.Erdos3.VectorPolynomial.AffinePolynomialLiftProperties.joint_frame line 40
  4. theorem OAI.Erdos3.VectorPolynomial.HasAffinePolynomialLifts.joint_frame line 62
  5. def OAI.Erdos3.VectorPolynomial.allocatedAffineDensity line 93
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineDensity_lifts line 97
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineDensity_nonneg line 114
  8. def OAI.Erdos3.VectorPolynomial.allocatedAffineSpatialDensity line 142
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSpatialDensity_nonneg line 149
  10. def OAI.Erdos3.VectorPolynomial.allocatedAffineSpatialPMF line 160
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSpatialPMF_toReal line 165
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSpatialPMF_support_lifts line 180
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineSpatialPMF_ae_lifts line 195
  14. def OAI.Erdos3.VectorPolynomial.HasQuarterAffinePolynomialLifts line 215
  15. theorem OAI.Erdos3.VectorPolynomial.HasQuarterAffinePolynomialLifts.to_hasAffinePolynomialLifts line 221
  16. theorem OAI.Erdos3.VectorPolynomial.HasQuarterAffinePolynomialLifts.joint_frame line 230
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineDensity_quarter_lifts line 251
  18. def OAI.Erdos3.VectorPolynomial.roundedPolynomialIntegerLift line 280
  19. def OAI.Erdos3.VectorPolynomial.roundedPolynomialSmallLift line 285
  20. theorem OAI.Erdos3.VectorPolynomial.AffinePolynomialLiftProperties.rounded_evaluation line 290
  21. theorem OAI.Erdos3.VectorPolynomial.HasQuarterAffinePolynomialLifts.rounded_joint line 313
  22. theorem OAI.Erdos3.VectorPolynomial.HasQuarterAffinePolynomialLifts.rounded_joint_residue line 329