OAI/Combinatorics/Progressions/Linear/AllocatedShortRankWitnessWidth.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedReadCoefficientChartResidues line 16
  2. def OAI.Erdos3.VectorPolynomial.allocatedChartActualResidues line 22
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedChartActualResidues_noise line 30
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedChartActualResidues_deck line 35
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedChartActualResidues_integer line 41
  6. def OAI.Erdos3.VectorPolynomial.allocatedChartResiduePrimePowerWitness line 51
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedChartResiduePrimePowerWitness_read line 60
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedChartResiduePrimePowerWitness_iff_actual line 75
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedReadCoefficientChartResidues_sampler line 91
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedChartResiduePrimePowerWitness_sampler_iff_actual line 104
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedChartResiduePrimePowerWitness_mixedArray_iff_actual line 122
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedChartResiduePrimePowerWitness_integerDeck_iff line 160
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRankReferenceLaw line 195
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRank_cell_bind_eq line 246
  15. def OAI.Erdos3.VectorPolynomial.allocatedSpatialRankSelectedWidth line 280
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRank_cell_event line 287
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRank_reference_event line 354
  18. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_rank_witness_comparison line 422
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedShortPrincipalRank_active line 534
  20. def OAI.Erdos3.VectorPolynomial.allocatedShortRankSelectedWidth line 539
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedShortRank_cell_event line 546
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedShortRank_reference_event line 613
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRankSelectedWidth_common_gap line 673
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRankSelectedWidth_budget line 688
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedShortRankSelectedWidth_common_gap line 730
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedShortRankSelectedWidth_budget line 745