OAI/Combinatorics/Progressions/Estimates/MarginalTailModeling.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_modeling_dual_obstruction line 18
  2. theorem OAI.Erdos3.mem_closure_model_set_of_dual_detector line 70
  3. theorem OAI.Erdos3.exists_uniform_convex_approximation line 93
  4. theorem OAI.Erdos3.seminorm_sq_le_square_mean line 137
  5. def OAI.Erdos3.weightedEuclideanMap line 156
  6. theorem OAI.Erdos3.weightedEuclideanMap_norm_sq line 161
  7. theorem OAI.Erdos3.exists_weighted_convex_approximation line 170
  8. theorem OAI.Erdos3.seminorm_sq_le_weighted_square_mean line 196
  9. theorem OAI.Erdos3.norm_uniform_inner_symm line 218
  10. theorem OAI.Erdos3.mem_closure_model_of_uniform_detector line 224
  11. theorem OAI.Erdos3.exists_convex_model_of_uniform_detector line 243
  12. theorem OAI.Erdos3.exists_empirical_length line 284
  13. theorem OAI.Erdos3.scaled_empirical_seminorm_bound line 308
  14. theorem OAI.Erdos3.exists_uniform_model_of_detector line 328
  15. theorem OAI.Erdos3.mem_closure_model_of_weighted_detector line 392
  16. theorem OAI.Erdos3.exists_convex_model_of_weighted_detector line 412
  17. theorem OAI.Erdos3.scaled_weighted_empirical_seminorm_bound line 454
  18. theorem OAI.Erdos3.exists_weighted_model_of_detector line 476
  19. theorem OAI.Erdos3.exists_finite_probability_model line 528
  20. theorem OAI.Erdos3.seminorm_mask_le line 561
  21. theorem OAI.Erdos3.seminorm_mask_le_condition line 579
  22. theorem OAI.Erdos3.seminorm_tail_le line 592
  23. theorem OAI.Erdos3.seminorm_le_mask_add_tail line 610
  24. theorem OAI.Erdos3.model_error_norm_le line 624
  25. theorem OAI.Erdos3.exists_model_with_tail_error line 655
  26. theorem OAI.Erdos3.exists_model_of_small_weighted_tail line 716
  27. theorem OAI.Erdos3.exists_model_of_marginal_excess line 748