The nonnegative-real exponential law

This module isolates the elementary push-forward identity relating the NNReal model of a unit exponential to Mathlib's real-valued exponential measure.

theorem Feige.map_nnexpMeasure_coe : MeasureTheory.Measure.map (fun (x : NNReal) => ↑x) nnexpMeasure = ProbabilityTheory.expMeasure 1