← Mathematical handbook

theorem Verification.gammaPDF_scale {a b c x : ℝ} (hb : 0 < b) (hc : 0 < c) (hx : 0 < x) : ENNReal.ofReal c * ProbabilityTheory.gammaPDF a (b / c) (c * x) = ProbabilityTheory.gammaPDF a b x

theorem Verification.gammaMeasure_map_mul {a b c : ℝ} (hb : 0 < b) (hc : 0 < c) : MeasureTheory.Measure.map (fun (x : ℝ) => c * x) (ProbabilityTheory.gammaMeasure a b) = ProbabilityTheory.gammaMeasure a (b / c)