← Mathematical handbook

theorem Verification.student_marginal_cdf_continuous {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) : Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) i))

theorem Verification.student_marginal_cdf_strictMono {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) : StrictMono ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) i))

theorem Verification.studentBivariate_cdf_conditional {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (a b : ℝ) : (studentBivariate r ⋯ ν hν).cdf ![ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 1) 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

theorem Verification.measurable_studentConditional_cdf {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (b : ℝ) : Measurable fun (x : ℝ) => ↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (studentConditionalDensity r ν x))) b

theorem Verification.studentBivariate_conditionalCDF {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (b : ℝ) : (fun (x : ℝ) => (studentBivariate r ⋯ ν hν).conditionalCDF (ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0) x) (ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 1) b)) =ᵐ[ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0] fun (x : ℝ) => ↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (studentConditionalDensity r ν x))) b