OAI/Combinatorics/Progressions/Estimates/CoefficientRowReindex.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.enormousCoefficient_mesh_conditions line 8
  2. theorem OAI.Erdos3.enormousCoefficient_error_rate line 27
  3. def OAI.Erdos3.coefficientImageMask line 36
  4. def OAI.Erdos3.selectedCoefficientDensity line 42
  5. theorem OAI.Erdos3.selectedCoefficient_mask line 50
  6. theorem OAI.Erdos3.coefficientImage_polynomial_error line 58
  7. theorem OAI.Erdos3.coefficientImage_enormous_error line 107
  8. def OAI.Erdos3.coefficientImageMultiplier line 154
  9. theorem OAI.Erdos3.coefficientImageMask_eq_multiplier line 159
  10. theorem OAI.Erdos3.coefficientImageMultiplier_nonneg line 165
  11. theorem OAI.Erdos3.coefficientImageMultiplier_le_index line 171
  12. theorem OAI.Erdos3.integerFromCols_image_eq_of_kernel_residues line 178
  13. def OAI.Erdos3.coefficientResidueMultiplier line 191
  14. theorem OAI.Erdos3.coefficientImageMultiplier_eq_residue line 195
  15. theorem OAI.Erdos3.coefficientResidueMultiplier_bounds line 207
  16. theorem OAI.Erdos3.monomialCoefficientMatrix_residue_eq line 217
  17. structure OAI.Erdos3.CoefficientFiberControl line 228
  18. theorem OAI.Erdos3.coefficientImage_enormous_of_control line 239
  19. theorem OAI.Erdos3.coefficientImageMultiplier_eq_of_output_residue line 267
  20. theorem OAI.Erdos3.coefficientResidueMultiplier_eq_of_output_residue line 278
  21. theorem OAI.Erdos3.integerScalarLattice_le_of_dvd line 289
  22. theorem OAI.Erdos3.integerScalarLattice_nat_refinement line 297
  23. theorem OAI.Erdos3.coefficientResidueMultiplier_eq_of_periods line 301
  24. theorem OAI.Erdos3.coefficientImageMultiplier_reindex_rows line 317
  25. theorem OAI.Erdos3.coefficientResidueMultiplier_reindex_rows line 347