Documentation

Papers.AnsariRockel2024.StudentConditional

← Mathematical handbook

theorem Papers.AnsariRockel2024.student_precision_measure_update (ν : ℝ) (hν : 0 < ν) (x : ℝ) :

((ProbabilityTheory.gammaMeasure (ν / 2) (ν / 2)).withDensity fun (t : ℝ) => ProbabilityTheory.gaussianPDF 0 (NNReal.mk ((√t)⁻¹ ^ 2) ⋯) x) = ENNReal.ofReal (Verification.studentMarginalPDF ν x) • ProbabilityTheory.gammaMeasure (ν / 2 + 1 / 2) (ν / 2 + x ^ 2 / 2)

theorem Papers.AnsariRockel2024.student_joint_density_factorization (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x y : ℝ) :

ENNReal.ofReal (Verification.studentJointPDF r ν (x, y)) = ENNReal.ofReal (Verification.studentMarginalPDF ν x) * Verification.studentConditionalDensity r ν x y

theorem Papers.AnsariRockel2024.student_conditional_density_normalized (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x : ℝ) :

∫⁻ (y : ℝ), Verification.studentConditionalDensity r ν x y = 1

theorem Papers.AnsariRockel2024.student_conditional_cdf_mixture (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x y : ℝ) :

↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (Verification.studentConditionalDensity r ν x))) y = ∫ (t : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((y - r * x) * √t / √(1 - r ^ 2)) ∂ProbabilityTheory.gammaMeasure (ν / 2 + 1 / 2) (ν / 2 + x ^ 2 / 2)

theorem Papers.AnsariRockel2024.student_conditional_cdf_standard (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x y : ℝ) :

↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (Verification.studentConditionalDensity r ν x))) y = ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0)) ((y - r * x) / √((ν + x ^ 2) * (1 - r ^ 2) / (ν + 1)))

theorem Papers.AnsariRockel2024.student_joint_disintegration (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (f : ℝ × ℝ → ENNReal) (hf : Measurable f) :

∫⁻ (p : ℝ × ℝ), f p ∂MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) = ∫⁻ (x : ℝ), ∫⁻ (y : ℝ), f (x, y) ∂MeasureTheory.volume.withDensity (Verification.studentConditionalDensity r ν x) ∂ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0

theorem Papers.AnsariRockel2024.student_conditional_kernel_isMarkov (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) :

ProbabilityTheory.IsMarkovKernel (Verification.studentConditionalKernel r ν)

theorem Papers.AnsariRockel2024.student_joint_eq_compProd (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) :

MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) = (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0).compProd (Verification.studentConditionalKernel r ν)

theorem Papers.AnsariRockel2024.student_joint_rectangle_conditional (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (a b : ℝ) :

theorem Papers.AnsariRockel2024.student_cdf_conditional (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (a b : ℝ) :

theorem Papers.AnsariRockel2024.student_conditionalCDF_standard (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (b : ℝ) :

(fun (x : ℝ) => (Verification.studentBivariate r ⋯ ν hν).conditionalCDF (ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0) x) (ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 1) b)) =ᵐ[ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0] fun (x : ℝ) => ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0)) ((b - r * x) / √((ν + x ^ 2) * (1 - r ^ 2) / (ν + 1)))