← Mathematical handbook

theorem Verification.gaussianPDFReal_scaled_inverse_sqrt {t c : ℝ} (ht : 0 < t) (hc : 0 < c) (m x : ℝ) : ProbabilityTheory.gaussianPDFReal m (NNReal.mk (((√t)⁻¹ * c) ^ 2) ⋯) x = (√(2 * Real.pi))⁻¹ * c⁻¹ * √t * Real.exp (-((x - m) ^ 2 / (2 * c ^ 2) * t))

noncomputable def Verification.studentQuadratic (r : ℝ) (p : ℝ × ℝ) : ℝ

Equations

• Verification.studentQuadratic r p = p.1 ^ 2 + (p.2 - r * p.1) ^ 2 / (1 - r ^ 2)

theorem Verification.studentQuadratic_nonneg {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (p : ℝ × ℝ) : 0 ≤ studentQuadratic r p

theorem Verification.student_gaussian_density_product {r t : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ht : 0 < t) (p : ℝ × ℝ) : ProbabilityTheory.gaussianPDF 0 (NNReal.mk ((√t)⁻¹ ^ 2) ⋯) p.1 * ProbabilityTheory.gaussianPDF (r * p.1) (NNReal.mk (((√t)⁻¹ * √(1 - r ^ 2)) ^ 2) ⋯) p.2 = ENNReal.ofReal (2 * Real.pi * √(1 - r ^ 2))⁻¹ * ENNReal.ofReal (t ^ 1 * Real.exp (-(studentQuadratic r p / 2 * t)))

noncomputable def Verification.studentJointPDF (r ν : ℝ) (p : ℝ × ℝ) : ℝ

Equations

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

theorem Verification.student_joint_density_evaluation {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (p : ℝ × ℝ) : gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯) (fun (t : ℝ) => (√t)⁻¹) p = ENNReal.ofReal (studentJointPDF r ν p)

theorem Verification.studentJointPDF_standard_form {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) {ν : ℝ} (hν : 0 < ν) (p : ℝ × ℝ) : studentJointPDF r ν p = (2 * Real.pi * √(1 - r ^ 2))⁻¹ * (1 + studentQuadratic r p / ν) ^ (-(ν / 2 + 1))

theorem Verification.studentQuadratic_standard_form {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (p : ℝ × ℝ) : studentQuadratic r p = (p.1 ^ 2 - 2 * r * p.1 * p.2 + p.2 ^ 2) / (1 - r ^ 2)