instBoundedRandomInt

Mathlib.Control.Random

URI: https://scilib.ai/kg/mathlib#Random.instBoundedRandomInt

Lean4

instance : BoundedRandom m Int where
  randomR lo hi h
    _ := do
    let ⟨z, _, h2⟩ ← randBound Nat 0 (Int.natAbs <| hi - lo) (Nat.zero_le _)
    pure
        ⟨z + lo, Int.le_add_of_nonneg_left (Int.ofNat_zero_le z),
          Int.add_le_of_le_sub_right <|
            Int.le_trans (Int.ofNat_le.mpr h2) (le_of_eq <| Int.natAbs_of_nonneg <| Int.sub_nonneg_of_le h)⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru