Documentation

Papers.AnsariRockel2026XiRho.BandOptimization

← Mathematical handbook

Global optimization for the normalization-defined diagonal-band family #

The explicit piecewise intercept and coefficient formulas for general slopes are separate obligations. This file constructs all slopes and proves their optimality using the marginal normalization directly.

source
@[reducible, inline]
noncomputable abbrev Papers.AnsariRockel2026XiRho.normalizedBand (b : ℝ) (hb : 0 ≤ b) :
ProbabilityTheory.Copula 2

The normalized clamped-affine family, for the entire nonnegative slope range.

Equations
Instances For
    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_conditionalCDF (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) :
    (fun (u : ↑unitInterval) => (normalizedBand b hb).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.unitClamp (Verification.bandIntercept b hb v - b * ↑u)
    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_isSI (b : ℝ) (hb : 0 ≤ b) :
    (normalizedBand b hb).IsSI
    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_support (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 ≤ b) :
    b * C.spearmanRho - C.chatterjeeXi ≤ b * (normalizedBand b hb).spearmanRho - (normalizedBand b hb).chatterjeeXi
    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_support_eq_iff (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 ≤ b) :
    b * C.spearmanRho - C.chatterjeeXi = b * (normalizedBand b hb).spearmanRho - (normalizedBand b hb).chatterjeeXi ↔ C = normalizedBand b hb
    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_maximal_rho (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi ≤ (normalizedBand b ⋯).chatterjeeXi) :
    C.spearmanRho ≤ (normalizedBand b ⋯).spearmanRho
    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_maximal_rho_eq_iff (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi = (normalizedBand b ⋯).chatterjeeXi) :
    C.spearmanRho = (normalizedBand b ⋯).spearmanRho ↔ C = normalizedBand b ⋯
    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_one :
    normalizedBand 1 ⋯ = unitDiagonalBand

    The implicitly normalized slope-one copula is exactly the explicit source copula.

    source
    theorem Papers.AnsariRockel2026XiRho.normalizedBand_zero :
    normalizedBand 0 ⋯ = ProbabilityTheory.Copula.independence 2

    The zero-slope endpoint is independence, without taking an assumed limit.