Documentation

Papers.AnsariRockel2026RhoFootrule.BoundaryFormula

← Mathematical handbook

Closed boundary formulas and sharp minimal dispersion #

The arithmetic arc descriptions are converted to the square-root correction in equation (9). The minimal variance is attained at every prescribed mean.

source
theorem Papers.AnsariRockel2026RhoFootrule.right_boundary_closed (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData) :
have k := ↑S.N * (↑S.N + 1); have ell := 1 / (2 * (↑S.N + 1)); have delta := k * S.v ^ 2; have m := ell + delta; upperRho (1 - 3 * m) = 1 - 6 * ell * (2 * m - ell) - 4 * delta * √delta / √k

Equation (9), the right half of each contact interval.

source
theorem Papers.AnsariRockel2026RhoFootrule.left_boundary_closed (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData) :
have k := ↑S.N * (↑S.N + 1); have ell := 1 / (2 * ↑S.N); have delta := k * S.v ^ 2; have m := ell - delta; upperRho (1 - 3 * m) = 1 - 6 * ell * (2 * m - ell) - 4 * delta * √delta / √k

Equation (9), the left half of each contact interval.

source
noncomputable def Papers.AnsariRockel2026RhoFootrule.minimumVariance (m : ℝ) :
ℝ

The variance correction as determined by the now verified sharp boundary.

Equations
Instances For
    source
    theorem Papers.AnsariRockel2026RhoFootrule.sharp_second_moment (C : ProbabilityTheory.Copula 2) :
    have m := ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure; m ^ 2 + minimumVariance m ≤ ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂C.toMeasure

    Proposition 1.6(i): the sharp improvement over the elementary second-moment bound.

    source
    theorem Papers.AnsariRockel2026RhoFootrule.minimum_variance_attained {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) :
    ∃ (C : ProbabilityTheory.Copula 2), ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure = m ∧ ∫ (x : Fin 2 → ↑unitInterval), (|↑(x 0) - ↑(x 1)| - m) ^ 2 ∂C.toMeasure = minimumVariance m

    Proposition 1.6(ii): the sharp variance exists and is attained for every mean in [0,1/2].

    source
    theorem Papers.AnsariRockel2026RhoFootrule.minimum_variance_nonneg {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) :
    0 ≤ minimumVariance m

    The correction is nonnegative on its full admissible domain.

    source
    theorem Papers.AnsariRockel2026RhoFootrule.right_variance_closed (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData) :
    have k := ↑S.N * (↑S.N + 1); have delta := k * S.v ^ 2; minimumVariance (1 / (2 * (↑S.N + 1)) + delta) = 2 * delta * √delta / (3 * √k) - delta ^ 2

    Exact square-root correction, right half.

    source
    theorem Papers.AnsariRockel2026RhoFootrule.left_variance_closed (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData) :
    have k := ↑S.N * (↑S.N + 1); have delta := k * S.v ^ 2; minimumVariance (1 / (2 * ↑S.N) - delta) = 2 * delta * √delta / (3 * √k) - delta ^ 2

    Exact square-root correction, left half.