OAI/Combinatorics/Progressions/Estimates/DiagonalRowTransfer.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_native_common_factor_products line 13
  2. theorem OAI.Erdos3.norm_mul_star_sub_mul_star_le_of_le_one line 64
  3. theorem OAI.Erdos3.NativePairPartition.partition_sum_norm line 96
  4. theorem OAI.Erdos3.exists_global_pair_comparison line 119
  5. theorem OAI.Erdos3.exists_precise_global_pair_comparison line 232
  6. theorem OAI.Erdos3.exists_quadratic_pair_orbit_factors line 337
  7. theorem OAI.Erdos3.exists_quadratic_global_exchange line 390
  8. theorem OAI.Erdos3.exists_quadratic_pair_projected_factors line 463
  9. theorem OAI.Erdos3.exists_quadratic_approximate_integration line 518
  10. theorem OAI.Erdos3.quadratic_original_error_bound line 608
  11. theorem OAI.Erdos3.exists_quadratic_original_integration line 665
  12. theorem OAI.Erdos3.unit_row_correlation_bound line 778
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cyclicDiagonalDerivative_unit line 831
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cyclicDiagonalDerivative_norm line 837
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.original_diagonal_row_correlation_bound line 844