← Mathematical handbook

noncomputable def Verification.sampleRankCopula {Ω : Type u_1} (X : ℕ → Ω → Fin 2 → ↑unitInterval) (n : ℕ) (ω : Ω) : ProbabilityTheory.Copula 2

Rank-based empirical copula. Its value on tied samples is immaterial under continuous marginal laws and is fixed to independence.

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.sampleRankCopula_ae_rate {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (C : ProbabilityTheory.Copula 2) (X : ℕ → Ω → Fin 2 → ↑unitInterval) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : ProbabilityTheory.iIndepFun X μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = C.toMeasure) : ∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (u v : ↑unitInterval), |(sampleRankCopula X n ω).cdf ![u, v] - C.cdf ![u, v]| ≤ 3 * empiricalCDFRadius n + 8 / (↑n + 1)

Almost-sure uniform CDF rate for the actual rank-based empirical copula.