← 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 Verification.equalSplit (n : ℕ) : ↑unitInterval

Equations

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

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

Equations

• Verification.equalBlocks 0 x✝ = x✝
• Verification.equalBlocks n.succ x✝ = x✝.ordinalSum (Verification.equalBlocks n x✝) (Verification.equalSplit n)

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

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

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

theorem Verification.HasFunctionalWitness.equalBlocks {C : ProbabilityTheory.Copula 2} (hC : HasFunctionalWitness C) (n : ℕ) : HasFunctionalWitness (Verification.equalBlocks n C)

theorem Verification.equalBlocks_lower_tail (C : ProbabilityTheory.Copula 2) {l : ℝ} (hC : C.HasLowerTailDependence l) (n : ℕ) : (equalBlocks n C).HasLowerTailDependence l

theorem Verification.equalBlocks_upper_tail (C : ProbabilityTheory.Copula 2) {l : ℝ} (hC : C.HasUpperTailDependence l) (n : ℕ) : (equalBlocks n C).HasUpperTailDependence l