OAI/Combinatorics/Progressions/Estimates/LocalMomentScale.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.abs_sum_mul_sub_le line 14
  2. theorem OAI.Erdos3.LocalConvolution.correlation_swap line 29
  3. theorem OAI.Erdos3.LocalConvolution.correlation_sub_self line 37
  4. theorem OAI.Erdos3.LocalConvolution.indicator_div_card line 48
  5. theorem OAI.Erdos3.LocalConvolution.sum_uniformMass_mul_eq_one line 53
  6. theorem OAI.Erdos3.LocalConvolution.correlation_indicator_left_eq line 64
  7. theorem OAI.Erdos3.LocalConvolution.correlation_indicator_right_eq line 71
  8. theorem OAI.Erdos3.LocalConvolution.convolution_indicator_eq line 76
  9. theorem OAI.Erdos3.LocalConvolution.correlation_indicator_right_sub_one_le line 88
  10. theorem OAI.Erdos3.LocalConvolution.convolution_indicator_sub_one_le line 96
  11. theorem OAI.Erdos3.LocalConvolution.convolution_sub_left line 118
  12. def OAI.Erdos3.LocalConvolution.balancedFunction line 126
  13. theorem OAI.Erdos3.LocalConvolution.normalized_cap_ge_one line 130
  14. theorem OAI.Erdos3.LocalConvolution.centered_convolution_error line 142
  15. theorem OAI.Erdos3.LocalConvolution.centered_correlation_error_identity line 150
  16. theorem OAI.Erdos3.LocalConvolution.centered_correlation_error_le line 159
  17. theorem OAI.Erdos3.sum_uniformMass_mul_eq_expect line 206
  18. theorem OAI.Erdos3.expect_add_eq_shift_mass line 215
  19. theorem OAI.Erdos3.abs_expect_add_sub_le line 222
  20. def OAI.Erdos3.LocalConvolution.localMomentExponentFactor line 239
  21. def OAI.Erdos3.LocalConvolution.localMomentGain line 242
  22. theorem OAI.Erdos3.LocalConvolution.localMomentExponentFactor_pos line 245
  23. theorem OAI.Erdos3.LocalConvolution.localMomentGain_pos line 248
  24. theorem OAI.Erdos3.LocalConvolution.localMomentGain_le_half line 251
  25. theorem OAI.Erdos3.LocalConvolution.local_alternatives_of_boundary line 256
  26. theorem OAI.Erdos3.abs_unit_weighted_mul_le line 330
  27. theorem OAI.Erdos3.abs_expect_pair_add_sub_le line 341
  28. theorem OAI.Erdos3.expect_neg_add_eq line 380
  29. theorem OAI.Erdos3.reflected_average_sub_le line 386
  30. def OAI.Erdos3.CellRefinement.replacementIntegral line 407
  31. theorem OAI.Erdos3.CellRefinement.replacementIntegral_weighted line 410
  32. theorem OAI.Erdos3.CellRefinement.replacementIntegral_eq_cells line 422
  33. theorem OAI.Erdos3.CellRefinement.abs_replacementIntegral_sub_le line 434
  34. theorem OAI.Erdos3.CellRefinement.abs_replacementIntegral_sub_le_of_unit_weights line 458
  35. theorem OAI.Erdos3.CellRefinement.abs_slice_sub_replacement_le line 477
  36. theorem OAI.Erdos3.LocalConvolution.smoothed_correlation_le_square_mean line 505
  37. theorem OAI.Erdos3.LocalConvolution.triple_smoothed_correlation_le_square_mean line 543
  38. theorem OAI.Erdos3.LocalConvolution.exists_localMomentScale line 567