Documentation

Copula.OrdinalSum.Basic

← Copula mathematical handbook

Binary ordinal sums of bivariate copulas #

The first copula occupies [0,a]², the second occupies [a,1]², and the CDF on the two off-diagonal rectangles is min(u,v). The construction includes a=0 and a=1. See Nelsen, second edition, §3.2.2.

source
@[simp]
theorem ProbabilityTheory.Copula.cdf_two_zero_right (C : Copula 2) (u : ↑unitInterval) :
C.cdf ![u, 0] = 0
source
noncomputable def ProbabilityTheory.Copula.ordinalSumCDF (C D : Copula 2) (a u v : ↑unitInterval) :
ℝ

An endpoint-safe expression for the ordinal-sum CDF.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ProbabilityTheory.Copula.isClassical_ordinalSumCDF (C D : Copula 2) (a : ↑unitInterval) :
    IsClassical fun (u : Fin 2 → ↑unitInterval) => C.ordinalSumCDF D a (u 0) (u 1)
    source
    noncomputable def ProbabilityTheory.Copula.ordinalSum (C D : Copula 2) (a : ↑unitInterval) :
    Copula 2

    Place C below the split a and D above it, with perfectly ordered block labels.

    Equations
    Instances For
      source
      @[simp]
      theorem ProbabilityTheory.Copula.cdf_ordinalSum (C D : Copula 2) (a : ↑unitInterval) (u : Fin 2 → ↑unitInterval) :
      (C.ordinalSum D a).cdf u = C.ordinalSumCDF D a (u 0) (u 1)
      source
      @[simp]
      theorem ProbabilityTheory.Copula.ordinalSum_zero (C D : Copula 2) :
      C.ordinalSum D 0 = D
      source
      @[simp]
      theorem ProbabilityTheory.Copula.ordinalSum_one (C D : Copula 2) :
      C.ordinalSum D 1 = C
      source
      theorem ProbabilityTheory.Copula.cdf_ordinalSum_lower (C D : Copula 2) (a u v : ↑unitInterval) (hu : u ≤ a) (hv : v ≤ a) :
      (C.ordinalSum D a).cdf ![u, v] = ↑a * C.cdf ![OrdinalSum.lowerCoord a u, OrdinalSum.lowerCoord a v]
      source
      theorem ProbabilityTheory.Copula.cdf_ordinalSum_upper (C D : Copula 2) (a u v : ↑unitInterval) (hu : a ≤ u) (hv : a ≤ v) :
      (C.ordinalSum D a).cdf ![u, v] = ↑a + (1 - ↑a) * D.cdf ![OrdinalSum.upperCoord a u, OrdinalSum.upperCoord a v]
      source
      theorem ProbabilityTheory.Copula.cdf_ordinalSum_lower_upper (C D : Copula 2) (a u v : ↑unitInterval) (hu : u ≤ a) (hv : a ≤ v) :
      (C.ordinalSum D a).cdf ![u, v] = ↑u
      source
      theorem ProbabilityTheory.Copula.cdf_ordinalSum_upper_lower (C D : Copula 2) (a u v : ↑unitInterval) (hu : a ≤ u) (hv : v ≤ a) :
      (C.ordinalSum D a).cdf ![u, v] = ↑v
      source
      @[simp]
      theorem ProbabilityTheory.Copula.cdf_ordinalSum_split (C D : Copula 2) (a : ↑unitInterval) :
      (C.ordinalSum D a).cdf ![a, a] = ↑a
      source
      theorem ProbabilityTheory.Copula.cdf_ordinalSum_lowerEmbed (C D : Copula 2) (a u v : ↑unitInterval) (ha : 0 < a) :
      (C.ordinalSum D a).cdf ![OrdinalSum.lowerEmbed a u, OrdinalSum.lowerEmbed a v] = ↑a * C.cdf ![u, v]
      source
      theorem ProbabilityTheory.Copula.cdf_ordinalSum_upperEmbed (C D : Copula 2) (a u v : ↑unitInterval) (ha : a < 1) :
      (C.ordinalSum D a).cdf ![OrdinalSum.upperEmbed a u, OrdinalSum.upperEmbed a v] = ↑a + (1 - ↑a) * D.cdf ![u, v]