def
definition
avg
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement on GitHub at line 75.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
72 meas : (ℝ → State) → ℝ → Obs
73
74/-- Midpoint sampling average (lightweight helper). -/
75@[simp] noncomputable def avg (T : ℝ) (_hT : 0 < T) (x : ℝ → ℝ) (t : ℝ) : ℝ :=
76 let tmid := t + T / 2
77 x tmid
78
79/-- CQ (coherence quotient) descriptor with bounds witnessed explicitly. -/
80structure CQ where
81 listensPerSec : ℝ
82 opsPerSec : ℝ
83 coherence8 : ℝ
84 coherence8_bounds :
85 0 ≤ coherence8 ∧ 0 ≤ coherence8 ∧ coherence8 ≤ 1 ∧ coherence8 ≤ 1
86
87/-- CQ score; zero when the operations-per-second denominator vanishes. -/
88@[simp] noncomputable def score (c : CQ) : ℝ :=
89 if c.opsPerSec = 0 then 0 else (c.listensPerSec / c.opsPerSec) * c.coherence8
90
91end Measurement
92end IndisputableMonolith