← Mathematical handbook

theorem Verification.laplaceRadialDensity_pos (q : ℝ) : 0 < laplaceRadialDensity q

theorem Verification.studentQuadratic_pos {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) {p : ℝ × ℝ} (hp : p ≠ (0, 0)) : 0 < studentQuadratic r p

theorem Verification.laplace_radial_tp2_witness {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : ∃ (t : ℝ), 0 < t ∧ t < 1 ∧ laplaceRadialDensity (studentQuadratic r (-1, 0)) * laplaceRadialDensity (studentQuadratic r (t, 1)) < laplaceRadialDensity (studentQuadratic r (-1, 1)) * laplaceRadialDensity (studentQuadratic r (t, 0))

A strict TP2 violation with all four evaluation points away from the singular origin.

theorem Verification.laplace_joint_density_tp2_witness {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : ∃ (t : ℝ), 0 < t ∧ t < 1 ∧ gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt (-1, 0) * gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt (t, 1) < gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt (-1, 1) * gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt (t, 0)