Documentation

Copula.Countermonotonic

← Mathematical handbook

The bivariate countermonotonic copula #

The law of (U, 1-U) for a uniform U attains the bivariate lower Fréchet–Hoeffding bound. No higher-dimensional version of that bound is asserted.

source
noncomputable def ProbabilityTheory.Copula.countermonotonic :
Copula 2

The law of a uniform variable paired with its reflection.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem ProbabilityTheory.Copula.toMeasure_countermonotonic :
    countermonotonic.toMeasure = MeasureTheory.Measure.map (fun (t : ↑unitInterval) => ![t, unitInterval.symm t]) MeasureTheory.volume
    source
    theorem ProbabilityTheory.Copula.reflect_comonotonic_eq_countermonotonic :
    (comonotonic 2).reflect {1} = countermonotonic

    Countermonotonicity is obtained by reflecting one coordinate of the diagonal law.

    source
    @[simp]
    theorem ProbabilityTheory.Copula.cdf_countermonotonic (u : Fin 2 → ↑unitInterval) :
    countermonotonic.cdf u = max 0 (↑(u 0) + ↑(u 1) - 1)

    The lower Fréchet–Hoeffding bound is attained in dimension two.