SegmentCodeEstimates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.SegmentCode.choose_weighted_le line 11
Source documentation
A weighted binomial coefficient estimate used for random binary blocks.
```
theorem choose_weighted_le (a u : ℕ) (hu : u ≤ a) :
    (a.choose u : ℝ) * 4 ^ (a-u) ≤ 5 ^ a := by
…
```
theorem OAI.TreeEdit.BinaryLower.SegmentCode.choose_le_weighted line 22
Source documentation
A convenient division-free consequence of the weighted estimate.
```
theorem choose_le_weighted (a u : ℕ) (hu : u ≤ a) :
    (a.choose u : ℝ) ≤ (5/4 : ℝ)^a * 4^u := by
…
```
theorem OAI.TreeEdit.BinaryLower.SegmentCode.weighted_identity line 33
theorem OAI.TreeEdit.BinaryLower.SegmentCode.nearly_full_matching_bound line 52
Source documentation
A prescribed almost-full common subsequence has an exponentially small union bound. The estimate is deliberately weaker than the manuscript's 2^(-a/2) but sufficient for the same fixed-length conversion theorem.
```
theorem nearly_full_matching_bound (a s : ℕ) (hs : s ≤ a)
    (hlarge : 99*a ≤ 100*s) :
    (a.choose s : ℝ)^2 * (1/2 : ℝ)^s ≤ (9/10 : ℝ)^a := by
…
```