OAI/Combinatorics/Progressions/Estimates/MixedPreciseSampledExchange.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeMixedPointwisePartition line 28
  2. def OAI.Erdos3.NativeMixedPointwisePartition.mono line 47
  3. theorem OAI.Erdos3.NativeMixedPointwisePartition.sampled_error line 57
  4. theorem OAI.Erdos3.NativeMixedPointwisePartition.sampled_approximation line 71
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.select_mixed_pointwise_partition line 113
  6. theorem OAI.Erdos3.exists_mixed_pointwise_partition line 156
  7. def OAI.Erdos3.mixedDiagonalSample line 273
  8. theorem OAI.Erdos3.mixedDiagonalSample_avoids line 276
  9. theorem OAI.Erdos3.NativeMixedPointwisePartition.weighted_diagonal_error line 299
  10. theorem OAI.Erdos3.NativeMixedPointwisePartition.diagonal_approximation line 317
  11. theorem OAI.Erdos3.exists_mixed_diagonal_partition line 331
  12. theorem OAI.Erdos3.NativeMixedPointwisePartition.weighted_two_variable_error line 423
  13. theorem OAI.Erdos3.NativeMixedPointwisePartition.weighted_two_variable_exchange_error line 438
  14. theorem OAI.Erdos3.NativeMixedPointwisePartition.two_variable_exchange_approximation line 466
  15. theorem OAI.Erdos3.exists_mixed_sampled_exchange line 500
  16. theorem OAI.Erdos3.exists_mixed_precise_sampled_exchange line 594