OAI/Combinatorics/Progressions/Estimates/CocycleHorizontalNormalization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.real_matrix_image_section_apply line 12
  2. theorem OAI.Erdos3.norm_matrix_mulVec_le line 23
  3. theorem OAI.Erdos3.real_image_section_norm_bound line 30
  4. theorem OAI.Erdos3.real_image_section_denominator_bound line 50
  5. theorem OAI.Erdos3.controlled_real_column_span_separation line 75
  6. theorem OAI.Erdos3.exists_common_site_denominator line 129
  7. theorem OAI.Erdos3.weighted_matrix_mulVec_bound line 187
  8. theorem OAI.Erdos3.real_image_section_weighted_bound line 213
  9. theorem OAI.Erdos3.exists_controlled_linear_splitting line 250
  10. theorem OAI.Erdos3.horizontal_parts_mem_sum line 305
  11. theorem OAI.Erdos3.horizontal_absorption_into_subspace line 317
  12. theorem OAI.Erdos3.horizontal_remove_zero line 341
  13. theorem OAI.Erdos3.horizontal_derivative_of_zero_parts line 351
  14. theorem OAI.Erdos3.horizontal_parts_separation line 364
  15. theorem OAI.Erdos3.controlled_small_vector_separation line 391
  16. theorem OAI.Erdos3.cocycle_horizontal_normalization line 421