OAI/Combinatorics/Progressions/Nilpotent/CyclicNiltestApproximation.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.productExpBound line 15
  2. theorem OAI.Erdos3.coe_productExpBound line 17
  3. def OAI.Erdos3.productObservableLipBudget line 19
  4. def OAI.Erdos3.productNiltestBudget line 21
  5. theorem OAI.Erdos3.productObservableLipBudget_nonneg line 24
  6. theorem OAI.Erdos3.productNiltestBudget_geometry line 29
  7. theorem OAI.Erdos3.productNiltestBudget_observable line 35
  8. theorem OAI.Erdos3.exists_productNiltestBudget_bound line 58
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.productLayerBasis_logHeight line 81
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.pi_geometry line 99
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjection_lattice line 140
  12. def OAI.Erdos3.RationalFilteredNilmanifold.productProjectionHom line 145
  13. def OAI.Erdos3.RationalFilteredNilmanifold.productProjection line 149
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjection_mk line 153
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjection_matrix_height line 156
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjection_lipschitz line 177
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjection_lipschitz_bound line 196
  18. def OAI.Erdos3.optionLieSpace line 220
  19. instance OAI.Erdos3.optionLieRing line 224
  20. instance OAI.Erdos3.optionLieAlgebra line 228
  21. def OAI.Erdos3.optionDimension line 233
  22. def OAI.Erdos3.RationalFilteredNilmanifold.optionFactors line 248
  23. def OAI.Erdos3.RationalFilteredNilmanifold.optionProduct line 253
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionProduct_geometry line 255
  25. def OAI.Erdos3.RationalFilteredNilmanifold.optionMaps line 268
  26. def OAI.Erdos3.RationalFilteredNilmanifold.optionProductMap line 273
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionProductMap_logHeight line 277
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionProductMap_real_kernel line 292
  29. def OAI.Erdos3.RationalFilteredNilmanifold.productObservable line 324
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.productObservable_bounds line 327
  31. def OAI.Erdos3.RationalFilteredNilmanifold.piNiltest line 357
  32. theorem OAI.Erdos3.RationalFilteredNilmanifold.piNiltest_eval line 368
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.piNiltest_complexity line 380
  34. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_product_niltest line 401
  35. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjection_smul line 434
  36. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjectionHom_mem_layer line 438
  37. theorem OAI.Erdos3.RationalFilteredNilmanifold.productObservable_vertical line 454
  38. theorem OAI.Erdos3.RationalFilteredNilmanifold.piNiltest_vertical line 481
  39. theorem OAI.Erdos3.RationalFilteredNilmanifold.piNiltest_orbit_eq line 495
  40. theorem OAI.Erdos3.RationalFilteredNilmanifold.productObservable_norm_le_one line 524
  41. def OAI.Erdos3.RationalFilteredNilmanifold.unitBoundedPiNiltest line 534
  42. theorem OAI.Erdos3.RationalFilteredNilmanifold.unitBoundedPiNiltest_normBound line 541
  43. theorem OAI.Erdos3.RationalFilteredNilmanifold.unitBoundedPiNiltest_eval line 546
  44. theorem OAI.Erdos3.RationalFilteredNilmanifold.unitBoundedPiNiltest_complexity line 552
  45. theorem OAI.Erdos3.complex_prod_unit_interval line 574
  46. theorem OAI.Erdos3.RationalFilteredNilmanifold.piNiltest_unit_interval line 592
  47. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.unit_interval_eval line 614
  48. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.unit_interval_evalCyclic line 617
  49. theorem OAI.Erdos3.exists_cellwise_niltest_error line 633
  50. theorem OAI.Erdos3.exists_cyclic_cellwise_niltest_approximation line 679