Documentation

Papers.Rockel2025Approximation.EqualGrids

← Mathematical handbook

Proposition 3.3 on all equal diagonal grids #

Here N=n+1 is any positive integer and Delta=I_N/N. This removes the dyadic restriction for rho and tau and adds deterministic xi and tail values.

source
noncomputable def Papers.Rockel2025Approximation.equalGrid (n : ℕ) (C : ProbabilityTheory.Copula 2) :
ProbabilityTheory.Copula 2
Equations
Instances For
    source
    theorem Papers.Rockel2025Approximation.equalGrid_cdf (n : ℕ) (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) :
    (equalGrid (n + 1) C).cdf ![u, v] = 1 / (↑n + 2) * C.cdf ![ProbabilityTheory.Copula.OrdinalSum.lowerCoord (Verification.equalSplit n) u, ProbabilityTheory.Copula.OrdinalSum.lowerCoord (Verification.equalSplit n) v] + (1 - 1 / (↑n + 2)) * (equalGrid n C).cdf ![ProbabilityTheory.Copula.OrdinalSum.upperCoord (Verification.equalSplit n) u, ProbabilityTheory.Copula.OrdinalSum.upperCoord (Verification.equalSplit n) v]
    source
    theorem Papers.Rockel2025Approximation.equalGrid_rho_tau (n : ℕ) (C : ProbabilityTheory.Copula 2) :
    (equalGrid n C).spearmanRho = 1 - (1 - C.spearmanRho) / (↑n + 1) ^ 2 ∧ (equalGrid n C).kendallTau = 1 - (1 - C.kendallTau) / (↑n + 1)
    source
    theorem Papers.Rockel2025Approximation.equal_checkerboard_rho_tau (n : ℕ) :
    (equalGrid n (ProbabilityTheory.Copula.independence 2)).spearmanRho = 1 - 1 / (↑n + 1) ^ 2 ∧ (equalGrid n (ProbabilityTheory.Copula.independence 2)).kendallTau = 1 - 1 / (↑n + 1)
    source
    theorem Papers.Rockel2025Approximation.equal_checkMin_coefficients (n : ℕ) :
    (equalGrid n (ProbabilityTheory.Copula.comonotonic 2)).spearmanRho = (equalGrid n (ProbabilityTheory.Copula.independence 2)).spearmanRho + 1 / (↑n + 1) ^ 2 ∧ (equalGrid n (ProbabilityTheory.Copula.comonotonic 2)).kendallTau = (equalGrid n (ProbabilityTheory.Copula.independence 2)).kendallTau + 1 / (↑n + 1) ∧ (equalGrid n (ProbabilityTheory.Copula.comonotonic 2)).chatterjeeXi = 1
    source
    theorem Papers.Rockel2025Approximation.equal_checkW_coefficients (n : ℕ) :
    (equalGrid n ProbabilityTheory.Copula.countermonotonic).spearmanRho = (equalGrid n (ProbabilityTheory.Copula.independence 2)).spearmanRho - 1 / (↑n + 1) ^ 2 ∧ (equalGrid n ProbabilityTheory.Copula.countermonotonic).kendallTau = (equalGrid n (ProbabilityTheory.Copula.independence 2)).kendallTau - 1 / (↑n + 1) ∧ (equalGrid n ProbabilityTheory.Copula.countermonotonic).chatterjeeXi = 1
    source
    theorem Papers.Rockel2025Approximation.equal_checkerboard_tails (n : ℕ) :
    (equalGrid n (ProbabilityTheory.Copula.independence 2)).HasLowerTailDependence 0 ∧ (equalGrid n (ProbabilityTheory.Copula.independence 2)).HasUpperTailDependence 0
    source
    theorem Papers.Rockel2025Approximation.equal_checkMin_tails (n : ℕ) :
    (equalGrid n (ProbabilityTheory.Copula.comonotonic 2)).HasLowerTailDependence 1 ∧ (equalGrid n (ProbabilityTheory.Copula.comonotonic 2)).HasUpperTailDependence 1
    source
    theorem Papers.Rockel2025Approximation.equal_checkW_tails (n : ℕ) :
    (equalGrid n ProbabilityTheory.Copula.countermonotonic).HasLowerTailDependence 0 ∧ (equalGrid n ProbabilityTheory.Copula.countermonotonic).HasUpperTailDependence 0