← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_sub_abs_le_uniform {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (f g : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (ε : ℝ) (h : ∀ (x : Ω), |f x - g x| ≤ ε) : |∫ (x : Ω), f x ∂μ - ∫ (x : Ω), g x ∂μ| ≤ ε

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.spearmanRho_cdf_stability (C D : Copula 2) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) : |C.spearmanRho - D.spearmanRho| ≤ 12 * ε

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.spearmanFootrule_cdf_stability (C D : Copula 2) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) : |C.spearmanFootrule - D.spearmanFootrule| ≤ 6 * ε

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalCDFRadius_tendsto : Filter.Tendsto empiricalCDFRadius Filter.atTop (nhds 0)

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.exists_permutationShuffle_rank_limits (C : Copula 2) : ∃ (π : (n : ℕ) → Equiv.Perm (Fin (n + 1))), Filter.Tendsto (fun (n : ℕ) => (PermutationShuffle.copula n (π n)).spearmanRho) Filter.atTop (nhds C.spearmanRho) ∧ Filter.Tendsto (fun (n : ℕ) => (PermutationShuffle.copula n (π n)).spearmanFootrule) Filter.atTop (nhds C.spearmanFootrule)

Equal-width permutation shuffles approximate both rank coefficients of every copula.