theorem
Papers.AnsariRockel2024.student_marginal_gaussian_limit
{ι : Type u_1}
{l : Filter ι}
(ν : ι → ℝ)
(hν : ∀ (i : ι), 0 < ν i)
(ht : Filter.Tendsto ν l Filter.atTop)
(r : ℝ)
(hr : r ∈ Set.Icc (-1) 1)
(j : Fin 2)
(a : ℝ)
:
Filter.Tendsto
(fun (i : ι) =>
↑(ProbabilityTheory.cdf
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) (ν i) ⋯) j))
a)
l (nhds (↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) a))
theorem
Papers.AnsariRockel2024.student_joint_gaussian_limit
{ι : Type u_1}
{l : Filter ι}
(ν : ι → ℝ)
(hν : ∀ (i : ι), 0 < ν i)
(ht : Filter.Tendsto ν l Filter.atTop)
(r : ℝ)
(hr : r ∈ Set.Icc (-1) 1)
(a b : ℝ)
:
Filter.Tendsto
(fun (i : ι) =>
(↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) (ν i) ⋯)).real (Set.Iic ![a, b]))
l
(nhds
((Verification.gaussianBivariate r hr).cdf
![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b]))
theorem
Papers.AnsariRockel2024.student_copula_gaussian_limit_interior
{ι : Type u_1}
{l : Filter ι}
(ν : ι → ℝ)
(hν : ∀ (i : ι), 0 < ν i)
(ht : Filter.Tendsto ν l Filter.atTop)
(r : ℝ)
(hr : r ∈ Set.Icc (-1) 1)
(u : Fin 2 → ↑unitInterval)
(hu : ∀ (j : Fin 2), ↑(u j) ∈ Set.Ioo 0 1)
:
Filter.Tendsto (fun (i : ι) => (Verification.studentBivariate r hr (ν i) ⋯).cdf u) l
(nhds ((Verification.gaussianBivariate r hr).cdf u))
theorem
Papers.AnsariRockel2024.student_copula_gaussian_limit
{ι : Type u_1}
{l : Filter ι}
(ν : ι → ℝ)
(hν : ∀ (i : ι), 0 < ν i)
(ht : Filter.Tendsto ν l Filter.atTop)
(r : ℝ)
(hr : r ∈ Set.Icc (-1) 1)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (Verification.studentBivariate r hr (ν i) ⋯).cdf u) l
(nhds ((Verification.gaussianBivariate r hr).cdf u))