Documentation

Copula.Rank.Region.MeanVariance.Paper.ExactRegion

← Copula mathematical handbook

The full sharp rho-footrule region #

The package supplies arithmetic boundary parameters, actual attaining copulas, and global inequalities. The coefficient order here matches the article. Uniqueness of the optimizing copula is proved in OptimizerUniqueness.lean.

source
@[reducible, inline]
abbrev ProbabilityTheory.Copula.RankRegion.MeanVariance.BoundaryParameter :
Type
Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.MeanVariance.upperRho (p : ℝ) :
    ℝ

    The upper boundary as a scalar function on its valid interval.

    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.upperRho_parameter (a : BoundaryParameter) :
      upperRho (RhoFootrule.UpperParameter.footrule a) = RhoFootrule.UpperParameter.rho a

      The scalar boundary agrees with every explicit arithmetic arc.

      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.boundary_coefficients (a : BoundaryParameter) :
      (RhoFootrule.UpperParameter.copula a).spearmanFootrule = RhoFootrule.UpperParameter.footrule a ∧ (RhoFootrule.UpperParameter.copula a).spearmanRho = RhoFootrule.UpperParameter.rho a

      Both coefficient identities of the constructed boundary copula.

      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.sharp_upper_bound (C : Copula 2) :
      C.spearmanRho ≤ upperRho C.spearmanFootrule

      Global sharp upper bound, valid for singular copulas too.

      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.upper_boundary_attained {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) :
      ∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.spearmanRho = upperRho p

      Every upper-boundary point is attained.

      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.sharp_lower_bound (C : Copula 2) :
      -1 + 2 * √((1 + 2 * C.spearmanFootrule) / 3) ^ 3 ≤ C.spearmanRho

      The known lower boundary, with its exact square-root normalization.

      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.lower_boundary_attained {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) :
      ∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.spearmanRho = -1 + 2 * √((1 + 2 * p) / 3) ^ 3
      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.exact_region (r p : ℝ) :
      (∃ (C : Copula 2), C.spearmanRho = r ∧ C.spearmanFootrule = p) ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ RhoFootrule.lowerBoundary p ≤ r ∧ r ≤ upperRho p

      Corollary 1.2: both directions, in the source's (rho, footrule) order.

      source
      theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.boundary_value_unique (a b : BoundaryParameter) (h : RhoFootrule.UpperParameter.footrule a = RhoFootrule.UpperParameter.footrule b) :
      RhoFootrule.UpperParameter.rho a = RhoFootrule.UpperParameter.rho b

      Arc junctions yield the same boundary value.