OAI/Combinatorics/Progressions/Estimates/CommonNativeSquareFactors.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.norm_finiteCorrelation_one line 14
  2. theorem OAI.Erdos3.finiteCorrelation_one_derivative line 20
  3. theorem OAI.Erdos3.exists_many_biased_box_shifts line 26
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_correlating_vertical_mode_preserving_characters line 109
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_correlating_vertical_mode line 141
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_detection_vertical_mode line 175
  7. def OAI.Erdos3.TranslatedStepDropSpec line 219
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.stepOne_controlled_symbol_factorization line 244
  9. theorem OAI.Erdos3.translatedStepDropSpec_one line 273
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_correlating_square_vertical_mode line 306
  11. def OAI.Erdos3.RationalFilteredNilmanifold.HasNativeBiasedSquare line 373
  12. def OAI.Erdos3.NativeBiasedSquareSpec line 415
  13. theorem OAI.Erdos3.exists_native_biased_square line 446
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasNativeBiasedSquare.mono line 533
  15. def OAI.Erdos3.NativeBiasedSquareFamilySpec line 547
  16. theorem OAI.Erdos3.exists_native_biased_square_family line 584
  17. def OAI.Erdos3.RationalFilteredNilmanifold.HasNativeBiasedSquareInModel line 642
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasNativeBiasedSquareInModel.mono line 690
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasNativeBiasedSquareInModel.forget line 704
  20. theorem OAI.Erdos3.NilpotentLieFiltration.topQuotientModel_basis_layers line 729
  21. def OAI.Erdos3.RationalFilteredNilmanifold.HasNativeFactoredSquareInModel line 758
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasNativeBiasedSquareInModel.factorization line 795
  23. theorem OAI.Erdos3.exists_adapted_uniform_two_shift_square line 831
  24. def OAI.Erdos3.RationalFilteredNilmanifold.HasFixedNativeSquareFactors line 913
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasNativeFactoredSquareInModel.exists_fixed line 944
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasFixedNativeSquareFactors.mono line 966
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_native_square_factors line 1002