← Mathematical handbook

theorem Verification.laplace_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⁻¹ * Real.exp (-(studentQuadratic r p / (2 * t))))

noncomputable def Verification.laplaceRadialDensity (q : ℝ) : ENNReal

The radial integral of the bivariate Laplace mixture. Its value may be infinite.

Equations

• Verification.laplaceRadialDensity q = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (t⁻¹ * Real.exp (-t - q / (2 * t)))

theorem Verification.laplace_joint_density_evaluation {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (p : ℝ × ℝ) : gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt p = ENNReal.ofReal (2 * Real.pi * √(1 - r ^ 2))⁻¹ * laplaceRadialDensity (studentQuadratic r p)

theorem Verification.laplaceRadialDensity_antitone : Antitone laplaceRadialDensity

theorem Verification.laplace_joint_radial_withDensity {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ENNReal.ofReal (2 * Real.pi * √(1 - r ^ 2))⁻¹ * laplaceRadialDensity (studentQuadratic r p)