intervalBounds

formal source

 107  | sigma σ _ => some σ
 108  | _ => none
 109
 110@[simp] def intervalBounds : Uncertainty → Option (ℝ × ℝ)
 111  | interval lo hi _ => some (lo, hi)
 112  | _ => none
 113
 114end Uncertainty
 115
 116/-- A measurement value with protocol + (optional) time window + (optional) uncertainty. -/
 117structure Measurement (α : Type) where
 118  value : α
 119  window : Option Window := none
 120  protocol : Protocol
 121  uncertainty : Option Uncertainty := none
 122  notes : List String := []
 123
 124namespace Measurement
 125
 126/-- Map the value of a measurement, preserving window/protocol/uncertainty/notes. -/
 127def map {α β : Type} (f : α → β) (m : Measurement α) : Measurement β :=
 128  { value := f m.value
 129    window := m.window
 130    protocol := m.protocol
 131    uncertainty := m.uncertainty
 132    notes := m.notes
 133  }
 134
 135/-- Map the value and replace protocol (e.g., when you derive a new observable). -/
 136def mapWithProtocol {α β : Type} (f : α → β) (p : Protocol) (m : Measurement α) : Measurement β :=
 137  { value := f m.value
 138    window := m.window
 139    protocol := p
 140    uncertainty := m.uncertainty