OAI/Combinatorics/Progressions/Estimates/CubicAntisymmetricModel.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.cyclicBranchOffset_zmod line 11
  2. theorem OAI.Erdos3.exists_cubic_diagonal_weights line 15
  3. theorem OAI.Erdos3.exists_absorb_cubic_error line 47
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_trilinear_derivative_equivalence line 115
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedDerivative line 230
  6. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicTrilinearTriple line 236
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicTrilinearTriple_unit line 243
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubic_trilinear_sample_correlation line 249
  9. theorem OAI.Erdos3.exists_cubic_trilinear_intervals line 298
  10. theorem OAI.Erdos3.exists_cubic_fixed_trilinear_intervals line 388
  11. theorem OAI.Erdos3.exists_cubic_separated_intervals line 507
  12. theorem OAI.Erdos3.exists_cubic_common_interval line 620
  13. theorem OAI.Erdos3.exists_cubic_positive_trilinear line 732
  14. theorem OAI.Erdos3.exists_cubic_cyclic_positive_trilinear line 836
  15. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicCyclicPair line 944
  16. theorem OAI.Erdos3.exists_cubic_reflected_model line 950
  17. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicIntegerPair line 1026
  18. theorem OAI.Erdos3.exists_cubic_unwrapped_reflection line 1031
  19. theorem OAI.Erdos3.exists_cubic_anchored_reflection line 1112
  20. theorem OAI.Erdos3.exists_cubic_antisymmetric_model line 1197