OAI/Combinatorics/Progressions/Geometry/BoxCornerMean.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MissesBoxCoordinate line 11
  2. theorem OAI.Erdos3.missesBoxCoordinate_head line 14
  3. def OAI.Erdos3.boxTailPhase line 19
  4. def OAI.Erdos3.boxTailTests line 23
  5. theorem OAI.Erdos3.boxTailTests_misses line 28
  6. theorem OAI.Erdos3.boxTailTests_norm line 36
  7. def OAI.Erdos3.boxTestCorrelation line 43
  8. theorem OAI.Erdos3.boxTestCorrelation_zero line 47
  9. def OAI.Erdos3.boxPhaseMoment line 52
  10. theorem OAI.Erdos3.boxPhaseMoment_zero line 56
  11. theorem OAI.Erdos3.boxPhaseMoment_succ line 60
  12. def OAI.Erdos3.boxCorner line 76
  13. def OAI.Erdos3.boxCornerProduct line 79
  14. theorem OAI.Erdos3.conjugationPower_eq_if_mod line 82
  15. theorem OAI.Erdos3.boxCorner_cons_false line 91
  16. theorem OAI.Erdos3.boxCorner_cons_true line 96
  17. theorem OAI.Erdos3.boxCornerProduct_mul line 101
  18. theorem OAI.Erdos3.boxCornerProduct_star line 105
  19. theorem OAI.Erdos3.boxCornerProduct_succ line 109
  20. theorem OAI.Erdos3.iteratedBoxDifference_eq_cornerProduct line 119
  21. theorem OAI.Erdos3.boxPhaseMoment_eq_expect_cornerProduct line 132
  22. theorem OAI.Erdos3.boxCorner_pair line 137
  23. theorem OAI.Erdos3.boxCornerProduct_map line 142
  24. def OAI.Erdos3.boxTailAmplitude line 166
  25. theorem OAI.Erdos3.boxTailAmplitude_cross line 171
  26. theorem OAI.Erdos3.boxTestCorrelation_head line 180
  27. theorem OAI.Erdos3.boxTestCorrelation_square_le line 195
  28. def OAI.Erdos3.boxCornerAnchor line 219
  29. theorem OAI.Erdos3.boxCornerProduct_eq_mul_anchor line 225
  30. theorem OAI.Erdos3.boxCornerAnchor_norm_le_one line 235
  31. theorem OAI.Erdos3.boxCornerAnchor_map line 246
  32. theorem OAI.Erdos3.boxCornerAnchor_prod_equiv line 259
  33. theorem OAI.Erdos3.exists_box_corner_anchor_correlation line 274
  34. theorem OAI.Erdos3.exists_true_of_ne_false line 288
  35. theorem OAI.Erdos3.boxTest_cauchySchwarz line 304
  36. theorem OAI.Erdos3.boxTest_cauchySchwarz_of_pos line 342
  37. def OAI.Erdos3.assignedBoxTest line 359
  38. theorem OAI.Erdos3.assignedBoxTest_prod line 364
  39. theorem OAI.Erdos3.assignedBoxTest_norm line 373
  40. theorem OAI.Erdos3.assignedBoxTest_misses line 384
  41. theorem OAI.Erdos3.assigned_site_cauchySchwarz line 396
  42. def OAI.Erdos3.boxPairEquiv line 416
  43. theorem OAI.Erdos3.integerBox_cornerProduct_mean line 428