OAI/Combinatorics/Progressions/Estimates/RawProductArrayNormalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rawProductArrayValue line 14
  2. def OAI.Erdos3.rawProductArrayJet line 20
  3. def OAI.Erdos3.scaledPrincipalCoefficient line 28
  4. def OAI.Erdos3.scaledTailCoefficient line 32
  5. def OAI.Erdos3.scaledProductArrayJet line 38
  6. def OAI.Erdos3.booleanConstantJet line 50
  7. theorem OAI.Erdos3.rawProductArrayValue_scaled line 63
  8. theorem OAI.Erdos3.scaledProductArrayJet_eq line 95