hasDerivAt_neg_exp_mul_exp — Mathlib

English

The exponential pdf Real is measurable: measurability of exponentialPDFReal.

Русский

Плотность экспоненциального распределения является измеримой: измеримость exponentialPDFReal.

LaTeX

$$$ \\text{measurable\_exponentialPDFReal}(r) := \\text{Measurable}(\\text{exponentialPDFReal}(r)) $$$

Lean4

theorem hasDerivAt_neg_exp_mul_exp {r x : ℝ} : HasDerivAt (fun a ↦ -exp (-(r * a))) (r * exp (-(r * x))) x :=
  by
  convert (((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1)) using 1
  · simp only [one_mul, id_eq, neg_mul]
  simp only [id_eq, neg_mul, mul_one, mul_neg, one_mul, neg_neg, mul_comm]

Похожие утверждения