OAI/Combinatorics/Progressions/Estimates/ModerateSliceTensorApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.jointRetainedExpansion_card_le_product line 11
  2. theorem OAI.Erdos3.independentPeriodTensor_coefficient_mass line 18
  3. theorem OAI.Erdos3.independentPeriodTensor_approximation line 30
  4. def OAI.Erdos3.finiteFamilyCap line 65
  5. theorem OAI.Erdos3.finiteFamilyCap_nonneg line 68
  6. theorem OAI.Erdos3.le_finiteFamilyCap line 71
  7. theorem OAI.Erdos3.weightedSliceTensor_approximation line 85
  8. theorem OAI.Erdos3.moderateSliceTensor_approximation line 184