← Mathematical handbook

Equal diagonal blocks of every positive size

The index n represents n+1 cells, so no zero-cell convention is needed.

noncomputable def ProbabilityTheory.Copula.RankRegion.equalSplit (n : ℕ) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.equalSplit n = ⟨1 / (↑n + 2), ⋯⟩

noncomputable def ProbabilityTheory.Copula.RankRegion.equalBlocks : ℕ → Copula 2 → Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.equalBlocks 0 x✝ = x✝
• ProbabilityTheory.Copula.RankRegion.equalBlocks n.succ x✝ = x✝.ordinalSum (ProbabilityTheory.Copula.RankRegion.equalBlocks n x✝) (ProbabilityTheory.Copula.RankRegion.equalSplit n)

theorem ProbabilityTheory.Copula.RankRegion.equalBlocks_rho (n : ℕ) (C : Copula 2) : (equalBlocks n C).spearmanRho = 1 - (1 - C.spearmanRho) / (↑n + 1) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.equalBlocks_tau (n : ℕ) (C : Copula 2) : (equalBlocks n C).kendallTau = 1 - (1 - C.kendallTau) / (↑n + 1)

theorem ProbabilityTheory.Copula.RankRegion.equalBlocks_footrule (n : ℕ) (C : Copula 2) : (equalBlocks n C).spearmanFootrule = 1 - (1 - C.spearmanFootrule) / (↑n + 1)