OAI/Combinatorics/Progressions/Estimates/QuarticPrimitiveGowers.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_corner_exchange_expansion line 14
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_fifteen_exchange_expansion line 75
  3. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPermutedDiagonalCorrection line 117
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPermutedDiagonalCorrection_norm line 125
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPermutedDiagonalCorrection_mean_error line 146
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_permuted_diagonal_expansion line 206
  7. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootFifteenCorrection line 271
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootFifteenCorrection_norm line 275
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootFifteenCorrection_mean_error line 293
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticRootFifteenCorrection_expansion line 328
  11. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootCyclicCorrection line 374
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRootCyclicCorrection_mean_error line 378
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticRootCyclicCorrection_expansion line 398
  14. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticOriginalDiagonalCorrection line 446
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticOriginalDiagonalCorrection_pointwise_error line 454
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticOriginalDiagonalCorrection_mean_error line 499
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticOriginalDiagonalCorrection_expansion line 524
  18. theorem OAI.Erdos3.exists_quartic_sampled_exchange_model line 604
  19. theorem OAI.Erdos3.exists_quartic_cyclic_comparison_model line 692
  20. theorem OAI.Erdos3.exists_quartic_original_integration line 825
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quartic_original_row_correlation_bound line 936
  22. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPrimitiveFactor line 1012
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPrimitiveFactor_norm line 1016
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticPrimitiveFactor_cross line 1023
  25. def OAI.Erdos3.NativeMixedCorrelation.quarticPrimitiveRow line 1040
  26. theorem OAI.Erdos3.NativeMixedCorrelation.quarticPrimitiveRow_eq line 1046
  27. theorem OAI.Erdos3.NativeMixedCorrelation.quarticPrimitiveRow_norm line 1054
  28. theorem OAI.Erdos3.exists_quartic_primitive_rows line 1066
  29. def OAI.Erdos3.NativeMixedCorrelation.quarticResidualRowFactor line 1189
  30. theorem OAI.Erdos3.NativeMixedCorrelation.quarticResidualRowFactor_norm line 1193
  31. theorem OAI.Erdos3.NativeMixedCorrelation.quarticPrimitiveRow_cross_residual line 1199
  32. theorem OAI.Erdos3.NativeMixedCorrelation.exists_quarticResidualRowFactor_expansion line 1207
  33. theorem OAI.Erdos3.exists_quartic_residual_cross_rows line 1240
  34. theorem OAI.Erdos3.exists_quartic_primitive_gowers_four line 1305