← Mathematical handbook

theorem Verification.symmetricCopula_diagonal_eq_triangle (C : ProbabilityTheory.Copula 2) (hC : C.transpose = C) (hac : C.toMeasure.AbsolutelyContinuous MeasureTheory.volume) (t : ↑unitInterval) : C.diagonal t = 2 * C.toMeasure.real {u : Fin 2 → ↑unitInterval | u 0 ≤ t ∧ u 1 ≤ u 0}

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

theorem Verification.studentBivariate_triangle_conditional {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (a : ℝ) : (studentBivariate r ⋯ ν hν).toMeasure.real {u : Fin 2 → ↑unitInterval | u 0 ≤ ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0) a ∧ u 1 ≤ u 0} = ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (studentConditionalDensity r ν x))) x ∂ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0

theorem Verification.studentBivariate_diagonal_conditional {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (a : ℝ) : (studentBivariate r ⋯ ν hν).diagonal (ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0) a) = 2 * ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (studentConditionalDensity r ν x))) x ∂ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0