OAI/Combinatorics/Progressions/Estimates/CubicPairFactoredModel.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_cubic_pair_orbit_factors line 20
  2. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubic_pair_top_agreement line 114
  3. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubic_pair_middle_top_agreement line 123
  4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubic_pair_middle_bracket_agreement line 134
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubic_pair_eval_factors line 161
  6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubic_pair_top_layer_invariant line 173
  7. theorem OAI.Erdos3.NativeSampleCorrelation.cubicOriginalComponent_cost line 210
  8. def OAI.Erdos3.NativeSampleCorrelation.cubicComparisonFrequencies line 218
  9. theorem OAI.Erdos3.NativeSampleCorrelation.cubicComparisonFrequency_apply line 223
  10. theorem OAI.Erdos3.NativeSampleCorrelation.cubicComparisonFrequency_real line 235
  11. def OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonTests line 245
  12. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonTests_complexity line 250
  13. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonTests_vertical line 262
  14. def OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonNiltest line 282
  15. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonNiltest_complexity line 290
  16. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonNiltest_orbit line 295
  17. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonNiltest_observable line 305
  18. theorem OAI.Erdos3.NativeSampleCorrelation.cubicPairComparisonNiltest_vertical line 318
  19. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubic_pair_comparison_invariant line 346
  20. def OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairFrozenVector line 390
  21. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairFrozenVector_unit line 396
  22. def OAI.Erdos3.NativePolynomialOrbitFactors.HasCubicPairFrozenEquivalence line 401
  23. theorem OAI.Erdos3.exists_cubic_frozen_equivalence_budget line 410
  24. theorem OAI.Erdos3.exists_cubic_pair_frozen_equivalence line 450
  25. theorem OAI.Erdos3.exists_cubic_pair_factored_model line 520