theorem
Papers.AnsariRockel2024.laplace_joint_radial_density
(r : ℝ)
(hr : r ∈ Set.Ioo (-1) 1)
:
MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow
↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (Verification.bivariateCorrelation r)
(ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) =>
ENNReal.ofReal (2 * Real.pi * √(1 - r ^ 2))⁻¹ * Verification.laplaceRadialDensity ((p.1 ^ 2 - 2 * r * p.1 * p.2 + p.2 ^ 2) / (1 - r ^ 2))
The actual Laplace joint law, with its Gaussian variance mixture evaluated as a one-dimensional radial integral.
theorem
Papers.AnsariRockel2024.laplace_joint_density_tp2_counterexample
(r : ℝ)
(hr : r ∈ Set.Ioo (-1) 1)
:
∃ (t : ℝ),
0 < t ∧ t < 1 ∧ Verification.gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt (-1, 0) * Verification.gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt
(t, 1) < Verification.gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt (-1, 1) * Verification.gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt (t, 0)
A strict violation for the explicitly identified joint density. This statement does not yet exclude every almost-everywhere equivalent density.
theorem
Papers.AnsariRockel2024.laplace_joint_no_tp2_density_version
{r : ℝ}
(hr : r ∈ Set.Ioo (-1) 1)
:
¬∃ (g : ℝ × ℝ → ℝ),
Measurable g ∧ (∀ (p : ℝ × ℝ), 0 ≤ g p) ∧ (∀ (a b c d : ℝ), a ≤ b → c ≤ d → g (a, d) * g (b, c) ≤ g (a, c) * g (b, d)) ∧ MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow
↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (Verification.bivariateCorrelation r)
(ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ENNReal.ofReal (g p)