← Mathematical handbook

noncomputable def Verification.studentConditionalKernel (r ν : ℝ) : ProbabilityTheory.Kernel ℝ ℝ

Equations

• Verification.studentConditionalKernel r ν = (ProbabilityTheory.Kernel.const ℝ MeasureTheory.volume).withDensity (Verification.studentConditionalDensity r ν)

theorem Verification.studentConditionalKernel_apply {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x : ℝ) : (studentConditionalKernel r ν) x = MeasureTheory.volume.withDensity (studentConditionalDensity r ν x)

theorem Verification.studentConditionalKernel_isMarkov {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : ProbabilityTheory.IsMarkovKernel (studentConditionalKernel r ν)

theorem Verification.student_joint_eq_compProd {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) = (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0).compProd (studentConditionalKernel r ν)

theorem Verification.student_joint_rectangle_conditional {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (a b : ℝ) : (MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν)).real (Set.Iic a ×ˢ Set.Iic b) = ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (studentConditionalDensity r ν x))) b ∂ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0