RootInformationBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual root information coefficient lies in the unit interval

Truncation, finite Hopf bounds and monotone convergence turn the almost sure linear small-ball bound into a finite mean bound. No entropy formula or ergodic theorem is assumed.

theorem OAI.DukePrimeDegree.rootInformationMean_le_one line 29
Source documentation
The coefficient defined by the actual root leaf information is finite and at most one.
```
theorem rootInformationMean_le_one : rootInformationMean hij μ 1 ≤ 1 := by
…
```