OAI/Combinatorics/Progressions/Estimates/QuarticPreciseSampledExchange.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeQuarticPointwisePartition line 30
  2. def OAI.Erdos3.NativeQuarticPointwisePartition.mono line 49
  3. theorem OAI.Erdos3.NativeQuarticPointwisePartition.sampled_error line 58
  4. theorem OAI.Erdos3.NativeQuarticPointwisePartition.sampled_approximation line 72
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.select_quartic_pointwise_partition line 114
  6. theorem OAI.Erdos3.exists_quartic_pointwise_partition line 157
  7. def OAI.Erdos3.quarticDiagonalSample line 268
  8. theorem OAI.Erdos3.quarticDiagonalSample_avoids line 270
  9. theorem OAI.Erdos3.NativeQuarticPointwisePartition.weighted_diagonal_error line 294
  10. theorem OAI.Erdos3.NativeQuarticPointwisePartition.diagonal_approximation line 312
  11. theorem OAI.Erdos3.exists_quartic_diagonal_partition line 326
  12. theorem OAI.Erdos3.NativeQuarticPointwisePartition.exists_correlating_anchor line 415
  13. theorem OAI.Erdos3.NativeQuarticPointwisePartition.weighted_diagonal_error_side line 504
  14. theorem OAI.Erdos3.NativeQuarticPointwisePartition.weighted_diagonal_exchange_error line 525
  15. theorem OAI.Erdos3.NativeQuarticPointwisePartition.diagonal_exchange_approximation line 553
  16. theorem OAI.Erdos3.NativeQuarticPointwisePartition.weighted_two_variable_error line 600
  17. theorem OAI.Erdos3.NativeQuarticPointwisePartition.weighted_two_variable_exchange_error line 616
  18. theorem OAI.Erdos3.NativeQuarticPointwisePartition.two_variable_exchange_approximation line 644
  19. def OAI.Erdos3.positiveCyclicTripleBudget line 678
  20. theorem OAI.Erdos3.PositiveCyclicNiltest.mul_three line 681
  21. def OAI.Erdos3.NativePolynomialOrbitFactors.HasQuarticCorrelatingAnchor line 702
  22. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasQuarticCorrelatingAnchor_mono line 716
  23. theorem OAI.Erdos3.NativeQuarticPairPartition.correlatingAnchor_of_cell line 727
  24. theorem OAI.Erdos3.exists_quartic_sampled_exchange line 777
  25. theorem OAI.Erdos3.exists_quartic_precise_sampled_exchange line 872