Revision #1415 → #1762 · back to history
c10586f37cba| Field | From #1415 | To #1762 |
|---|---|---|
| note | An applied sample-size formula for bounded outputs with no Mathlib counterpart. | An applied sample-size formula for bounded outputs (Hoeffding-style); the underlying Hoeffding inequality is not yet formalized in Mathlib. |
8a474be55e009c4984c580933c4c6ef85ddf1deb7c87edc7