OAI/Combinatorics/Progressions/Estimates/AnchoredReflectedFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.mixedTailDifference line 14
  2. theorem OAI.Erdos3.exists_mixed_reflected_correlation line 18
  3. theorem OAI.Erdos3.exists_mixed_reflected_exp_correlation line 80
  4. theorem OAI.Erdos3.mixedTailDifference_eq_anchor line 116
  5. theorem OAI.Erdos3.mixedTailDifference_norm line 122
  6. theorem OAI.Erdos3.mixedTailDifference_map line 129
  7. def OAI.Erdos3.mixedReflectedCorner line 136
  8. theorem OAI.Erdos3.mixedReflectedCorner_norm line 144
  9. theorem OAI.Erdos3.mixedReflectedCorner_independent line 155
  10. theorem OAI.Erdos3.exists_mixed_anchor_weights line 187
  11. theorem OAI.Erdos3.exists_anchored_reflected_family line 280