Documentation

Copula.Diagonal

← Copula mathematical handbook

Diagonal sections of bivariate copulas #

Necessary diagonal conditions and the characterization of the upper Fréchet copula by its diagonal (Nelsen, second edition, §3.2.6 and Exercise 2.8).

source
noncomputable def ProbabilityTheory.Copula.diagonal (C : Copula 2) (t : ↑unitInterval) :
ℝ

The diagonal section of a bivariate copula.

Equations
Instances For
    source
    @[simp]
    theorem ProbabilityTheory.Copula.diagonal_zero (C : Copula 2) :
    C.diagonal 0 = 0
    source
    @[simp]
    theorem ProbabilityTheory.Copula.diagonal_one (C : Copula 2) :
    C.diagonal 1 = 1
    source
    theorem ProbabilityTheory.Copula.diagonal_nonneg (C : Copula 2) (t : ↑unitInterval) :
    0 ≤ C.diagonal t
    source
    theorem ProbabilityTheory.Copula.diagonal_le (C : Copula 2) (t : ↑unitInterval) :
    C.diagonal t ≤ ↑t
    source
    theorem ProbabilityTheory.Copula.diagonal_lower_bound (C : Copula 2) (t : ↑unitInterval) :
    max 0 (2 * ↑t - 1) ≤ C.diagonal t
    source
    theorem ProbabilityTheory.Copula.monotone_diagonal (C : Copula 2) :
    Monotone C.diagonal
    source
    theorem ProbabilityTheory.Copula.abs_diagonal_sub_le (C : Copula 2) (s t : ↑unitInterval) :
    |C.diagonal s - C.diagonal t| ≤ 2 * |↑s - ↑t|
    source
    theorem ProbabilityTheory.Copula.lipschitzWith_diagonal (C : Copula 2) :
    LipschitzWith 2 C.diagonal
    source
    theorem ProbabilityTheory.Copula.continuous_diagonal (C : Copula 2) :
    Continuous C.diagonal
    source
    theorem ProbabilityTheory.Copula.diagonal_sub_mem_Icc (C : Copula 2) {s t : ↑unitInterval} (h : s ≤ t) :
    C.diagonal t - C.diagonal s ∈ Set.Icc 0 (2 * (↑t - ↑s))
    source
    @[simp]
    theorem ProbabilityTheory.Copula.diagonal_independence (t : ↑unitInterval) :
    (independence 2).diagonal t = ↑t ^ 2
    source
    @[simp]
    theorem ProbabilityTheory.Copula.diagonal_comonotonic (t : ↑unitInterval) :
    (comonotonic 2).diagonal t = ↑t
    source
    @[simp]
    theorem ProbabilityTheory.Copula.diagonal_countermonotonic (t : ↑unitInterval) :
    countermonotonic.diagonal t = max 0 (2 * ↑t - 1)
    source
    theorem ProbabilityTheory.Copula.diagonal_eq_id_iff (C : Copula 2) :
    (∀ (t : ↑unitInterval), C.diagonal t = ↑t) ↔ C = comonotonic 2

    The upper Fréchet copula is determined by its diagonal.

    source
    theorem ProbabilityTheory.Copula.measureReal_max_le (C : Copula 2) (t : ↑unitInterval) :
    C.toMeasure.real {x : Fin 2 → ↑unitInterval | max (x 0) (x 1) ≤ t} = C.diagonal t

    The diagonal is the distribution function of the maximum of the two coordinates.

    source
    theorem ProbabilityTheory.Copula.measureReal_min_le (C : Copula 2) (t : ↑unitInterval) :
    C.toMeasure.real {x : Fin 2 → ↑unitInterval | min (x 0) (x 1) ≤ t} = 2 * ↑t - C.diagonal t

    The complementary diagonal formula gives the distribution function of the minimum.