OAI/Combinatorics/Progressions/Estimates/QuarticPairPartitionPrecision.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_quartic_pair_outer_control line 19
  2. def OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairAnchoredVector line 101
  3. def OAI.Erdos3.NativePolynomialOrbitFactors.HasQuarticPairLocalApproximation line 105
  4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasQuarticPairLocalApproximation_mono line 114
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairFrozenVector_diagonal line 127
  6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairFrozenVector_error line 141
  7. theorem OAI.Erdos3.exists_quartic_pair_local_approximation line 187
  8. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasQuarticPairFrozenEquivalence_mono line 290
  9. def OAI.Erdos3.NativePolynomialOrbitFactors.HasQuarticPairFrozenReduction line 295
  10. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasQuarticPairFrozenReduction_mono line 298
  11. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairFrozenEquivalence_at line 303
  12. theorem OAI.Erdos3.exists_quartic_pair_frozen_reduction line 313
  13. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleTest line 395
  14. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleTest_eval line 401
  15. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleTest_unit line 406
  16. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleTest_complexity line 412
  17. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.quarticPairMiddleTest_common_vertical line 421
  18. theorem OAI.Erdos3.exists_quartic_pair_middle_model line 466
  19. theorem OAI.Erdos3.NativePolynomialOrbitFactors.quarticPairAnchoredVector_norm line 584
  20. theorem OAI.Erdos3.NativePolynomialOrbitFactors.select_quartic_pair_local_partition line 588
  21. theorem OAI.Erdos3.exists_quartic_pair_local_partition line 653
  22. structure OAI.Erdos3.NativeQuarticPairPartition line 767
  23. def OAI.Erdos3.NativeQuarticPairPartition.mono line 790
  24. theorem OAI.Erdos3.exists_quartic_pair_precise_partition line 803