variation

Mathlib.Util.CountHeartbeats

URI: https://scilib.ai/kg/mathlib#Mathlib.CountHeartbeats.variation

Lean4

/-- Given a `List Nat`, return the minimum, maximum, and standard deviation.
-/
def variation (counts : List Nat) : List Nat :=
  let min := counts.min?.getD 0
  let max := counts.max?.getD 0
  let toFloat (n : Nat) := n.toUInt64.toFloat
  let toNat (f : Float) := f.toUInt64.toNat
  let counts' := counts.map toFloat
  let μ : Float := counts'.foldl (· + ·) 0 / toFloat counts.length
  let stddev : Float := Float.sqrt <| ((counts'.map fun i => (i - μ) ^ 2).foldl (· + ·) 0) / toFloat counts.length
  [min, max, toNat stddev]

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

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

Разделы

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

Аффилиация

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