OAI/Combinatorics/Progressions/Estimates/RelativePatchWeightDescent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_monotone_lowest_weight_prefix line 10
  2. theorem OAI.Erdos3.PolynomialPatch.castRank_weight_apply line 38
  3. theorem OAI.Erdos3.PolynomialPatch.exists_lowestLayer_prefix line 44
  4. theorem OAI.Erdos3.relativePatchDistinctWeights_tail line 74
  5. theorem OAI.Erdos3.relativePatchDistinctWeights_castRank line 105
  6. theorem OAI.Erdos3.relativePatchDistinctWeights_coordinateFiber line 111
  7. theorem OAI.Erdos3.relativePatchComplexity_coordinateFiber line 116
  8. theorem OAI.Erdos3.relativePatchDistinctWeights_tail_le line 121