pith. machine review for the scientific record. sign in
def definition def or abbrev

measure_to_joule_seconds

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  68noncomputable def measure_to_joule_seconds (cal : ExternalCalibration) (m : Measurement Act) : Measurement ℝ :=

proof body

Definition body.

  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
  75end SI
  76end Calibration
  77end RSNative
  78end Measurement
  79end IndisputableMonolith

depends on (11)

Lean names referenced from this declaration's body.