OAI/Analysis/FiniteFactor/TagExponentialLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.log_one_sub_ge_neg_two line 11

   Source documentation

   The explicit logarithm bound used in the source tag probability.

   theorem log_one_sub_ge_neg_two {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1/2) :
       -2*t ≤ Real.log (1-t) := by
   …

2. theorem OAI.FiniteFactor.tag_probability_exponential_lower line 23

   Source documentation

   The source's exactly-one-tag probability has a uniform positive lower bound, despite the growing block size.

   theorem tag_probability_exponential_lower (m : ℕ) (hm : 100 ≤ m) :
       Real.exp (-82) ≤ (1-41/(m : ℝ))^(m-1) := by
   …