OAI/Combinatorics/Progressions/Estimates/FiniteCellRefinement.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.matchedCellSpace line 13
  2. def OAI.Erdos3.matchedFirstCell line 15
  3. def OAI.Erdos3.matchedSecondCell line 18
  4. theorem OAI.Erdos3.matchedCellSpace_nonempty line 22
  5. theorem OAI.Erdos3.expect_matchedFirstCell line 26
  6. theorem OAI.Erdos3.expect_matchedFirstCell_sq line 31
  7. theorem OAI.Erdos3.mean_matchedFirstCell_le line 36
  8. theorem OAI.Erdos3.mean_matchedSecondCell_le line 42
  9. theorem OAI.Erdos3.matched_cell_potential_le line 60
  10. theorem OAI.Erdos3.expect_outside_reflected_le line 86
  11. theorem OAI.Erdos3.abs_reflected_restriction_le line 103
  12. theorem OAI.Erdos3.CellRefinement.bilinearIntegral_restrict line 135
  13. theorem OAI.Erdos3.CellRefinement.bilinearIntegral_translate line 144
  14. theorem OAI.Erdos3.CellRefinement.replacementIntegral_eq_restricted_cells line 158
  15. theorem OAI.Erdos3.CellRefinement.replacementIntegral_common_shape line 167
  16. def OAI.Erdos3.CellRefinement.matchedPairAverage line 188
  17. theorem OAI.Erdos3.CellRefinement.matchedPairAverage_eq_space line 191
  18. theorem OAI.Erdos3.CellRefinement.expect_matchedPairAverage line 196
  19. theorem OAI.Erdos3.CellRefinement.matchedPairAverage_const line 209
  20. theorem OAI.Erdos3.CellRefinement.abs_matchedPairAverage_sub_le line 213
  21. theorem OAI.Erdos3.CellRefinement.abs_matchedPairAverage_shift_sub_le line 226
  22. theorem OAI.Erdos3.cellAverage_div line 261
  23. theorem OAI.Erdos3.matchedSecondCell_second_moment_ge line 265
  24. def OAI.Erdos3.CellRefinement.matchedIndependentAverage line 305
  25. theorem OAI.Erdos3.CellRefinement.matchedIndependentAverage_eq_average line 308
  26. theorem OAI.Erdos3.CellRefinement.matchedIndependentAverage_eq_cells line 316
  27. theorem OAI.Erdos3.CellRefinement.matchedIndependentAverage_eq_restricted_cells line 330
  28. theorem OAI.Erdos3.CellRefinement.expect_translated_cell line 342
  29. theorem OAI.Erdos3.CellRefinement.abs_matchedIndependentAverage_sub_le line 349
  30. theorem OAI.Erdos3.CellRefinement.matched_independent_cell_potential_le line 369
  31. def OAI.Erdos3.CellRefinement.matchedIntegral line 392
  32. theorem OAI.Erdos3.CellRefinement.matchedIntegral_sum_order line 395
  33. theorem OAI.Erdos3.CellRefinement.matchedIntegral_div_weights line 411
  34. theorem OAI.Erdos3.CellRefinement.matchedIntegral_eq_convolution line 422
  35. theorem OAI.Erdos3.CellRefinement.abs_matchedIntegral_restrict_sub_le line 439
  36. theorem OAI.Erdos3.CellRefinement.matched_flat_integral_le line 474
  37. theorem OAI.Erdos3.CellRefinement.matched_flat_integral_le_normalized line 496
  38. def OAI.Erdos3.CellRefinement.parentMatchedAverage line 529
  39. theorem OAI.Erdos3.CellRefinement.parentMatchedAverage_eq_average line 532
  40. theorem OAI.Erdos3.CellRefinement.parentMatchedAverage_eq_integrals line 538
  41. def OAI.Erdos3.CellRefinement.parentTruncatedIntegral line 555
  42. theorem OAI.Erdos3.CellRefinement.abs_parentMatchedAverage_sub_le line 561
  43. theorem OAI.Erdos3.CellRefinement.abs_parentMatchedAverage_sub_truncated_le line 584
  44. theorem OAI.Erdos3.CellRefinement.parent_integral_truncated_comparison line 601
  45. theorem OAI.Erdos3.CellRefinement.parentTruncatedIntegral_eq_convolution line 626
  46. def OAI.Erdos3.CellRefinement.centerSlice line 650
  47. theorem OAI.Erdos3.CellRefinement.centerSlice_bounds line 653
  48. theorem OAI.Erdos3.CellRefinement.centerSlice_supported line 659
  49. theorem OAI.Erdos3.CellRefinement.centerSlice_mean line 664
  50. theorem OAI.Erdos3.CellRefinement.centerSlice_normalized_cap line 668
  51. def OAI.Erdos3.CellRefinement.centerPotential line 678
  52. def OAI.Erdos3.CellRefinement.centerMatchedIntegral line 681
  53. def OAI.Erdos3.CellRefinement.centerChildIntegral line 684
  54. def OAI.Erdos3.CellRefinement.centerChildPotential line 691
  55. theorem OAI.Erdos3.CellRefinement.centerMatchedIntegral_mean line 697
  56. theorem OAI.Erdos3.CellRefinement.centerPotential_nonneg line 704
  57. theorem OAI.Erdos3.CellRefinement.centerPotential_mean_le line 711
  58. theorem OAI.Erdos3.CellRefinement.centerChildPotential_le line 719
  59. theorem OAI.Erdos3.CellRefinement.bilinearIntegral_translated_centerSlices line 740
  60. theorem OAI.Erdos3.CellRefinement.centerChildIntegral_eq_rebased line 747
  61. theorem OAI.Erdos3.CellRefinement.centerChildPotential_eq_rebased line 762
  62. def OAI.Erdos3.CellRefinement.CellBilinearBound line 781
  63. theorem OAI.Erdos3.CellRefinement.CellBilinearBound.mono line 788
  64. theorem OAI.Erdos3.CellRefinement.cellBilinearBound_of_upper line 795
  65. theorem OAI.Erdos3.CellRefinement.translated_integral_le_of_cellBilinearBound line 813
  66. theorem OAI.Erdos3.CellRefinement.centerChildIntegral_le_of_cellBilinearBound line 826
  67. theorem OAI.Erdos3.CellRefinement.finite_cell_refinement line 861
  68. theorem OAI.Erdos3.CellRefinement.refinement_coefficient_le line 894
  69. theorem OAI.Erdos3.CellRefinement.exists_refinement_depth line 913