OAI/Combinatorics/Progressions/Lattices/AllocatedPhysicalIntegerRankLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.selectedResidueDensityPMF_event_congr_of_density_ne_zero line 12
  2. theorem OAI.Erdos3.largestTestedBadDepth_congr_on_tested line 41
  3. theorem OAI.Erdos3.largestBadPrimeProduct_congr_on_tested line 51
  4. theorem OAI.Erdos3.selectedResidueDensityPMF_badProduct_event_congr line 60
  5. theorem OAI.Erdos3.finite_nat_sup_measurable line 89
  6. theorem OAI.Erdos3.largestTestedBadDepth_measurable line 99
  7. theorem OAI.Erdos3.largestBadPrimeProduct_measurable line 113
  8. theorem OAI.Erdos3.largestBadPrimeProduct_tail_measurableSet line 122
  9. theorem OAI.Erdos3.density_mul_badPrimeProduct_indicator_measurable line 129
  10. theorem OAI.Erdos3.VectorPolynomial.exists_coefficientDeck_integer_lift line 166
  11. theorem OAI.Erdos3.VectorPolynomial.exists_coefficientDeck_integer_event_read line 212
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCoefficient_integer_event_read line 251
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedPhysical_integer_coefficient_read line 305
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedPhysical_integer_rank_read line 348
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedPhysical_integer_rank_law line 418