OAI/Combinatorics/Progressions/Estimates/ComplexFiniteMeans.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.expect_fin_cons line 12
  2. theorem OAI.Erdos3.norm_expect_mul_star_sq_le line 25
  3. theorem OAI.Erdos3.expect_square_le line 34
  4. theorem OAI.Erdos3.prod_bool_tuple_succ line 39
  5. def OAI.Erdos3.orderedProductTail line 61
  6. theorem OAI.Erdos3.orderedProductTail_zero line 64
  7. theorem OAI.Erdos3.orderedProductTail_succ line 68
  8. theorem OAI.Erdos3.orderedProduct_telescope line 72
  9. def OAI.Erdos3.axisProduct line 89
  10. def OAI.Erdos3.axisSuffix line 92
  11. theorem OAI.Erdos3.axisSuffix_update line 96
  12. theorem OAI.Erdos3.axisProduct_nonneg line 107
  13. theorem OAI.Erdos3.axisSuffix_nonneg line 111
  14. theorem OAI.Erdos3.axisProduct_le_exp line 121
  15. theorem OAI.Erdos3.axisSuffix_le_exp line 129
  16. def OAI.Erdos3.realShiftCorrelation line 159
  17. def OAI.Erdos3.realBilinearAverage line 162
  18. theorem OAI.Erdos3.bilinear_shift_identity line 165
  19. theorem OAI.Erdos3.bilinear_bound_bad_shift_density line 195
  20. theorem OAI.Erdos3.exists_small_bad_shift_set line 236
  21. theorem OAI.Erdos3.expect_prod_boolean_pow_le line 269
  22. def OAI.Erdos3.cellAverage line 313
  23. theorem OAI.Erdos3.cellAverage_nonneg line 316
  24. theorem OAI.Erdos3.cellAverage_le line 320
  25. theorem OAI.Erdos3.expect_comp_le_expect_of_support line 326
  26. theorem OAI.Erdos3.expect_cellAverage_comp_le line 341
  27. theorem OAI.Erdos3.centered_product_mean_expansion line 362
  28. theorem OAI.Erdos3.centered_product_mean_abs_le line 376
  29. theorem OAI.Erdos3.absolute_centered_product_mean_le line 392
  30. theorem OAI.Erdos3.exists_common_slice_of_equal_marginals line 422
  31. theorem OAI.Erdos3.complex_ofReal_expect line 456
  32. theorem OAI.Erdos3.real_mean_le_of_complex_mean_close line 461