OAI/Combinatorics/Progressions/Geometry/BoxDifferenceHom.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.expect_prod_split line 13
  2. theorem OAI.Erdos3.expect_empty_tuple line 19
  3. theorem OAI.Erdos3.expect_two_dependent_fin_cons line 30
  4. theorem OAI.Erdos3.expect_pow_two_pow_le line 42
  5. theorem OAI.Erdos3.expect_double_pow_two_pow_le line 54
  6. theorem OAI.Erdos3.norm_mean_first_difference line 62
  7. def OAI.Erdos3.finiteBoxCorrelation line 80
  8. theorem OAI.Erdos3.finiteBoxCorrelation_re_eq_mean_square line 85
  9. theorem OAI.Erdos3.finiteBoxCorrelation_re_nonneg line 102
  10. theorem OAI.Erdos3.norm_weighted_expect_sq_le line 107
  11. theorem OAI.Erdos3.norm_weighted_pair_mean_pow_four_le_box line 118
  12. def OAI.Erdos3.iteratedBoxDifference line 170
  13. theorem OAI.Erdos3.iterated_box_cauchy_schwarz line 178
  14. def OAI.Erdos3.boxSlice line 223
  15. def OAI.Erdos3.boxSliceEquiv line 225
  16. theorem OAI.Erdos3.expect_boxSlice line 234
  17. def OAI.Erdos3.boxKernel line 244
  18. def OAI.Erdos3.boxAnchorFactor line 247
  19. theorem OAI.Erdos3.boxKernel_slice line 251
  20. theorem OAI.Erdos3.boxKernel_mean line 255
  21. theorem OAI.Erdos3.boxAnchorFactor_norm_le_one line 270
  22. theorem OAI.Erdos3.boxAnchorFactor_mean_square line 276
  23. def OAI.Erdos3.finiteTripleBoxCorrelation line 307
  24. theorem OAI.Erdos3.finiteTripleBoxCorrelation_re_nonneg line 311
  25. theorem OAI.Erdos3.norm_pairwise_weighted_mean_pow_eight_le_box line 318
  26. def OAI.Erdos3.additiveBoxDifference line 392
  27. theorem OAI.Erdos3.additiveBoxDifference_sum line 400
  28. theorem OAI.Erdos3.additiveBoxDifference_product line 412
  29. theorem OAI.Erdos3.exists_box_anchor_approximation line 442
  30. theorem OAI.Erdos3.exists_box_anchor_correlation line 493
  31. theorem OAI.Erdos3.additiveBoxDifference_hom line 513