OAI/Combinatorics/Progressions/Estimates/CubicOriginalDiagonalComparison.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_original_root_equivalence line 13
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_last_slot_translation_equivalence line 72
  3. theorem OAI.Erdos3.exists_cubic_unshifted_exchange line 104
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_permuted_seven_expansion line 207
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_seven_exchange_expansion line 287
  6. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedDiagonalCorrection line 345
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedDiagonalCorrection_norm line 353
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedDiagonalCorrection_mean_error line 374
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_permuted_diagonal_expansion line 433
  10. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalCubeCorrection line 495
  11. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalCubeCorrection_norm line 503
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalCubeCorrection_mean_error line 522
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_diagonal_cube_expansion line 583
  14. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRootSevenCorrection line 642
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRootSevenCorrection_norm line 646
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRootSevenCorrection_mean_error line 664
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubicRootSevenCorrection_expansion line 692
  18. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRootCyclicCorrection line 738
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRootCyclicCorrection_mean_error line 742
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubicRootCyclicCorrection_expansion line 761
  21. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalDiagonalCorrection line 809
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalDiagonalCorrection_pointwise_error line 817
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicOriginalDiagonalCorrection_mean_error line 862
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubicOriginalDiagonalCorrection_expansion line 887