Documentation

Copula.KendallDistribution

← Copula mathematical handbook

Kendall distributions #

The Kendall distribution is the law of C(U) when U has copula C. It is defined in every finite dimension, including zero. Its CDF uses closed lower intervals, so an atom at zero is retained (as for countermonotonicity).

source
noncomputable def ProbabilityTheory.Copula.kendallDistribution {d : ℕ} (C : Copula d) :
MeasureTheory.ProbabilityMeasure ℝ

The probability law of the copula CDF evaluated at a draw from the copula.

Equations
Instances For
    source
    @[simp]
    theorem ProbabilityTheory.Copula.toMeasure_kendallDistribution {d : ℕ} (C : Copula d) :
    ↑C.kendallDistribution = MeasureTheory.Measure.map C.cdf C.toMeasure
    source
    noncomputable def ProbabilityTheory.Copula.kendallCDF {d : ℕ} (C : Copula d) :
    ℝ → ℝ

    Kendall's distribution function K_C(t) = P(C(U) ≤ t).

    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.kendallCDF_eq {d : ℕ} (C : Copula d) (t : ℝ) :
      C.kendallCDF t = C.toMeasure.real {x : Fin d → ↑unitInterval | C.cdf x ≤ t}
      source
      theorem ProbabilityTheory.Copula.kendallCDF_nonneg {d : ℕ} (C : Copula d) (t : ℝ) :
      0 ≤ C.kendallCDF t
      source
      theorem ProbabilityTheory.Copula.kendallCDF_le_one {d : ℕ} (C : Copula d) (t : ℝ) :
      C.kendallCDF t ≤ 1
      source
      theorem ProbabilityTheory.Copula.monotone_kendallCDF {d : ℕ} (C : Copula d) :
      Monotone C.kendallCDF
      source
      theorem ProbabilityTheory.Copula.right_continuous_kendallCDF {d : ℕ} (C : Copula d) (t : ℝ) :
      ContinuousWithinAt C.kendallCDF (Set.Ici t) t
      source
      theorem ProbabilityTheory.Copula.kendallCDF_of_neg {d : ℕ} (C : Copula d) {t : ℝ} (ht : t < 0) :
      C.kendallCDF t = 0
      source
      theorem ProbabilityTheory.Copula.kendallCDF_of_one_le {d : ℕ} (C : Copula d) {t : ℝ} (ht : 1 ≤ t) :
      C.kendallCDF t = 1
      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallCDF_one {d : ℕ} (C : Copula d) :
      C.kendallCDF 1 = 1
      source
      theorem ProbabilityTheory.Copula.le_kendallCDF {d : ℕ} [NeZero d] (C : Copula d) (t : ↑unitInterval) :
      ↑t ≤ C.kendallCDF ↑t

      A nonempty copula's Kendall distribution stochastically lies below uniform.

      source
      theorem ProbabilityTheory.Copula.integral_kendallDistribution {d : ℕ} (C : Copula d) (f : ℝ → ℝ) (hf : Measurable f) :
      ∫ (t : ℝ), f t ∂↑C.kendallDistribution = ∫ (x : Fin d → ↑unitInterval), f (C.cdf x) ∂C.toMeasure

      Integration against the Kendall law is integration of the CDF transform.

      source
      theorem ProbabilityTheory.Copula.kendallTau_eq_integral_kendallDistribution (C : Copula 2) :
      C.kendallTau = 4 * ∫ (t : ℝ), t ∂↑C.kendallDistribution - 1
      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallDistribution_comonotonic {d : ℕ} [NeZero d] :
      ↑(comonotonic d).kendallDistribution = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ↑u) MeasureTheory.volume
      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallCDF_comonotonic {d : ℕ} [NeZero d] (t : ↑unitInterval) :
      (comonotonic d).kendallCDF ↑t = ↑t
      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallDistribution_dim_zero (C : Copula 0) :
      ↑C.kendallDistribution = MeasureTheory.Measure.dirac 1

      Dimension zero gives the constant CDF value one, rather than a uniform Kendall law.

      source
      theorem ProbabilityTheory.Copula.integral_pow_kendallDistribution_independence (d n : ℕ) :
      ∫ (t : ℝ), t ^ n ∂↑(independence d).kendallDistribution = (1 / (↑n + 1)) ^ d

      All natural moments of the independent copula's Kendall law, including dimension zero.

      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallDistribution_countermonotonic :
      ↑countermonotonic.kendallDistribution = MeasureTheory.Measure.dirac 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallCDF_countermonotonic (t : ↑unitInterval) :
      countermonotonic.kendallCDF ↑t = 1

      Countermonotonicity has an atom of mass one at zero, not K_W(0) = 0.

      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallDistribution_transpose (C : Copula 2) :
      C.transpose.kendallDistribution = C.kendallDistribution
      source
      @[simp]
      theorem ProbabilityTheory.Copula.kendallCDF_transpose (C : Copula 2) :
      C.transpose.kendallCDF = C.kendallCDF