OAI/Combinatorics/Progressions/Estimates/RowRestrictedDeckSiteMask.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.coefficientDeckPeriodCap line 14
  2. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckPeriodCap_nonneg line 18
  3. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetDensity_product line 24
  4. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetDensity_period_bound line 51
  5. def OAI.Erdos3.VectorPolynomial.coefficientDeckSmallPeriodDensity line 79
  6. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSmallPeriodDensity_apply line 84
  7. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSmallPeriodDensity_bounds line 99
  8. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetDensity_eq_of_period line 113
  9. def OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask line 141
  10. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask_apply line 146
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask_bounds line 163
  12. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask_expansion line 171
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask_coefficient_sum line 184
  14. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask_reconstructed line 198
  15. def OAI.Erdos3.VectorPolynomial.mixedCoveredBooleanSiteValue line 240
  16. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredBooleanSiteValue_mixed line 247
  17. def OAI.Erdos3.VectorPolynomial.coveredBooleanSiteValue line 254
  18. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredBooleanSiteValue_chart line 264
  19. def OAI.Erdos3.rowRestrictedSiteMatrix line 283
  20. theorem OAI.Erdos3.integerBooleanSitesFromRows_eq_mulVec line 286
  21. def OAI.Erdos3.VectorPolynomial.mixedCoveredRowsSiteValue line 315
  22. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredRowsSiteValue_integer line 321
  23. def OAI.Erdos3.VectorPolynomial.coveredRowsSiteValue line 330
  24. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredRowsSiteValue_chart line 341
  25. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask_of_lifts line 368
  26. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckSiteMask_ambient_lifts line 386
  27. theorem OAI.Erdos3.arrayCoordinateEquiv_integerMatrixTorusMap line 427
  28. theorem OAI.Erdos3.VectorPolynomial.coveredBooleanSiteValue_eq_siteFromLow line 449
  29. theorem OAI.Erdos3.VectorPolynomial.coveredBooleanSiteValue_coefficient line 468
  30. theorem OAI.Erdos3.rowRestrictedExtraction_mul_reconstruction line 491
  31. theorem OAI.Erdos3.rowRestrictedReconstruction_zsmul_inverse line 500
  32. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckRowsSiteMask_of_lifts line 523
  33. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckRowsSiteMask_reconstructed line 541