OAI/Combinatorics/Progressions/Estimates/BiasedSynchronizedSquareFamily.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_real_reduced_fast_relative line 18
  2. theorem OAI.Erdos3.NilpotentLieFiltration.synchronized_real_reduced_fast_relative line 46
  3. def OAI.Erdos3.NilpotentLieFiltration.ReducedSquareRelativeCongruent line 79
  4. theorem OAI.Erdos3.NilpotentLieFiltration.symbolFastIn_reducedSquareRealSymbolHom line 86
  5. def OAI.Erdos3.NilpotentLieFiltration.SynchronizedReducedSquareFamilySpec line 94
  6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_synchronized_reduced_square_family line 132
  7. def OAI.Erdos3.NilpotentLieFiltration.PointwiseSynchronizedSquareFamilySpec line 191
  8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_pointwise_synchronized_square_family line 236
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasFixedNativeSquareFactors.canonical_factors line 327
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasFixedNativeSquareFactors.fullFast_top_frequency line 355
  11. def OAI.Erdos3.RationalFilteredNilmanifold.SynchronizedNativeSquareData line 390
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.SynchronizedNativeSquareData.mono line 435
  13. def OAI.Erdos3.SynchronizedNativeCommonCoefficientSpec line 469
  14. theorem OAI.Erdos3.exists_synchronized_native_common_coefficients line 508
  15. def OAI.Erdos3.SynchronizedNativeSquareFamilySpec line 614
  16. theorem OAI.Erdos3.exists_synchronized_native_square_family line 650
  17. def OAI.Erdos3.BiasedSynchronizedSquareFamilySpec line 700
  18. theorem OAI.Erdos3.exists_biased_synchronized_square_family line 767
  19. theorem OAI.Erdos3.exists_stepTwo_biased_synchronized_square_family line 860