OAI/Combinatorics/Progressions/Nilpotent/LocalMajorDenseSliceNiltest.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scaleComplex line 24
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scaleComplex_eval line 39
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scaleComplex_evalCyclic line 42
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scaleComplex_norm line 45
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scaleComplex_complexity line 50
  6. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.evalReal line 73
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.evalReal_integer line 76
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.norm_evalReal_le line 81
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.continuous_evalReal line 84
  10. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.expNormalize line 107
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.expNormalize_norm line 110
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.expNormalize_complexity line 123
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.expNormalize_eval line 130
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_bounded_niltest_pair_sum line 143
  15. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.phaseShift line 203
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.phaseShift_orbit line 206
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.phaseShift_normBound line 209
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.phaseShift_lipBound line 217
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.phaseShift_complexity_iff line 225
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.phaseShift_eval line 229
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.phaseShift_evalReal line 232
  22. instance OAI.Erdos3.RationalTorus.zeroAlgebraSubsingleton line 243
  23. def OAI.Erdos3.RationalTorus.trivialFiltration line 246
  24. theorem OAI.Erdos3.RationalTorus.trivialFiltration_basis_layers line 256
  25. theorem OAI.Erdos3.RationalTorus.trivial_lattice_inner_grid line 262
  26. theorem OAI.Erdos3.RationalTorus.trivial_lattice_outer_grid line 267
  27. def OAI.Erdos3.RationalTorus.trivialNilmanifold line 272
  28. theorem OAI.Erdos3.RationalTorus.trivialNilmanifold_geometry line 276
  29. theorem OAI.Erdos3.RationalTorus.trivialNilmanifold_const_one_complexity line 285
  30. def OAI.Erdos3.zeroDegreePolynomialPhaseNiltest line 307
  31. theorem OAI.Erdos3.zeroDegreePolynomialPhaseNiltest_normBound line 312
  32. theorem OAI.Erdos3.zeroDegreePolynomialPhaseNiltest_complexity line 318
  33. theorem OAI.Erdos3.zeroDegreePolynomialPhaseNiltest_evalReal line 328
  34. theorem OAI.Erdos3.exists_zeroDegreePolynomialPhaseNiltest line 336
  35. def OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedObservable line 360
  36. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedObservable_mk line 365
  37. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedObservable_norm_le_one line 371
  38. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedObservable_lipschitz line 382
  39. def OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedNiltest line 400
  40. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedNiltest_eval line 412
  41. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedNiltest_evalReal line 420
  42. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationBufferedNiltest_complexity line 428
  43. def OAI.Erdos3.OrdinaryPolynomialPhase.weight line 450
  44. theorem OAI.Erdos3.OrdinaryPolynomialPhase.weight_pos line 452
  45. theorem OAI.Erdos3.OrdinaryPolynomialPhase.weight_le line 454
  46. abbrev OAI.Erdos3.OrdinaryPolynomialPhase.nilmanifold line 461
  47. def OAI.Erdos3.OrdinaryPolynomialPhase.budget line 464
  48. theorem OAI.Erdos3.OrdinaryPolynomialPhase.two_le_budget line 469
  49. theorem OAI.Erdos3.OrdinaryPolynomialPhase.nilmanifold_geometry line 477
  50. theorem OAI.Erdos3.OrdinaryPolynomialPhase.specialize_rename line 485
  51. theorem OAI.Erdos3.OrdinaryPolynomialPhase.exists_phase_orbit line 492
  52. theorem OAI.Erdos3.OrdinaryPolynomialPhase.exists_niltest line 524
  53. theorem OAI.Erdos3.OrdinaryPolynomialPhase.exists_niltest_of_degree line 548
  54. theorem OAI.Erdos3.exists_localMajor_slice_niltest line 595
  55. theorem OAI.Erdos3.exists_localMajor_dense_slice_niltest line 672
  56. theorem OAI.Erdos3.major_phase_nine_tenths line 709
  57. theorem OAI.Erdos3.exists_localMajor_dense_slice_niltest_nine_tenths line 714
  58. theorem OAI.Erdos3.exists_localMajor_dense_slice_niltest_early line 739