OAI/Combinatorics/Progressions/Estimates/MixedPairFrozenEquivalence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparison_component_cost line 28
  2. def OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairFrequencies line 34
  3. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairFrequency_apply line 39
  4. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairFrequency_real line 51
  5. def OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonTests line 61
  6. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonTests_complexity line 67
  7. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonTests_vertical line 79
  8. def OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonNiltest line 99
  9. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonNiltest_complexity line 107
  10. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonNiltest_orbit line 112
  11. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonNiltest_observable line 122
  12. theorem OAI.Erdos3.NativeSampleCorrelation.mixedOriginalPairComparisonNiltest_vertical line 135
  13. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixed_original_pair_comparison_invariant line 163
  14. def OAI.Erdos3.NativePolynomialOrbitFactors.mixedPairFrozenVector line 208
  15. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixedPairFrozenVector_unit line 214
  16. def OAI.Erdos3.NativePolynomialOrbitFactors.HasMixedPairFrozenEquivalence line 219
  17. theorem OAI.Erdos3.exists_mixed_frozen_equivalence_budget line 228
  18. theorem OAI.Erdos3.exists_mixed_pair_frozen_equivalence line 267