OAI/Combinatorics/Progressions/Estimates/ProductTensorGroupedBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteTaggedTupleEquiv line 14
  2. theorem OAI.Erdos3.finiteTaggedTuple_sum line 20
  3. theorem OAI.Erdos3.finiteProductIntegral_tagged line 42
  4. def OAI.Erdos3.orderedFamilyTensor line 64
  5. theorem OAI.Erdos3.orderedFamilyTensor_energy line 72
  6. theorem OAI.Erdos3.productMean_sum_embeddings_le line 109
  7. theorem OAI.Erdos3.productTensor_pattern_integral line 137
  8. theorem OAI.Erdos3.productTensor_pattern_bound line 165
  9. theorem OAI.Erdos3.productTensor_grouped_bound line 199