← Mathematical handbook

noncomputable def Verification.huslerReissExponent (δ x y : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.huslerReiss_density_balance (δ x y : ℝ) (hδ : 0 < δ) (hx : 0 < x) (hy : 0 < y) : x * ProbabilityTheory.gaussianPDFReal 0 1 (1 / δ + δ / 2 * Real.log (x / y)) = y * ProbabilityTheory.gaussianPDFReal 0 1 (1 / δ + δ / 2 * Real.log (y / x))

theorem Verification.huslerReissExponent_hasDerivAt (δ x y : ℝ) (hδ : 0 < δ) (hx : 0 < x) (hy : 0 < y) : HasDerivAt (fun (d : ℝ) => huslerReissExponent d x y) (-2 / δ ^ 2 * (x * ProbabilityTheory.gaussianPDFReal 0 1 (1 / δ + δ / 2 * Real.log (x / y)))) δ

theorem Verification.huslerReissExponent_antitone (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : AntitoneOn (fun (δ : ℝ) => huslerReissExponent δ x y) (Set.Ioi 0)