OAI/Combinatorics/Progressions/Estimates/QuadraticPairStepDrop.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_intrinsic_step_drop line 13
  2. structure OAI.Erdos3.NativeAntisymmetricPairFactorization line 86
  3. def OAI.Erdos3.NativeAntisymmetricPairFactorization.mono line 104
  4. theorem OAI.Erdos3.exists_antisymmetric_pair_step_drop line 121
  5. structure OAI.Erdos3.NativeCubicPairFactorization line 204
  6. def OAI.Erdos3.NativeCubicPairFactorization.mono line 223
  7. theorem OAI.Erdos3.exists_cubic_pair_step_drop line 240
  8. theorem OAI.Erdos3.exists_finite_product_vertical_step_drop line 313
  9. theorem OAI.Erdos3.exists_antisymmetric_pair_orbit_factors line 393
  10. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_top_agreement line 487
  11. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_middle_top_agreement line 496
  12. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_middle_bracket_agreement line 507
  13. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_eval_factors line 534
  14. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_top_layer_invariant line 546
  15. def OAI.Erdos3.NativeSampleCorrelation.pairComparisonTests line 582
  16. theorem OAI.Erdos3.NativeSampleCorrelation.pairComparisonTests_complexity line 587
  17. theorem OAI.Erdos3.NativeSampleCorrelation.pairComparisonTests_vertical line 599
  18. def OAI.Erdos3.NativeSampleCorrelation.pairComparisonNiltest line 619
  19. theorem OAI.Erdos3.NativeSampleCorrelation.pairComparisonNiltest_complexity line 627
  20. theorem OAI.Erdos3.NativeSampleCorrelation.pairComparisonNiltest_orbit line 632
  21. theorem OAI.Erdos3.NativeSampleCorrelation.pairComparisonNiltest_observable line 642
  22. theorem OAI.Erdos3.NativeSampleCorrelation.pairComparisonNiltest_vertical line 655
  23. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pair_comparison_invariant line 683
  24. def OAI.Erdos3.NativePolynomialOrbitFactors.pairFrozenVector line 726
  25. theorem OAI.Erdos3.NativePolynomialOrbitFactors.pairFrozenVector_unit line 732
  26. def OAI.Erdos3.NativePolynomialOrbitFactors.HasPairFrozenEquivalence line 737
  27. theorem OAI.Erdos3.exists_antisymmetric_pair_frozen_equivalence line 746
  28. theorem OAI.Erdos3.exists_quadratic_pair_step_drop line 827