Documentation

Papers.AnsariRockel2026RhoFootrule.FoldedExample

← Mathematical handbook

Example 2.8 with the source's exact folded-uniform joint law #

source
@[reducible, inline]
noncomputable abbrev Papers.AnsariRockel2026RhoFootrule.foldedExample :
ProbabilityTheory.Copula 2
Equations
Instances For
    source
    theorem Papers.AnsariRockel2026RhoFootrule.foldedExample_joint_law :
    foldedExample.toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ![Verification.foldRank u, u]) MeasureTheory.volume

    X=abs(2U-1) and Y=U, with U uniform, exactly as in the source.

    source
    theorem Papers.AnsariRockel2026RhoFootrule.foldedExample_uniform_predictor :
    MeasureTheory.MeasurePreserving Verification.foldRank MeasureTheory.volume MeasureTheory.volume
    source
    theorem Papers.AnsariRockel2026RhoFootrule.foldedExample_conditionalCDF (v : ↑unitInterval) :
    (fun (u : ↑unitInterval) => foldedExample.conditionalCDF u v) =ᵐ[MeasureTheory.volume] Verification.foldKernel v

    The conditional distribution is equally supported at (1-r)/2 and (1+r)/2.

    source
    theorem Papers.AnsariRockel2026RhoFootrule.foldedExample_conditionalMean :
    Verification.conditionalMean foldedExample =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1 / 2
    source
    theorem Papers.AnsariRockel2026RhoFootrule.foldedExample_coefficients :
    foldedExample.chatterjeeXi = 1 / 4 ∧ copulaCorrelationRatio foldedExample = 0
    source
    theorem Papers.AnsariRockel2026RhoFootrule.quarter_xi_zero_ratio_attained :
    ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = 1 / 4 ∧ copulaCorrelationRatio C = 0

    An actual copula attains the bottom of the quarter-xi slice.

    source
    theorem Papers.AnsariRockel2026RhoFootrule.zero_ratio_interval_attained (x : ℝ) (hx : x ∈ Set.Icc 0 (1 / 4)) :
    ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ copulaCorrelationRatio C = 0

    The entire horizontal part of the constructive lower inner curve (44).