Documentation

Copula.Information

← Copula mathematical handbook

Copula information and entropy #

Copula information is KL divergence from the independent uniform law. In two dimensions it is mutual information; in higher dimensions it is total correlation. Values lie in ℝ≥0∞, so singular dependence is not silently converted to a finite real number. Copula entropy is its negative in EReal. The logarithm convention is natural logarithms (information in nats).

source
noncomputable def ProbabilityTheory.Copula.copulaInformation {d : ℕ} (C : Copula d) :
ENNReal

Relative entropy of the copula law with respect to independent uniforms.

Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.copulaEntropy {d : ℕ} (C : Copula d) :
    EReal

    Extended copula entropy. Infinite information gives entropy -∞.

    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.copulaInformation_eq_zero_iff {d : ℕ} (C : Copula d) :
      C.copulaInformation = 0 ↔ C = independence d
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaInformation_independence (d : ℕ) :
      (independence d).copulaInformation = 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaEntropy_independence (d : ℕ) :
      (independence d).copulaEntropy = 0
      source
      theorem ProbabilityTheory.Copula.copulaEntropy_nonpos {d : ℕ} (C : Copula d) :
      C.copulaEntropy ≤ 0
      source
      theorem ProbabilityTheory.Copula.copulaEntropy_eq_zero_iff {d : ℕ} (C : Copula d) :
      C.copulaEntropy = 0 ↔ C = independence d
      source
      theorem ProbabilityTheory.Copula.copulaInformation_ne_top_iff {d : ℕ} (C : Copula d) :
      C.copulaInformation ≠ ⊤ ↔ C.toMeasure.AbsolutelyContinuous (independence d).toMeasure ∧ MeasureTheory.Integrable (MeasureTheory.llr C.toMeasure (independence d).toMeasure) C.toMeasure

      Exact finiteness conditions, including integrability of the log-likelihood ratio.

      source
      theorem ProbabilityTheory.Copula.copulaInformation_eq_top_of_not_ac {d : ℕ} (C : Copula d) (h : ¬C.toMeasure.AbsolutelyContinuous (independence d).toMeasure) :
      C.copulaInformation = ⊤
      source
      theorem ProbabilityTheory.Copula.copulaInformation_eq_integral {d : ℕ} (C : Copula d) (hac : C.toMeasure.AbsolutelyContinuous (independence d).toMeasure) (hi : MeasureTheory.Integrable (MeasureTheory.llr C.toMeasure (independence d).toMeasure) C.toMeasure) :
      C.copulaInformation = ENNReal.ofReal (∫ (x : Fin d → ↑unitInterval), MeasureTheory.llr C.toMeasure (independence d).toMeasure x ∂C.toMeasure)

      The finite integral formula, with the two probability-mass correction terms cancelled.

      source
      theorem ProbabilityTheory.Copula.copulaInformation_eq_lintegral_density {d : ℕ} (C : Copula d) (hac : C.toMeasure.AbsolutelyContinuous (independence d).toMeasure) :
      C.copulaInformation = ∫⁻ (x : Fin d → ↑unitInterval), ENNReal.ofReal (InformationTheory.klFun (C.toMeasure.rnDeriv (independence d).toMeasure x).toReal) ∂(independence d).toMeasure

      A nonnegative density-integral representation, also valid for infinite information. Here klFun c = c * log c + 1 - c and the density is the Radon–Nikodym derivative.

      source
      theorem ProbabilityTheory.Copula.copulaInformation_rearrange_le {d : ℕ} (C : Copula d) (f : Fin d → ↑unitInterval → ↑unitInterval) (hf : ∀ (i : Fin d), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) :
      (C.rearrange f hf).copulaInformation ≤ C.copulaInformation

      Coordinatewise processing preserving uniform margins cannot increase information.

      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaInformation_shuffle (C : Copula 2) (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) :
      (C.shuffle e he).copulaInformation = C.copulaInformation
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaEntropy_shuffle (C : Copula 2) (e : ↑unitInterval ≃ᵐ ↑unitInterval) (he : MeasureTheory.MeasurePreserving (⇑e) MeasureTheory.volume MeasureTheory.volume) :
      (C.shuffle e he).copulaEntropy = C.copulaEntropy
      source
      theorem ProbabilityTheory.Copula.volume_cube_graph {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) :
      MeasureTheory.volume {x : Fin 2 → ↑unitInterval | x 1 = f (x 0)} = 0

      A measurable graph has zero independent bivariate uniform probability.

      source
      theorem ProbabilityTheory.Copula.IsCompletelyDependent.copulaInformation_eq_top {C : Copula 2} (h : C.IsCompletelyDependent) :
      C.copulaInformation = ⊤

      Every completely dependent bivariate copula has infinite mutual information.

      source
      theorem ProbabilityTheory.Copula.IsCompletelyDependent.copulaEntropy_eq_bot {C : Copula 2} (h : C.IsCompletelyDependent) :
      C.copulaEntropy = ⊥
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaInformation_comonotonic :
      (comonotonic 2).copulaInformation = ⊤
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaInformation_countermonotonic :
      countermonotonic.copulaInformation = ⊤
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaEntropy_comonotonic :
      (comonotonic 2).copulaEntropy = ⊥
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaEntropy_countermonotonic :
      countermonotonic.copulaEntropy = ⊥
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaInformation_dim_zero (C : Copula 0) :
      C.copulaInformation = 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.copulaInformation_dim_one (C : Copula 1) :
      C.copulaInformation = 0