theorem
Verification.laplace_joint_real_density_continuousAt
{r : ℝ}
(hr : r ∈ Set.Ioo (-1) 1)
{p : ℝ × ℝ}
(hp : p ≠ (0, 0))
:
ContinuousAt
(fun (z : ℝ × ℝ) =>
(gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt z).toReal)
p
theorem
Verification.laplace_joint_no_tp2_density
{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 (bivariateCorrelation r)
(ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ENNReal.ofReal (g p)
No nonnegative measurable TP2 density represents the actual Laplace joint law.