OAI/NumberTheory/TotientAsymptotic/TailBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite tail bounds and nonnegative coefficients from exponential random variables.

  1. lemma OAI.TotientAsymptotic.alpha_le line 13
  2. def OAI.TotientAsymptotic.tailPrimeBound line 22
  3. def OAI.TotientAsymptotic.tailCofactorBound line 25
  4. lemma OAI.TotientAsymptotic.one_le_tailPrimeBound line 28
  5. lemma OAI.TotientAsymptotic.index_inv_pow_mono line 34
  6. lemma OAI.TotientAsymptotic.witness_prime_bound line 43
  7. lemma OAI.TotientAsymptotic.witness_cofactor_bound line 74
  8. def OAI.TotientAsymptotic.tailUniverse line 89
  9. lemma OAI.TotientAsymptotic.tailUniverse_finite line 93
  10. lemma OAI.TotientAsymptotic.witness_mem_tailUniverse line 107
  11. theorem OAI.TotientAsymptotic.finite_tail_data line 111
  12. lemma OAI.TotientAsymptotic.witnesses_finite line 117
  13. lemma OAI.TotientAsymptotic.witness_w_bound line 125
  14. lemma OAI.TotientAsymptotic.witness_totient_bound line 139
  15. lemma OAI.TotientAsymptotic.tailLog_nonneg line 145
  16. lemma OAI.TotientAsymptotic.D_nonneg line 152
  17. def OAI.TotientAsymptotic.tailMass line 160
  18. lemma OAI.TotientAsymptotic.tailMass_nonneg line 162
  19. lemma OAI.TotientAsymptotic.D_le_log line 166
  20. lemma OAI.TotientAsymptotic.D_le_linear line 181
  21. lemma OAI.TotientAsymptotic.maxD_nonneg line 188
  22. lemma OAI.TotientAsymptotic.maxD_le_linear line 197
  23. theorem OAI.TotientAsymptotic.summable_tail_threshold line 211
  24. lemma OAI.TotientAsymptotic.finite_witness_subsets line 228
  25. instance OAI.TotientAsymptotic.expOne_probability line 237
  26. def OAI.TotientAsymptotic.exponentialProduct line 240
  27. instance OAI.TotientAsymptotic.exponentialProduct_probability line 243
  28. lemma OAI.TotientAsymptotic.expOne_real_Ioi line 247
  29. lemma OAI.TotientAsymptotic.expOne_Ioi line 253
  30. lemma OAI.TotientAsymptotic.exponential_box_probability line 257
  31. def OAI.TotientAsymptotic.witnessEvent line 273
  32. lemma OAI.TotientAsymptotic.measurableSet_witnessEvent line 276
  33. lemma OAI.TotientAsymptotic.threshold_coefficient_pos line 280
  34. lemma OAI.TotientAsymptotic.witnessEvent_intersection line 284
  35. lemma OAI.TotientAsymptotic.witnessEvent_intersection_probability line 308
  36. lemma OAI.TotientAsymptotic.coefficient_eq_union_probability line 320
  37. theorem OAI.TotientAsymptotic.AH_nonneg line 358