OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/ExtractionRates.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointExtractionRates.goodCount line 17
  2. def OAI.MatrixMultiplication.JointExtractionRates.goodIncidence line 21
  3. theorem OAI.MatrixMultiplication.JointExtractionRates.sum_goodCount_eq_sum_goodIncidence line 25
  4. theorem OAI.MatrixMultiplication.JointExtractionRates.exists_goodCount_ge line 32
  5. theorem OAI.MatrixMultiplication.JointExtractionRates.exists_good_subfamily line 48
  6. theorem OAI.MatrixMultiplication.JointExtractionRates.eventually_exists_good_subfamily line 56
  7. theorem OAI.MatrixMultiplication.JointExtractionRates.incidence_lower_of_survival_and_loss line 67
  8. theorem OAI.MatrixMultiplication.JointExtractionRates.exists_goodCount_ge_half_survival line 89
  9. theorem OAI.MatrixMultiplication.JointExtractionRates.tendsto_polynomial_mul_exp_neg line 104
  10. theorem OAI.MatrixMultiplication.JointExtractionRates.eventually_error_le_half line 116
  11. theorem OAI.MatrixMultiplication.JointExtractionRates.tendsto_log_one_sub_error_div_nat line 128
  12. def OAI.MatrixMultiplication.JointExtractionRates.hashModulus line 136
  13. theorem OAI.MatrixMultiplication.JointExtractionRates.hashModulus_ge line 139
  14. theorem OAI.MatrixMultiplication.JointExtractionRates.hashModulus_log_bounds line 144
  15. theorem OAI.MatrixMultiplication.JointExtractionRates.tendsto_log_hashModulus_div_nat line 158
  16. theorem OAI.MatrixMultiplication.JointExtractionRates.eventual_log_upper_of_error line 175
  17. theorem OAI.MatrixMultiplication.JointExtractionRates.eventually_ratio_le_exp_neg_of_log_bounds line 188
  18. theorem OAI.MatrixMultiplication.JointExtractionRates.eventually_degree_div_hashModulus_le_exp line 218
  19. theorem OAI.MatrixMultiplication.JointExtractionRates.tendsto_sqrt_div_nat_of_div_nat line 230
  20. theorem OAI.MatrixMultiplication.JointExtractionRates.tendsto_log_modularSet_card_div_nat line 244
  21. theorem OAI.MatrixMultiplication.JointExtractionRates.tendsto_log_yield_lower line 270
  22. theorem OAI.MatrixMultiplication.JointExtractionRates.exp_log_yield_lower line 286
  23. theorem OAI.MatrixMultiplication.JointExtractionRates.eventually_floor_exp_le_of_log_lower line 299
  24. theorem OAI.MatrixMultiplication.JointExtractionRates.eventually_exists_many_good line 313
  25. theorem OAI.MatrixMultiplication.JointExtractionRates.eventually_exists_many_good_explicit line 349
  26. theorem OAI.MatrixMultiplication.JointExtractionRates.fixed_product_subexponential line 373
  27. theorem OAI.MatrixMultiplication.JointExtractionRates.presence_replications_subexponential line 382