OAI/Combinatorics/Progressions/Estimates/RealSubspaceIntersectionCorrections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realDenominatorGrid_sub line 12
  2. theorem OAI.Erdos3.realDenominatorGrid_sub_product line 23
  3. theorem OAI.Erdos3.realDenominatorGrid_linear_combination line 37
  4. theorem OAI.Erdos3.linear_lift_grid_of_coefficients line 56
  5. theorem OAI.Erdos3.rational_lift_absorption_grid line 64
  6. theorem OAI.Erdos3.norm_sub_lift_bound line 73
  7. theorem OAI.Erdos3.norm_removed_derivative_bound line 88
  8. theorem OAI.Erdos3.kernel_split_factor_le_exp line 113
  9. theorem OAI.Erdos3.exists_controlled_kernel_split line 137
  10. theorem OAI.Erdos3.horizontal_absorption_with_split line 200
  11. theorem OAI.Erdos3.exists_image_intersection_corrections line 242
  12. theorem OAI.Erdos3.exists_common_intersection_corrections line 350
  13. theorem OAI.Erdos3.exists_basis_intersection_correction line 404