← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalCDFRadius_scaled_bound (n : ℕ) : (↑n + 2) ^ (1 / 3) * empiricalCDFRadius n ≤ √(16 * Real.log (↑n + 2) / (↑n + 2) ^ (1 / 3))

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalCDFRadius_scaled_tendsto : Filter.Tendsto (fun (n : ℕ) => (↑n + 2) ^ (1 / 3) * empiricalCDFRadius n) Filter.atTop (nhds 0)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalMesh_scaled_tendsto : Filter.Tendsto (fun (n : ℕ) => (↑n + 2) ^ (1 / 3) / (↑n + 1)) Filter.atTop (nhds 0)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalRankRate_scaled_tendsto : Filter.Tendsto (fun (n : ℕ) => (↑n + 2) ^ (1 / 3) * (3 * empiricalCDFRadius n + 8 / (↑n + 1))) Filter.atTop (nhds 0)