← Mathematical handbook

noncomputable def Verification.studentBivariate (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : ProbabilityTheory.Copula 2

Equations

• Verification.studentBivariate r hr ν hν = ProbabilityTheory.Copula.studentT (Verification.bivariateCorrelation r) ⋯ ⋯ ν hν

theorem Verification.studentBivariate_isSklarCopula (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : ProbabilityTheory.Copula.IsSklarCopula (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) (studentBivariate r hr ν hν)

theorem Verification.ofContinuousMarginals_comonotonic_of_ae_eq (μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)) (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal μ i))) (he : ∀ᵐ (x : Fin 2 → ℝ) ∂↑μ, x 0 = x 1) : ProbabilityTheory.Copula.ofContinuousMarginals μ hc = ProbabilityTheory.Copula.comonotonic 2

theorem Verification.gaussian_one_ae_equal : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation 1), x.ofLp 0 = x.ofLp 1

theorem Verification.gaussianScaleMixture_one (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation 1) ⋯ ⋯ μ s hs hp = ProbabilityTheory.Copula.comonotonic 2

theorem Verification.studentBivariate_one (ν : ℝ) (hν : 0 < ν) : studentBivariate 1 ⋯ ν hν = ProbabilityTheory.Copula.comonotonic 2