OAI/Combinatorics/Progressions/Estimates/QuarticPairComparison.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeQuarticPairFactorization line 20
  2. def OAI.Erdos3.NativeQuarticPairFactorization.mono line 39
  3. theorem OAI.Erdos3.exists_quartic_pair_step_drop line 56
  4. theorem OAI.Erdos3.exists_quartic_pair_orbit_factors line 137
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quartic_pair_top_agreement line 233
  6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quartic_pair_middle_top_agreement line 242
  7. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quartic_pair_middle_bracket_agreement line 253
  8. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quartic_pair_eval_factors line 280
  9. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quartic_pair_top_layer_invariant line 292
  10. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairComparison_component_cost line 329
  11. def OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonTests line 337
  12. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonTests_complexity line 342
  13. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonTests_vertical line 354
  14. def OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonNiltest line 374
  15. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonNiltest_complexity line 382
  16. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonNiltest_orbit line 387
  17. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonNiltest_observable line 397
  18. theorem OAI.Erdos3.NativeSampleCorrelation.quarticPairComparisonNiltest_vertical line 410
  19. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quartic_pair_comparison_invariant line 438