OAI/Combinatorics/Progressions/Estimates/MixedPrimitiveGowers.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_mixed_sum_pair_factors line 25
  2. def OAI.Erdos3.HasPositiveMixedTargetInterval line 80
  3. theorem OAI.Erdos3.HasCommonMixedTargetInterval.positive line 92
  4. def OAI.Erdos3.HasCyclicMixedTargetCorrelation line 162
  5. theorem OAI.Erdos3.HasCyclicMixedTargetCorrelation.mono line 170
  6. theorem OAI.Erdos3.exists_mixed_interval_cutoff_weights line 177
  7. theorem OAI.Erdos3.mixedInterval_zeroExtension_average line 208
  8. theorem OAI.Erdos3.HasPositiveMixedTargetInterval.cyclic line 231
  9. theorem OAI.Erdos3.HasCyclicMixedTargetCorrelation.mixed_sum line 273
  10. theorem OAI.Erdos3.exists_retained_cyclic_sum line 323
  11. theorem OAI.Erdos3.exists_cyclic_target_pair_factors line 390
  12. theorem OAI.Erdos3.exists_retained_mixed_pair_factors line 433
  13. theorem OAI.Erdos3.exists_retained_mixed_sampled_exchange line 497
  14. theorem OAI.Erdos3.exists_retained_mixed_cyclic_comparison line 593
  15. theorem OAI.Erdos3.exists_retained_mixed_original_integration line 718
  16. def OAI.Erdos3.mixedRowCoordinateCount line 833
  17. theorem OAI.Erdos3.mixedRowIndex_card line 835
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixed_original_row_correlation_bound line 846
  19. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPrimitiveFactor line 921
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPrimitiveFactor_norm line 925
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedPrimitiveFactor_cross line 932
  22. def OAI.Erdos3.NativeMixedCorrelation.mixedPrimitiveRow line 949
  23. theorem OAI.Erdos3.NativeMixedCorrelation.mixedPrimitiveRow_eq line 955
  24. theorem OAI.Erdos3.NativeMixedCorrelation.mixedPrimitiveRow_norm line 963
  25. theorem OAI.Erdos3.exists_mixed_primitive_rows line 976
  26. def OAI.Erdos3.NativeMixedCorrelation.mixedResidualRowFactor line 1099
  27. theorem OAI.Erdos3.NativeMixedCorrelation.mixedResidualRowFactor_norm line 1103
  28. theorem OAI.Erdos3.NativeMixedCorrelation.mixedPrimitiveRow_cross_residual line 1110
  29. theorem OAI.Erdos3.NativeMixedCorrelation.exists_mixedResidualRowFactor_expansion line 1118
  30. theorem OAI.Erdos3.exists_mixed_residual_cross_rows line 1151
  31. theorem OAI.Erdos3.exists_mixed_primitive_gowers line 1220