OAI/Combinatorics/Progressions/Estimates/MixedPairComparison.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasLowerRankOrbitFamily.reindex line 14
  2. def OAI.Erdos3.NativeRankRelation.CommonData.CorrelatedLocalMarkedFamily line 61
  3. theorem OAI.Erdos3.NativeRankRelation.CommonData.CorrelatedAffineComparison.localMarkedFamily line 124
  4. def OAI.Erdos3.localCoveredInducedBudget line 197
  5. def OAI.Erdos3.NativeRankRelation.CommonData.CorrelatedLocalInducedFamily line 234
  6. theorem OAI.Erdos3.NativeRankRelation.CommonData.CorrelatedLocalMarkedFamily.induce line 304
  7. def OAI.Erdos3.NativeCorrelationStructure.HasLocalMarkedFamily line 371
  8. theorem OAI.Erdos3.exists_native_local_marked_family line 417
  9. theorem OAI.Erdos3.NativeRankRelation.CommonData.CorrelatedLocalInducedFamily.product line 500
  10. theorem OAI.Erdos3.exists_localCoveredInducedBudget_bound line 555
  11. def OAI.Erdos3.NativeCorrelationStructure.HasLocalInducedFamily line 578
  12. theorem OAI.Erdos3.exists_native_local_induced_family line 626
  13. theorem OAI.Erdos3.productNiltestBudget_mono line 682
  14. theorem OAI.Erdos3.exists_native_product_correlation line 687
  15. theorem OAI.Erdos3.exists_mixed_pair_orbit_factors line 759
  16. theorem OAI.Erdos3.exists_mixed_pair_outer_control line 847
  17. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixed_pair_top_agreement line 930
  18. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixed_pair_middle_top_agreement line 939
  19. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixed_pair_middle_bracket_agreement line 950
  20. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixed_pair_eval_factors line 977
  21. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixed_pair_top_layer_invariant line 989
  22. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairComparison_component_cost line 1026
  23. def OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonTests line 1034
  24. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonTests_complexity line 1040
  25. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonTests_vertical line 1052
  26. def OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonNiltest line 1072
  27. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonNiltest_complexity line 1080
  28. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonNiltest_orbit line 1085
  29. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonNiltest_observable line 1095
  30. theorem OAI.Erdos3.NativeSampleCorrelation.mixedPairComparisonNiltest_vertical line 1108
  31. theorem OAI.Erdos3.NativePolynomialOrbitFactors.mixed_pair_comparison_invariant line 1136