Documentation

Papers.AnsariRockel2026XiRho.DiagonalBandUnit

← Mathematical handbook

The unit-slope diagonal-band copula #

The b = 1 member of equations (19)--(22), including both response endpoints.

noncomputable def Papers.AnsariRockel2026XiRho.unitBandIntercept (v : ↑unitInterval) :

Equations

Papers.AnsariRockel2026XiRho.unitBandIntercept v = if ↑v ≤ 1 / 2 then √(2 * ↑v) else 2 - √(2 * (1 - ↑v))

Instances For

noncomputable def Papers.AnsariRockel2026XiRho.unitBandKernel (v u : ↑unitInterval) :

Equations

Papers.AnsariRockel2026XiRho.unitBandKernel v u = Verification.unitClamp (Papers.AnsariRockel2026XiRho.unitBandIntercept v - ↑u)

Instances For

theorem Papers.AnsariRockel2026XiRho.sqrt_two_mem {v : ↑unitInterval} (hv : ↑v ≤ 1 / 2) :

√(2 * ↑v) ∈ Set.Icc 0 1

theorem Papers.AnsariRockel2026XiRho.unitBandIntercept_monotone :

Monotone unitBandIntercept

theorem Papers.AnsariRockel2026XiRho.unitBandKernel_monotone (u : ↑unitInterval) :

Monotone fun (v : ↑unitInterval) => unitBandKernel v u

theorem Papers.AnsariRockel2026XiRho.unitBandKernel_integrable (v : ↑unitInterval) :

MeasureTheory.Integrable (unitBandKernel v) MeasureTheory.volume

theorem Papers.AnsariRockel2026XiRho.unitBandKernel_lower (v u : ↑unitInterval) (hv : ↑v ≤ 1 / 2) :

unitBandKernel v u = Verification.ramp ⟨√(2 * ↑v), ⋯⟩ u

theorem Papers.AnsariRockel2026XiRho.unitBandKernel_upper (v u : ↑unitInterval) (hv : 1 / 2 ≤ ↑v) :

unitBandKernel v u = 1 - Verification.ramp ⟨√(2 * (1 - ↑v)), ⋯⟩ (unitInterval.symm u)

theorem Papers.AnsariRockel2026XiRho.unitBandKernel_zero (u : ↑unitInterval) :

unitBandKernel 0 u = 0

theorem Papers.AnsariRockel2026XiRho.unitBandKernel_one (u : ↑unitInterval) :

unitBandKernel 1 u = 1

theorem Papers.AnsariRockel2026XiRho.unitBandKernel_mean (v : ↑unitInterval) :

∫ (u : ↑unitInterval), unitBandKernel v u = ↑v

noncomputable def Papers.AnsariRockel2026XiRho.unitDiagonalBand :

ProbabilityTheory.Copula 2

The actual copula C₁ from the article, constructed from its conditional law.

Equations

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

Instances For

theorem Papers.AnsariRockel2026XiRho.unitDiagonalBand_cdf (u v : ↑unitInterval) :

unitDiagonalBand.cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, unitBandKernel v t

theorem Papers.AnsariRockel2026XiRho.unitDiagonalBand_conditionalCDF (v : ↑unitInterval) :

(fun (u : ↑unitInterval) => unitDiagonalBand.conditionalCDF u v) =ᵐ[MeasureTheory.volume] unitBandKernel v

theorem Papers.AnsariRockel2026XiRho.unitDiagonalBand_derivative (v : ↑unitInterval) :

(fun (u : ↑unitInterval) => deriv (unitDiagonalBand.cdfSection v) ↑u) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.unitClamp (unitBandIntercept v - ↑u)

theorem Papers.AnsariRockel2026XiRho.unitDiagonalBand_isSI :

unitDiagonalBand.IsSI

theorem Papers.AnsariRockel2026XiRho.unitDiagonalBand_support (C : ProbabilityTheory.Copula 2) :

C.spearmanRho - C.chatterjeeXi ≤ unitDiagonalBand.spearmanRho - unitDiagonalBand.chatterjeeXi

theorem Papers.AnsariRockel2026XiRho.unitDiagonalBand_support_eq_iff (C : ProbabilityTheory.Copula 2) :

C.spearmanRho - C.chatterjeeXi = unitDiagonalBand.spearmanRho - unitDiagonalBand.chatterjeeXi ↔ C = unitDiagonalBand