`Measurement`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RSNative.Core
domain: Measurement
line: 117 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Measurement.RSNative.Core on GitHub at line 117.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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
 141    notes := m.notes
 142  }
 143
 144/-- Transform the uncertainty record (when present). -/
 145def mapUncertainty {α : Type} (uMap : Uncertainty → Uncertainty) (m : Measurement α) : Measurement α :=
 146  { value := m.value
 147    window := m.window

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.