Tail.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceCutoff_ge_shift line 10
theorem OAI.FiniteFactor.sourceCutoff_tail_bound line 20
Source documentation
The exact geometric tail estimate used in scales and tail trimming.
```
theorem sourceCutoff_tail_bound (s : ℕ) :
    (∑' n : ℕ, 1 / ((sourceStageState (s+n)).K : ℝ)) ≤
      2 / ((sourceStageState s).K : ℝ) := by
…
```
Mentions: OAI.FiniteFactor.sourceStageState
def OAI.FiniteFactor.sourceTailAngleSum line 38
theorem OAI.FiniteFactor.SourceAngles.tail_sum_bound line 41
theorem OAI.FiniteFactor.sourceSampling_tail_ratio line 66
Source documentation
The largest proposed sampling power divided by the next cutoff has the source exponent gap 7/10 - 3/4 = -1/20.
```
theorem sourceSampling_tail_ratio (s : ℕ) :
    4 * (sourceBlockSize s : ℝ)^((7/10 : ℝ)*(sourceBlockSize s : ℝ)) /
      ((sourceStageState (s+1)).K : ℝ) ≤
    4 * (sourceBlockSize s : ℝ)^(-(sourceBlockSize s : ℝ)/20) := by
…
```
Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceStageState