OAI/Combinatorics/Progressions/Nilpotent/NiltestAffineProjection.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.substitute line 20
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_substitute line 24
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.substitute_complexityLE line 31
  4. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.affinePullback line 35
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_affinePullback line 39
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.affinePullback_complexityLE line 45
  7. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.linearPullbackHom line 49
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_linearPullbackHom line 54
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.linearPullbackHom_complexityLE line 64
  10. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.translate line 83
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_translate line 89
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.translate_complexityLE line 100
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_nested_box_restriction line 118
  14. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.coordinateEquiv line 145
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_coordinateEquiv line 150
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_coordinateEquiv_symm line 157
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.coordinateEquiv_observable line 162
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.coordinateEquiv_normBound line 165
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.coordinateEquiv_lipBound line 168
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.coordinateEquiv_complexityLE line 171
  21. theorem OAI.Erdos3.exists_correlating_niltest_product_piece line 185
  22. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.symbol line 241
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.symbol_translate line 246
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.mean_translate_box line 255
  25. def OAI.Erdos3.scalarAffinePolynomial line 273
  26. theorem OAI.Erdos3.scalarAffinePolynomial_support line 276
  27. theorem OAI.Erdos3.VectorPolynomial.substitute_scalarAffinePolynomial line 286
  28. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback line 308
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_complexityLE line 312
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_log line 316
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_eval_integer line 321
  32. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_symbol line 330
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_factorization line 346
  34. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_symbol_inverse_stride line 378
  35. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffineCell_factorization_to_original line 392
  36. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.symbol_eq_of_orbit_eq line 434
  37. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.affinePullback_orbit_eq_of_orbit_eq line 444
  38. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_affine_finset_kernel_projection_family line 452