OAI/Combinatorics/Progressions/Linear/PreparedSpatialKernelBlocks.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.modularRank_exceptional_numeric line 11
  2. theorem OAI.Erdos3.finiteProbability_rank_markov line 47
  3. theorem OAI.Erdos3.modularRank_exceptional_probability line 66
  4. def OAI.Erdos3.modularRankSmallBallExponent line 98
  5. theorem OAI.Erdos3.modularRankSmallBallExponent_pos line 100
  6. theorem OAI.Erdos3.modularRankSmallBallExponent_eq line 103
  7. theorem OAI.Erdos3.modularRank_exceptional_probability_of_parameters line 111
  8. def OAI.Erdos3.modularInitialRankStrength line 134
  9. def OAI.Erdos3.modularInitialBlockCount line 137
  10. theorem OAI.Erdos3.modularInitialRankStrength_exponent line 140
  11. theorem OAI.Erdos3.modularInitialBlockCount_threshold line 150
  12. theorem OAI.Erdos3.modularInitialBlockCount_linear_bound line 166
  13. theorem OAI.Erdos3.modularRank_tag_cost_le line 180
  14. theorem OAI.Erdos3.modularInitialBlockCount_two_dimensions line 206
  15. def OAI.Erdos3.VectorPolynomial.preparedSpatialKernelBlocks line 218
  16. theorem OAI.Erdos3.VectorPolynomial.preparedSpatialKernelBlocks_outside_selection line 235