OAI/Combinatorics/Progressions/Estimates/CubicDerivativeModel.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeCubicPointwisePartition line 28
  2. def OAI.Erdos3.NativeCubicPointwisePartition.mono line 48
  3. theorem OAI.Erdos3.NativeCubicPointwisePartition.sampled_error line 57
  4. theorem OAI.Erdos3.NativeCubicPointwisePartition.sampled_approximation line 72
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.select_cubic_pointwise_partition line 115
  6. theorem OAI.Erdos3.exists_cubic_pointwise_partition line 159
  7. def OAI.Erdos3.cubicDiagonalSample line 272
  8. theorem OAI.Erdos3.cubicDiagonalSample_avoids line 274
  9. theorem OAI.Erdos3.NativeCubicPointwisePartition.weighted_diagonal_error line 297
  10. theorem OAI.Erdos3.NativeCubicPointwisePartition.diagonal_approximation line 315
  11. theorem OAI.Erdos3.exists_cubic_diagonal_partition line 329
  12. theorem OAI.Erdos3.NativeCubicPointwisePartition.exists_correlating_anchor line 418
  13. theorem OAI.Erdos3.NativeCubicPointwisePartition.weighted_diagonal_error_side line 504
  14. theorem OAI.Erdos3.NativeCubicPointwisePartition.weighted_diagonal_exchange_error line 526
  15. theorem OAI.Erdos3.NativeCubicPointwisePartition.diagonal_exchange_approximation line 554
  16. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizedDerivativeRow line 587
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizedDerivativeRow_norm line 592
  18. theorem OAI.Erdos3.exists_fixed_cubic_shifted_correlation line 616
  19. theorem OAI.Erdos3.NativeCubicPointwisePartition.exists_shifted_derivative_anchor line 705
  20. theorem OAI.Erdos3.exists_cubic_diagonal_exchange line 781
  21. def OAI.Erdos3.NativePolynomialOrbitFactors.HasCubicCorrelatingAnchor line 894
  22. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasCubicCorrelatingAnchor_mono line 908
  23. theorem OAI.Erdos3.NativeCubicPairPartition.correlatingAnchor_of_cell line 919
  24. def OAI.Erdos3.NativePolynomialOrbitFactors.HasCubicVerticalCorrelatingAnchor line 993
  25. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasCubicVerticalCorrelatingAnchor_mono line 1017
  26. theorem OAI.Erdos3.exists_cubic_correlating_vertical_pair line 1029
  27. theorem OAI.Erdos3.exists_cubic_derivative_anchor line 1148
  28. theorem OAI.Erdos3.exists_cubic_derivative_model line 1225
  29. theorem OAI.Erdos3.exists_cubic_vertical_derivative_model line 1320