OAI/LinearAlgebra/MatrixFields/Entropy/JointExtractionRates.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.scale_exists line 18
2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridScale line 23
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.population_le_scale line 25
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.previous_scale_lt_population line 28
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.scale_pos line 32
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.scale_gt_of_population_gt line 39
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridScale_monotone line 47
8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridDimension line 51
9. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridWidth line 53
10. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridGroupOrder line 55
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridDimension_pos line 57
12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridWidth_ge_two line 60
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.dimension_le_power line 64
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.grid_population_bound line 73
15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridGroupOrder_eq line 99
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridGroupOrder_pos line 109
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.population_le_gridGroupOrder line 113
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridGroupOrder_monotone line 119
19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.asymptotic_grid_tags_slices line 125
20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.log_gridGroupOrder line 134
21. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.log_population_le_log_gridGroupOrder line 139
22. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.previous_scale_log_lt line 144
23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.log_gridGroupOrder_le_of_scale line 153
24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.scale_error_bound line 170
25. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.eventually_log_gridGroupOrder_le line 177
26. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.uniform_log_gridGroupOrder_le line 198
27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_div_log_population line 218
28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_div_nat line 240
29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.log_nat_prod line 274
30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.tendsto_log_nat_prod_div_nat line 281
31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_prod_div_nat line 294
32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.tendsto_log_nat_weighted_prod_div_nat line 304
33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_weighted_prod_div_nat line 318
34. def OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.goodCount line 342
35. def OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.goodIncidence line 346
36. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.sum_goodCount_eq_sum_goodIncidence line 350
37. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.exists_goodCount_ge line 357
38. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.exists_good_subfamily line 373
39. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventually_exists_good_subfamily line 381
40. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.incidence_lower_of_survival_and_loss line 392
41. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.exists_goodCount_ge_half_survival line 414
42. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.tendsto_polynomial_mul_exp_neg line 429
43. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventually_error_le_half line 441
44. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.tendsto_log_one_sub_error_div_nat line 453
45. def OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.hashModulus line 461
46. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.hashModulus_ge line 464
47. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.hashModulus_log_bounds line 469
48. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.tendsto_log_hashModulus_div_nat line 483
49. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventual_log_upper_of_error line 500
50. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventually_ratio_le_exp_neg_of_log_bounds line 513
51. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventually_degree_div_hashModulus_le_exp line 543
52. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.tendsto_sqrt_div_nat_of_div_nat line 555
53. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.tendsto_log_modularSet_card_div_nat line 569
54. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.tendsto_log_yield_lower line 595
55. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.exp_log_yield_lower line 611
56. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventually_floor_exp_le_of_log_lower line 624
57. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventually_exists_many_good line 638
58. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.eventually_exists_many_good_explicit line 674
59. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.fixed_product_subexponential line 698
60. theorem OAI.MatrixAllFields.MatrixMultiplication.JointExtractionRates.presence_replications_subexponential line 707