OAI/Combinatorics/Progressions/Estimates/CubicPairPartitionPrecision.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_cubic_pair_outer_control line 18
  2. def OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairAnchoredVector line 101
  3. def OAI.Erdos3.NativePolynomialOrbitFactors.HasCubicPairLocalApproximation line 105
  4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasCubicPairLocalApproximation_mono line 114
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairFrozenVector_diagonal line 127
  6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairFrozenVector_error line 141
  7. theorem OAI.Erdos3.exists_cubic_pair_local_approximation line 187
  8. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasCubicPairFrozenEquivalence_mono line 290
  9. def OAI.Erdos3.NativePolynomialOrbitFactors.HasCubicPairFrozenReduction line 295
  10. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasCubicPairFrozenReduction_mono line 298
  11. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairFrozenEquivalence_at line 303
  12. theorem OAI.Erdos3.exists_cubic_pair_frozen_reduction line 313
  13. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleTest line 394
  14. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleTest_eval line 400
  15. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleTest_unit line 405
  16. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleTest_complexity line 411
  17. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.cubicPairMiddleTest_common_vertical line 420
  18. theorem OAI.Erdos3.exists_cubic_pair_middle_model line 465
  19. theorem OAI.Erdos3.norm_sub_positive_sum_le_weighted line 572
  20. theorem OAI.Erdos3.weighted_partition_mean_error line 585
  21. theorem OAI.Erdos3.NativePolynomialOrbitFactors.cubicPairAnchoredVector_norm line 626
  22. theorem OAI.Erdos3.NativePolynomialOrbitFactors.select_cubic_pair_local_partition line 630
  23. theorem OAI.Erdos3.exists_cubic_pair_local_partition line 695
  24. structure OAI.Erdos3.NativeCubicPairPartition line 809
  25. def OAI.Erdos3.NativeCubicPairPartition.mono line 832
  26. theorem OAI.Erdos3.exists_cubic_pair_precise_partition line 845