Documentation

Copula.OrdinalSum.Components

← Copula mathematical handbook

Extracting the copulas below and above a diagonal cut #

At a diagonal fixed point, restriction to either positive-length square and affine rescaling gives a copula. The lower and upper constructions only require their own block to have positive length.

source
theorem ProbabilityTheory.Copula.OrdinalSum.lowerEmbed_mono (a : ↑unitInterval) :
Monotone (lowerEmbed a)
source
theorem ProbabilityTheory.Copula.OrdinalSum.upperEmbed_mono (a : ↑unitInterval) :
Monotone (upperEmbed a)
source
@[simp]
theorem ProbabilityTheory.Copula.OrdinalSum.lowerEmbed_zero (a : ↑unitInterval) :
lowerEmbed a 0 = 0
source
@[simp]
theorem ProbabilityTheory.Copula.OrdinalSum.lowerEmbed_one (a : ↑unitInterval) :
lowerEmbed a 1 = a
source
@[simp]
theorem ProbabilityTheory.Copula.OrdinalSum.upperEmbed_zero (a : ↑unitInterval) :
upperEmbed a 0 = a
source
@[simp]
theorem ProbabilityTheory.Copula.OrdinalSum.upperEmbed_one (a : ↑unitInterval) :
upperEmbed a 1 = 1
source
theorem ProbabilityTheory.Copula.OrdinalSum.lowerEmbed_lowerCoord (a u : ↑unitInterval) (hu : u ≤ a) :
lowerEmbed a (lowerCoord a u) = u
source
theorem ProbabilityTheory.Copula.OrdinalSum.upperEmbed_upperCoord (a u : ↑unitInterval) (hu : a ≤ u) :
upperEmbed a (upperCoord a u) = u
source
theorem ProbabilityTheory.Copula.isClassical_lowerOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha : C.diagonal a = ↑a) :
IsClassical fun (u : Fin 2 → ↑unitInterval) => C.cdf ![OrdinalSum.lowerEmbed a (u 0), OrdinalSum.lowerEmbed a (u 1)] / ↑a
source
theorem ProbabilityTheory.Copula.isClassical_upperOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha1 : a < 1) (ha : C.diagonal a = ↑a) :
IsClassical fun (u : Fin 2 → ↑unitInterval) => (C.cdf ![OrdinalSum.upperEmbed a (u 0), OrdinalSum.upperEmbed a (u 1)] - ↑a) / (1 - ↑a)
source
noncomputable def ProbabilityTheory.Copula.lowerOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha : C.diagonal a = ↑a) :
Copula 2

Restrict to the lower square at a diagonal cut, then rescale it to the unit square.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.upperOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha1 : a < 1) (ha : C.diagonal a = ↑a) :
    Copula 2

    Restrict to the upper square at a diagonal cut, then rescale it to the unit square.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem ProbabilityTheory.Copula.cdf_lowerOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha : C.diagonal a = ↑a) (u : Fin 2 → ↑unitInterval) :
      (C.lowerOrdinalComponent a ha0 ha).cdf u = C.cdf ![OrdinalSum.lowerEmbed a (u 0), OrdinalSum.lowerEmbed a (u 1)] / ↑a
      source
      @[simp]
      theorem ProbabilityTheory.Copula.cdf_upperOrdinalComponent (C : Copula 2) (a : ↑unitInterval) (ha1 : a < 1) (ha : C.diagonal a = ↑a) (u : Fin 2 → ↑unitInterval) :
      (C.upperOrdinalComponent a ha1 ha).cdf u = (C.cdf ![OrdinalSum.upperEmbed a (u 0), OrdinalSum.upperEmbed a (u 1)] - ↑a) / (1 - ↑a)