OAI/Combinatorics/Progressions/Estimates/QuarticPairFrozenEquivalence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparison_component_cost line 28
  2. def OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairFrequencies line 34
  3. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairFrequency_apply line 39
  4. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairFrequency_real line 51
  5. def OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonTests line 61
  6. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonTests_complexity line 66
  7. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonTests_vertical line 78
  8. def OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonNiltest line 98
  9. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonNiltest_complexity line 106
  10. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonNiltest_orbit line 111
  11. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonNiltest_observable line 121
  12. theorem OAI.Erdos3.NativeSampleCorrelation.quarticOriginalPairComparisonNiltest_vertical line 134
  13. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quartic_original_pair_comparison_invariant line 162
  14. def OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairFrozenVector line 207
  15. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairFrozenVector_unit line 213
  16. def OAI.Erdos3.NativePolynomialOrbitFactors.HasQuarticPairFrozenEquivalence line 218
  17. theorem OAI.Erdos3.exists_quartic_frozen_equivalence_budget line 227
  18. theorem OAI.Erdos3.exists_quartic_pair_frozen_equivalence line 266