OAI/Combinatorics/Progressions/Nilpotent/NiltestScalarTransfer.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_niltest_affine_reference_comparison line 24
  2. theorem OAI.Erdos3.exists_niltest_mesh_reference_bounds line 122
  3. theorem OAI.Erdos3.exists_niltest_mesh_scalar_transfer line 213
  4. theorem OAI.Erdos3.exists_niltest_geometric_scalar_transfer line 332
  5. theorem OAI.Erdos3.exists_niltest_initial_scalar_transfer line 507
  6. theorem OAI.Erdos3.exists_niltest_threshold_scalar_transfer line 675
  7. theorem OAI.Erdos3.exists_niltest_polynomial_window_transfer line 784
  8. theorem OAI.Erdos3.exists_niltest_polynomial_box_transfer line 886
  9. theorem OAI.Erdos3.exists_niltest_window_scalar_transfer line 1006
  10. theorem OAI.Erdos3.exists_niltest_box_scalar_transfer line 1091
  11. theorem OAI.Erdos3.exists_niltest_scalar_transfer line 1192