OAI/Combinatorics/Progressions/Estimates/NativeResidualCrossInduction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.norm_fourierCoeff_le_gowers_two line 13
  2. theorem OAI.Erdos3.mean_derivative_gowers_power_le line 21
  3. theorem OAI.Erdos3.exp_le_gowers_of_mean_derivative line 28
  4. def OAI.Erdos3.NativeCrossRowDetection line 53
  5. def OAI.Erdos3.NativeCharacterCrossRowDetection line 65
  6. theorem OAI.Erdos3.exists_native_cross_row_detection_one line 78
  7. theorem OAI.Erdos3.exists_gowers_of_native_cross_family line 90
  8. theorem OAI.Erdos3.exists_characters_of_stepOne_rows line 178
  9. theorem OAI.Erdos3.exists_native_character_cross_row_step line 270
  10. theorem OAI.Erdos3.exists_native_cross_row_detection line 303
  11. theorem OAI.Erdos3.exists_native_character_cross_row_detection line 321
  12. def OAI.Erdos3.NativeResidualCrossRowDetection line 340
  13. theorem OAI.Erdos3.exists_native_residual_cross_row_detection_zero line 356
  14. theorem OAI.Erdos3.exists_gowers_of_bounded_native_residual_cross_family line 423
  15. theorem OAI.Erdos3.exists_gowers_of_native_residual_cross_family line 512
  16. theorem OAI.Erdos3.exists_native_residual_cross_row_step line 598
  17. theorem OAI.Erdos3.exists_native_residual_cross_row_detection line 641
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_gowers_of_residual_cross_rows line 649