← Mathematical handbook

theorem Verification.gaussianConditionalPDF_isTP2 {r : ℝ} (hr : 0 ≤ r) (v : NNReal) (hv : 0 < v) : ProbabilityTheory.IsTP2 fun (x y : ℝ) => ProbabilityTheory.gaussianPDFReal (r * x) v y

theorem Verification.gaussianDensityRatio_isTP2 {r : ℝ} (hr : 0 ≤ r) (v : NNReal) (hv : 0 < v) : ProbabilityTheory.IsTP2 fun (x y : ℝ) => ProbabilityTheory.gaussianPDFReal (r * x) v y / ProbabilityTheory.gaussianPDFReal 0 1 y

theorem Verification.gaussianCopulaDensity_isTP2 {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (hp : 0 ≤ r) : ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => gaussianCopulaDensity r ![u, v]

theorem Verification.gaussianBivariate_hasMTP2Density {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (hp : 0 ≤ r) : (gaussianBivariate r ⋯).HasMTP2Density

theorem Verification.gaussianBivariate_hasMTP2Density_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).HasMTP2Density ↔ 0 ≤ r ∧ r < 1