OAI/Combinatorics/Progressions/Estimates/CubicPrimitiveRows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_cubic_precise_unshifted_exchange line 20
  2. theorem OAI.Erdos3.exists_cubic_unshifted_exchange_model line 110
  3. theorem OAI.Erdos3.exists_cubic_cyclic_comparison_model line 186
  4. theorem OAI.Erdos3.exists_cubic_original_integration line 288
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicCyclicDiagonalDerivative_unit line 391
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicCyclicDiagonalDerivative_norm line 397
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubic_original_row_correlation_bound line 405
  8. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPrimitiveFactor line 494
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPrimitiveFactor_norm line 498
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPrimitiveFactor_cross line 504
  11. theorem OAI.Erdos3.exists_cubic_primitive_rows line 515