OAI/Combinatorics/Progressions/Estimates/UnitVerticalCyclicDifference.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_explicit_quadratic_root_equivalence line 12
  2. theorem OAI.Erdos3.norm_unit_vector_exchange_error line 67
  3. def OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticSquareTriple line 92
  4. def OAI.Erdos3.NativeMultidegreeNilcharacter.diagonalSquareCorrection line 97
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.diagonalSquareCorrection_norm line 104
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.diagonalSquareCorrection_mean_error line 122
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quadratic_diagonal_square_comparison line 176
  8. theorem OAI.Erdos3.norm_smoothed_branch_error line 252
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticSquareTriple_norm line 280
  10. def OAI.Erdos3.NativeMultidegreeNilcharacter.wrappedDiagonalCorrection line 287
  11. def OAI.Erdos3.NativeMultidegreeNilcharacter.cyclicDiagonalCorrection line 294
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.wrappedDiagonalCorrection_mean_error line 302
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cyclicDiagonalCorrection_mean_error line 346
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cyclicDiagonalCorrection_expansion line 388
  15. def OAI.Erdos3.integerSecondDifference line 482
  16. def OAI.Erdos3.cyclicSecondDifference line 485
  17. def OAI.Erdos3.smoothedSecondDifference line 489
  18. theorem OAI.Erdos3.integerSecondDifference_norm line 494
  19. theorem OAI.Erdos3.cyclicSecondDifference_branches line 500
  20. theorem OAI.Erdos3.smoothedSecondDifference_mean_error line 520
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_diagonalSquareCorrection_expansion line 561
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cyclicExchangeCorrection_expansion line 609
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cyclicExchangeCorrection_mean_error line 637
  24. theorem OAI.Erdos3.exists_smoothedSecondDifference_expansion line 661
  25. theorem OAI.Erdos3.exists_cyclicSecondDifference_approximation line 708
  26. def OAI.Erdos3.NativeMultidegreeNilcharacter.quadraticRoot line 764
  27. def OAI.Erdos3.NativeMultidegreeNilcharacter.rootExchangeCorrection line 768
  28. def OAI.Erdos3.NativeMultidegreeNilcharacter.rootCyclicCorrection line 772
  29. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.rootCyclicCorrection_mean_error line 777
  30. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_rootCyclicCorrection_expansion line 793
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_cyclic_second_difference_models line 836