OAI/Combinatorics/Progressions/Lattices/ResidueRefinementBudgets.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FiniteCoefficientSlice.residuePattern line 11
  2. def OAI.Erdos3.FiniteCoefficientSlice.residueLabels line 13
  3. abbrev OAI.Erdos3.FiniteCoefficientSlice.ResidueLabel line 16
  4. def OAI.Erdos3.FiniteCoefficientSlice.residueLabelMap line 18
  5. def OAI.Erdos3.FiniteCoefficientSlice.refineResidues line 21
  6. theorem OAI.Erdos3.FiniteCoefficientSlice.refineResidues_old_residue line 29
  7. def OAI.Erdos3.FiniteCoefficientSlice.refineResiduesEmbedding line 39
  8. theorem OAI.Erdos3.FiniteCoefficientSlice.refineResiduesEmbedding_value line 47
  9. theorem OAI.Erdos3.FiniteCoefficientSlice.refineResiduesEmbedding_range line 51
  10. theorem OAI.Erdos3.FiniteCoefficientSlice.residueLabels_card_le line 69
  11. theorem OAI.Erdos3.FiniteCoefficientSlice.residueLabelMap_value_mod line 73
  12. theorem OAI.Erdos3.FiniteCoefficientSlice.refineResidues_mass_pos line 81
  13. theorem OAI.Erdos3.FiniteCoefficientSlice.retained_refineResidues_mean_ge line 93
  14. def OAI.Erdos3.FiniteCubeSlice.residuePattern line 115
  15. def OAI.Erdos3.FiniteCubeSlice.residueLabels line 118
  16. abbrev OAI.Erdos3.FiniteCubeSlice.ResidueLabel line 121
  17. def OAI.Erdos3.FiniteCubeSlice.residueLabelMap line 124
  18. def OAI.Erdos3.FiniteCubeSlice.refineResidues line 128
  19. theorem OAI.Erdos3.FiniteCubeSlice.refineResidues_old_residue line 135
  20. def OAI.Erdos3.FiniteCubeSlice.refineResiduesEmbedding line 146
  21. theorem OAI.Erdos3.FiniteCubeSlice.refineResiduesEmbedding_coordinates line 154
  22. theorem OAI.Erdos3.FiniteCubeSlice.refineResiduesEmbedding_range line 159
  23. theorem OAI.Erdos3.FiniteCubeSlice.residueLabels_card_le line 178
  24. theorem OAI.Erdos3.FiniteCubeSlice.refineResidues_mass_pos line 184
  25. theorem OAI.Erdos3.FiniteCubeSlice.retained_refineResidues_mean_ge line 196
  26. theorem OAI.Erdos3.FiniteCubeSlice.residueLabels_card_le_uniform line 219
  27. theorem OAI.Erdos3.FiniteCubeSlice.residueLabels_product_card_le line 227
  28. theorem OAI.Erdos3.FiniteCoefficientSlice.residueLabels_product_card_le line 233