OAI/Combinatorics/Progressions/FixedDensity/PolynomialApproximation.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.finitePairing line 13
  2. theorem OAI.Erdos3.FixedDensity.finitePairing_add_left line 17
  3. theorem OAI.Erdos3.FixedDensity.finitePairing_add_right line 28
  4. theorem OAI.Erdos3.FixedDensity.finitePairing_sub_left line 39
  5. theorem OAI.Erdos3.FixedDensity.finitePairing_sub_right line 50
  6. theorem OAI.Erdos3.FixedDensity.finitePairing_smul_left line 61
  7. theorem OAI.Erdos3.FixedDensity.finitePairing_smul_right line 71
  8. theorem OAI.Erdos3.FixedDensity.finitePairing_comm line 81
  9. theorem OAI.Erdos3.FixedDensity.finitePairing_mono_left line 89
  10. theorem OAI.Erdos3.FixedDensity.finitePairing_mono_right line 96
  11. def OAI.Erdos3.FixedDensity.IsUnitBounded line 103
  12. theorem OAI.Erdos3.FixedDensity.IsUnitBounded.nonneg line 106
  13. theorem OAI.Erdos3.FixedDensity.IsUnitBounded.le_one line 111
  14. theorem OAI.Erdos3.FixedDensity.isUnitBounded_zero line 116
  15. theorem OAI.Erdos3.FixedDensity.isUnitBounded_one line 120
  16. def OAI.Erdos3.FixedDensity.unitCubeSet line 124
  17. theorem OAI.Erdos3.FixedDensity.unitCubeSet_eq_Icc line 127
  18. theorem OAI.Erdos3.FixedDensity.unitCubeSet_convex line 133
  19. theorem OAI.Erdos3.FixedDensity.unitCubeSet_compact line 138
  20. theorem OAI.Erdos3.FixedDensity.unitCubeSet_closed line 143
  21. theorem OAI.Erdos3.FixedDensity.unitCubeSet_nonempty line 148
  22. def OAI.Erdos3.FixedDensity.finitePairingLinearMap line 152
  23. def OAI.Erdos3.FixedDensity.finitePairingCLM line 160
  24. theorem OAI.Erdos3.FixedDensity.finitePairingCLM_apply line 166
  25. def OAI.Erdos3.FixedDensity.finiteTestProfile line 171
  26. theorem OAI.Erdos3.FixedDensity.finiteTestProfile_apply line 178
  27. def OAI.Erdos3.FixedDensity.profileErrorSet line 184
  28. theorem OAI.Erdos3.FixedDensity.mem_profileErrorSet_iff line 187
  29. theorem OAI.Erdos3.FixedDensity.profileErrorSet_convex line 198
  30. theorem OAI.Erdos3.FixedDensity.profileErrorSet_compact line 202
  31. theorem OAI.Erdos3.FixedDensity.profileErrorSet_closed line 207
  32. theorem OAI.Erdos3.FixedDensity.profileErrorSet_nonempty line 211
  33. def OAI.Erdos3.FixedDensity.denseModelProfileSet line 219
  34. theorem OAI.Erdos3.FixedDensity.denseModelProfileSet_convex line 224
  35. theorem OAI.Erdos3.FixedDensity.denseModelProfileSet_compact line 236
  36. theorem OAI.Erdos3.FixedDensity.denseModelProfileSet_closed line 248
  37. theorem OAI.Erdos3.FixedDensity.denseModelProfileSet_nonempty line 254
  38. def OAI.Erdos3.FixedDensity.HasFiniteDenseModel line 267
  39. theorem OAI.Erdos3.FixedDensity.hasFiniteDenseModel_iff_profile_mem line 273
  40. theorem OAI.Erdos3.FixedDensity.exists_finiteDenseModel_separator line 309
  41. def OAI.Erdos3.FixedDensity.dualCoefficient line 349
  42. theorem OAI.Erdos3.FixedDensity.dual_apply_eq_sum_coefficient line 355
  43. def OAI.Erdos3.FixedDensity.coefficientL1 line 375
  44. theorem OAI.Erdos3.FixedDensity.coefficientL1_nonneg line 379
  45. theorem OAI.Erdos3.FixedDensity.coefficientL1_eq_zero_iff line 384
  46. theorem OAI.Erdos3.FixedDensity.coefficientL1_smul line 400
  47. theorem OAI.Erdos3.FixedDensity.coefficientL1_dualCoefficient_pos line 406
  48. def OAI.Erdos3.FixedDensity.finiteTestCombination line 424
  49. theorem OAI.Erdos3.FixedDensity.finiteTestCombination_zero line 430
  50. theorem OAI.Erdos3.FixedDensity.finiteTestCombination_smul_coeff line 437
  51. theorem OAI.Erdos3.FixedDensity.finitePairing_finiteTestCombination line 446
  52. theorem OAI.Erdos3.FixedDensity.dual_profile_eq_pairing_combination line 469
  53. def OAI.Erdos3.FixedDensity.dualErrorVector line 482
  54. theorem OAI.Erdos3.FixedDensity.dualErrorVector_mem line 488
  55. theorem OAI.Erdos3.FixedDensity.dual_apply_dualErrorVector line 502
  56. def OAI.Erdos3.FixedDensity.positivePart line 519
  57. theorem OAI.Erdos3.FixedDensity.positivePart_apply line 523
  58. theorem OAI.Erdos3.FixedDensity.positivePart_nonneg line 528
  59. theorem OAI.Erdos3.FixedDensity.le_positivePart line 533
  60. theorem OAI.Erdos3.FixedDensity.positivePart_of_nonneg line 539
  61. theorem OAI.Erdos3.FixedDensity.positivePart_of_nonpos line 546
  62. theorem OAI.Erdos3.FixedDensity.positivePart_zero line 553
  63. theorem OAI.Erdos3.FixedDensity.positivePart_smul_of_nonneg line 558
  64. def OAI.Erdos3.FixedDensity.positiveSupportIndicator line 565
  65. theorem OAI.Erdos3.FixedDensity.positiveSupportIndicator_unitBounded line 569
  66. theorem OAI.Erdos3.FixedDensity.positiveSupportIndicator_mul line 577
  67. theorem OAI.Erdos3.FixedDensity.finitePairing_positiveSupportIndicator line 586
  68. theorem OAI.Erdos3.FixedDensity.finitePairing_le_mean_positivePart line 594
  69. theorem OAI.Erdos3.FixedDensity.finitePairing_le_majorant_positivePart line 607
  70. theorem OAI.Erdos3.FixedDensity.finitePairing_one_left line 622
  71. theorem OAI.Erdos3.FixedDensity.majorant_positivePart_correlation_of_separates_unitCube line 627
  72. def OAI.Erdos3.FixedDensity.HasPositivePartCorrelationBound line 645
  73. def OAI.Erdos3.FixedDensity.HasNormalizedPositivePartCorrelationBound line 653
  74. theorem OAI.Erdos3.FixedDensity.hasPositivePartCorrelationBound_of_normalized line 660
  75. theorem OAI.Erdos3.FixedDensity.hasFiniteDenseModel_of_positivePartCorrelationBound line 695
  76. def OAI.Erdos3.FixedDensity.testMonomial line 734
  77. theorem OAI.Erdos3.FixedDensity.testMonomial_apply line 740
  78. def OAI.Erdos3.FixedDensity.polynomialCoefficientL1 line 746
  79. theorem OAI.Erdos3.FixedDensity.polynomialCoefficientL1_nonneg line 749
  80. theorem OAI.Erdos3.FixedDensity.finiteTestCombination_apply line 754
  81. theorem OAI.Erdos3.FixedDensity.finitePairing_finset_sum_right line 761
  82. theorem OAI.Erdos3.FixedDensity.finitePairing_fintype_sum_right line 777
  83. theorem OAI.Erdos3.FixedDensity.finiteTestCombination_pow_eq_sum_monomials line 784
  84. theorem OAI.Erdos3.FixedDensity.polynomial_eval_finiteTestCombination line 798
  85. theorem OAI.Erdos3.FixedDensity.finitePairing_polynomial_eval_finiteTestCombination line 819
  86. theorem OAI.Erdos3.FixedDensity.sum_abs_coefficientMonomial line 852
  87. def OAI.Erdos3.FixedDensity.HasMonomialCorrelationBound line 864
  88. theorem OAI.Erdos3.FixedDensity.abs_finitePairing_polynomial_eval_le line 871
  89. def OAI.Erdos3.FixedDensity.IsUnitBoundedTestFamily line 925
  90. theorem OAI.Erdos3.FixedDensity.abs_finiteTestCombination_le_coefficientL1 line 929
  91. theorem OAI.Erdos3.FixedDensity.finiteTestCombination_mem_unitInterval line 953
  92. def OAI.Erdos3.FixedDensity.ApproximatesPositivePartOnUnitInterval line 964
  93. theorem OAI.Erdos3.FixedDensity.exists_polynomial_approximating_positivePart line 969
  94. theorem OAI.Erdos3.FixedDensity.polynomial_eval_approximates_positivePart_combination line 982
  95. theorem OAI.Erdos3.FixedDensity.abs_finitePairing_le_mul_mean_abs line 994
  96. def OAI.Erdos3.FixedDensity.centeredAbsoluteMean line 1013
  97. theorem OAI.Erdos3.FixedDensity.centeredAbsoluteMean_nonneg line 1017
  98. theorem OAI.Erdos3.FixedDensity.centeredAbsoluteMean_le_mean_add_one line 1022
  99. theorem OAI.Erdos3.FixedDensity.hasNormalizedPositivePartCorrelationBound_of_polynomial line 1039
  100. theorem OAI.Erdos3.FixedDensity.hasPositivePartCorrelationBound_of_polynomial line 1108