OAI/Combinatorics/Progressions/Estimates/FixedPartnerPower.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_large_fixed_choices line 11
  2. def OAI.Erdos3.functionCorrelationLinearMap line 51
  3. def OAI.Erdos3.functionCorrelationSeminorm line 58
  4. theorem OAI.Erdos3.functionCorrelationSeminorm_apply line 61
  5. theorem OAI.Erdos3.functionCorrelationSeminorm_le line 64
  6. def OAI.Erdos3.weightedModelError line 84
  7. theorem OAI.Erdos3.weightedModelError_nonneg line 88
  8. theorem OAI.Erdos3.weightedModelError_mean_le line 94
  9. theorem OAI.Erdos3.exists_large_good_error_set line 102
  10. theorem OAI.Erdos3.exists_large_fixed_dependent_choices line 145
  11. def OAI.Erdos3.shiftTestSeminormAt line 188
  12. def OAI.Erdos3.shiftTestingSeminorm line 192
  13. theorem OAI.Erdos3.shiftTestSeminormAt_bddAbove line 200
  14. theorem OAI.Erdos3.shiftTestSeminormAt_apply line 213
  15. theorem OAI.Erdos3.shiftTestingSeminorm_apply line 220
  16. theorem OAI.Erdos3.shiftTestingSeminorm_le line 227
  17. theorem OAI.Erdos3.exists_nearly_maximizing_shift_tests line 242
  18. theorem OAI.Erdos3.shiftTestingSeminorm_le_of_nonneg line 269
  19. def OAI.Erdos3.translatedTestFamily line 297
  20. theorem OAI.Erdos3.translatedTestFamily_norm_le_one line 299
  21. theorem OAI.Erdos3.correlation_le_shiftTestSeminormAt line 305
  22. theorem OAI.Erdos3.first_model_error_le_shiftTest line 312
  23. theorem OAI.Erdos3.second_model_error_le_shiftTest line 322
  24. theorem OAI.Erdos3.mean_negated_shiftTest line 336
  25. theorem OAI.Erdos3.weighted_shiftTest_model_error_mean line 343
  26. theorem OAI.Erdos3.exists_model_partner line 362
  27. theorem OAI.Erdos3.exists_fixed_model_partners line 386
  28. theorem OAI.Erdos3.exists_fixed_partners_of_shift_models line 434
  29. theorem OAI.Erdos3.two_stage_model_precision_bound line 475
  30. theorem OAI.Erdos3.exp_sub_two_le_quarter_exp line 505
  31. theorem OAI.Erdos3.exists_fixed_partners_power line 511