OAI/Combinatorics/Progressions/Linear/AllocatedModularRankFullWitness.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.largestBadDepth_pullback line 11
  2. def OAI.Erdos3.VectorPolynomial.allocatedMixedActualCoefficientSample line 33
  3. def OAI.Erdos3.VectorPolynomial.allocatedMixedActualBadProduct line 40
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedActualBadProduct_eq line 48
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedActual_primePower_event line 60
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedActual_bad_product_probability line 87
  7. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocatedMixedActual_bad_product_cutoff line 112
  8. theorem OAI.Erdos3.VectorPolynomial.decide_eq_classical line 150
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedFullMixed_witness_iff line 177
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedFullMixed_primePower_event line 194
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedProductMixed_primePower_event line 236