`scaleUncertainty`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RSNative.Calibration.SI
domain: Measurement
line: 44 · 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 44.

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

  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
  56      (fun u => scaleUncertainty cal.seconds_per_tick (le_of_lt cal.seconds_pos) u) m)
  57
  58noncomputable def measure_to_meters (cal : ExternalCalibration) (m : Measurement Voxel) : Measurement ℝ :=
  59  Measurement.map (to_meters cal)
  60    (Measurement.mapUncertainty
  61      (fun u => scaleUncertainty cal.meters_per_voxel (le_of_lt cal.meters_pos) u) m)
  62
  63noncomputable def measure_to_joules (cal : ExternalCalibration) (m : Measurement Coh) : Measurement ℝ :=
  64  Measurement.map (to_joules cal)
  65    (Measurement.mapUncertainty
  66      (fun u => scaleUncertainty cal.joules_per_coh (le_of_lt cal.joules_pos) u) m)
  67
  68noncomputable def measure_to_joule_seconds (cal : ExternalCalibration) (m : Measurement Act) : Measurement ℝ :=
  69  Measurement.map (to_joule_seconds cal)
  70    (Measurement.mapUncertainty
  71      (fun u =>
  72        scaleUncertainty (cal.joules_per_coh * cal.seconds_per_tick)
  73          (mul_nonneg (le_of_lt cal.joules_pos) (le_of_lt cal.seconds_pos)) u) m)
  74

papers checked against this theorem

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