`to_seconds`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RSNative.Calibration.SI
domain: Measurement
line: 25 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.RSNative.Calibration.SI on GitHub at line 25.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  22
  23/-! ## Scalar conversions -/
  24
  25@[simp] noncomputable def to_seconds (cal : ExternalCalibration) (t : Tick) : ℝ :=
  26  (t : ℝ) * cal.seconds_per_tick
  27
  28@[simp] noncomputable def to_meters (cal : ExternalCalibration) (L : Voxel) : ℝ :=
  29  (L : ℝ) * cal.meters_per_voxel
  30
  31@[simp] noncomputable def to_joules (cal : ExternalCalibration) (E : Coh) : ℝ :=
  32  (E : ℝ) * cal.joules_per_coh
  33
  34/-- Convert action quanta (act) to SI \(J·s\).
  35
  36In RS-native units, `1 act` corresponds to `1 coh * 1 tick`.
  37So the SI conversion is `joules_per_coh * seconds_per_tick`.
  38-/
  39@[simp] noncomputable def to_joule_seconds (cal : ExternalCalibration) (A : Act) : ℝ :=
  40  (A : ℝ) * (cal.joules_per_coh * cal.seconds_per_tick)
  41
  42/-! ## Measurement-level conversion helpers -/
  43
  44private def scaleUncertainty (c : ℝ) (hc : 0 ≤ c) (u : Uncertainty) : Uncertainty :=
  45  match u with
  46  | .sigma σ hσ =>
  47      .sigma (σ * c) (mul_nonneg hσ hc)
  48  | .interval lo hi hlohi =>
  49      .interval (lo * c) (hi * c) (mul_le_mul_of_nonneg_right hlohi hc)
  50  | .discrete support =>
  51      .discrete (support.map (fun vw => (vw.1 * c, vw.2)))
  52
  53noncomputable def measure_to_seconds (cal : ExternalCalibration) (m : Measurement Tick) : Measurement ℝ :=
  54  Measurement.map (to_seconds cal)
  55    (Measurement.mapUncertainty

papers checked against this theorem

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