OAI/Combinatorics/Progressions/Estimates/NativeBoundedVariablePatchExpansion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.productPartitionWeight line 15
  2. theorem OAI.Erdos3.productPartitionWeight_nonneg line 18
  3. theorem OAI.Erdos3.productPartitionWeight_pos_coordinate line 22
  4. theorem OAI.Erdos3.sum_productPartitionWeight line 34
  5. theorem OAI.Erdos3.productPartitionWeight_diameter line 43
  6. def OAI.Erdos3.intervalTensorWeight line 65
  7. def OAI.Erdos3.intervalTensorApprox line 69
  8. theorem OAI.Erdos3.intervalTensorWeight_nonneg line 74
  9. theorem OAI.Erdos3.intervalTensorWeight_sum line 78
  10. theorem OAI.Erdos3.intervalTensorWeight_near line 85
  11. theorem OAI.Erdos3.intervalTensorApprox_error line 94
  12. theorem OAI.Erdos3.intervalTensorApprox_coefficient_sum line 106
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_product_partition_approximation line 124
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_native_product_approximation line 180
  15. theorem OAI.Erdos3.exists_bounded_variable_patch_expansion line 254