The flashlight transformation of a copula

This file formalizes the following theorem and its proof:

Theorem. Let C_α be a d-copula, I := {1, …, d}, S ⊆ I, P_U(⋂_{i ∈ I} {U_i ≤ u_i}) := C_α(u) a measure, and C^F_{α,S}(u) := P_U((⋂_{i ∈ S} {U_i > 1 - u_i}) ∩ (⋂_{i ∈ S̄} {U_i ≤ u_i})). Then C^F_{α,S} is a d-copula and can be expressed as C^F_{α,S}(u) = ∑_{A ⊆ S} (-1)^|A| C_α(κ_{S,A}(1, u), …, κ_{S,A}(d, u)), where S̄ = I \ S and κ_{S,A}(i, u) is 1 - u_i if i ∈ A, 1 if i ∈ S \ A and u_i if i ∈ S̄.

Formalization notes

• The index set I = {1, …, d} is modelled by an arbitrary finite type ι, and P_U by a probability measure μ on ι → ℝ whose distribution function agrees with C_α on [0,1]^ι.
• A corner z ∈ ×_{i=1}^d {u_i, v_i} of a box B = ×_{i=1}^d [u_i, v_i] is indexed by the set s of coordinates with z_k = v_k, i.e. z = s.piecewise v u. Then N_I(z, u, v) = |sᶜ|, the number of coordinates at the lower bound.
• The sieve formula for measures [Comtet1974] is not available in Mathlib and is proved below.
• The step P_U((⋂_{i ∈ A} {U_i ≤ 1 - u_i}) ∩ (⋂_{i ∈ S̄} {U_i ≤ u_i})) = C_α(κ_{S,A}(1, u), …) implicitly replaces the events {U_i ≤ 1} for i ∈ S \ A by the whole space. This is justified here explicitly: since C_α(1, …, 1) = 1, the event ⋂_{i ∈ I} {U_i ≤ 1} has probability one, so intersecting with it does not change any probability.

References

• Text S1 (proof of the theorem): https://doi.org/10.1371/journal.pcbi.1000577.s001
• The paper: https://doi.org/10.1371/journal.pcbi.1000577
• [Comtet1974] L. Comtet, Advanced Combinatorics, D. Reidel Publishing Company, 1974.

The lemma

noncomputable def Flashlight.restrictMeasure {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (A : Set Ω) (hA : MeasurableSet A) : MeasureTheory.Measure Ω

Lemma. Let (Ω, 𝓕, P) be a probability space with A ∈ 𝓕. Then P^A := P(• ∩ A) is a measure on 𝓕.

Equations

• Flashlight.restrictMeasure P A hA = MeasureTheory.Measure.ofMeasurable (fun (E : Set Ω) (x : MeasurableSet E) => P (E ∩ A)) ⋯ ⋯

theorem Flashlight.restrictMeasure_apply {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {A : Set Ω} (hA : MeasurableSet A) {E : Set Ω} (hE : MeasurableSet E) : (restrictMeasure P A hA) E = P (E ∩ A)

theorem Flashlight.restrictMeasure_real_apply {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {A : Set Ω} (hA : MeasurableSet A) {E : Set Ω} (hE : MeasurableSet E) : (restrictMeasure P A hA).real E = P.real (E ∩ A)

instance Flashlight.instIsFiniteMeasureRestrictMeasure {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] {A : Set Ω} (hA : MeasurableSet A) : MeasureTheory.IsFiniteMeasure (restrictMeasure P A hA)

The sieve formula for finite measures [Comtet1974]

theorem Flashlight.measureReal_inter_biInter_compl {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [DecidableEq ι] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] (E : ι → Set Ω) (hE : ∀ (i : ι), MeasurableSet (E i)) (S : Finset ι) {F : Set Ω} (hF : MeasurableSet F) : ν.real (F ∩ ⋂ i ∈ S, (E i)ᶜ) = ∑ A ∈ S.powerset, (-1) ^ A.card * ν.real (F ∩ ⋂ i ∈ A, E i)

Inclusion–exclusion, complement form.

theorem Flashlight.sum_range_succ_neg_one_pow (g : ℕ → ℝ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (-1) ^ k * g k = g 0 - ∑ k ∈ Finset.Icc 1 n, (-1) ^ (k - 1) * g k

theorem Flashlight.measureReal_biUnion_sieve {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [DecidableEq ι] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] (E : ι → Set Ω) (hE : ∀ (i : ι), MeasurableSet (E i)) (S : Finset ι) : ν.real (⋃ i ∈ S, E i) = ∑ k ∈ Finset.Icc 1 S.card, (-1) ^ (k - 1) * ∑ A ∈ Finset.powersetCard k S, ν.real (⋂ i ∈ A, E i)

Sieve formula (inclusion–exclusion principle) for finite measures: ν(⋃_{i ∈ S} E_i) = ∑_{k=1}^{|S|} (-1)^{k-1} ∑_{A ⊆ S, |A| = k} ν(⋂_{i ∈ A} E_i).

Copulas

def Flashlight.unitCube (ι : Type u_2) : Set (ι → ℝ)

The unit cube [0,1]^ι.

Equations

• Flashlight.unitCube ι = {u : ι → ℝ | ∀ (i : ι), u i ∈ Set.Icc 0 1}

def Flashlight.boxVolume {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : (ι → ℝ) → ℝ) (u v : ι → ℝ) : ℝ

V_C(B) = ∑_{z ∈ ×_{i=1}^d {u_i, v_i}} (-1)^{N_I(z, u, v)} C(z) for the box B = ×_{i=1}^d [u_i, v_i], where the corner z = s.piecewise v u takes the value v_k for k ∈ s and u_k otherwise, so that N_I(z, u, v) = |sᶜ|.

Equations

• Flashlight.boxVolume C u v = ∑ s : Finset ι, (-1) ^ sᶜ.card * C (s.piecewise v u)

structure Flashlight.IsCopula {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : (ι → ℝ) → ℝ) : Prop

C is a d-copula (only its values on [0,1]^ι matter).

• grounded (u : ι → ℝ) : u ∈ unitCube ι → (∃ (i : ι), u i = 0) → C u = 0

  C is grounded.

• margins (i : ι) (t : ℝ) : t ∈ Set.Icc 0 1 → C (Function.update 1 i t) = t

  C has uniform margins.

• increasing (u : ι → ℝ) : u ∈ unitCube ι → ∀ v ∈ unitCube ι, u ≤ v → 0 ≤ boxVolume C u v

  C is d-increasing.

The objects of the theorem

def Flashlight.kappa {ι : Type u_1} [DecidableEq ι] (S A : Finset ι) (u : ι → ℝ) : ι → ℝ

κ_{S,A}(i, u) is 1 - u_i if i ∈ A, 1 if i ∈ S \ A and u_i if i ∈ S̄.

Equations

• Flashlight.kappa S A u i = if i ∈ A then 1 - u i else if i ∈ S then 1 else u i

def Flashlight.flashlightSum {ι : Type u_1} [DecidableEq ι] (C : (ι → ℝ) → ℝ) (S : Finset ι) (u : ι → ℝ) : ℝ

The right-hand side of the flashlight formula, ∑_{A ⊆ S} (-1)^|A| C_α(κ_{S,A}(1, u), …, κ_{S,A}(d, u)).

Equations

• Flashlight.flashlightSum C S u = ∑ A ∈ S.powerset, (-1) ^ A.card * C (Flashlight.kappa S A u)

def Flashlight.flashlightMeasure {ι : Type u_1} (μ : MeasureTheory.Measure (ι → ℝ)) (S : Finset ι) (u : ι → ℝ) : ℝ

C^F_{α,S}(u) := P_U((⋂_{i ∈ S} {U_i > 1 - u_i}) ∩ (⋂_{i ∈ S̄} {U_i ≤ u_i})).

Equations

• Flashlight.flashlightMeasure μ S u = μ.real {x : ι → ℝ | (∀ i ∈ S, 1 - u i < x i) ∧ ∀ i ∉ S, x i ≤ u i}

Elementary lemmas

theorem Flashlight.one_mem_Icc : 1 ∈ Set.Icc 0 1

theorem Flashlight.one_sub_mem_Icc {t : ℝ} (ht : t ∈ Set.Icc 0 1) : 1 - t ∈ Set.Icc 0 1

theorem Flashlight.one_mem_unitCube {ι : Type u_1} [Fintype ι] [DecidableEq ι] : 1 ∈ unitCube ι

theorem Flashlight.update_mem_unitCube {ι : Type u_1} [Fintype ι] [DecidableEq ι] {u : ι → ℝ} (hu : u ∈ unitCube ι) (a : ι) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : Function.update u a t ∈ unitCube ι

theorem Flashlight.piecewise_mem_unitCube {ι : Type u_1} [Fintype ι] [DecidableEq ι] {u v : ι → ℝ} (hu : u ∈ unitCube ι) (hv : v ∈ unitCube ι) (s : Finset ι) : s.piecewise v u ∈ unitCube ι

theorem Flashlight.kappa_mem_unitCube {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S A : Finset ι) {u : ι → ℝ} (hu : u ∈ unitCube ι) : kappa S A u ∈ unitCube ι

theorem Flashlight.IsCopula.congr {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C D : (ι → ℝ) → ℝ} (hC : IsCopula C) (h : ∀ u ∈ unitCube ι, C u = D u) : IsCopula D

Being a copula only depends on the values on the unit cube.

theorem Flashlight.IsCopula.apply_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : (ι → ℝ) → ℝ} (hC : IsCopula C) [Nonempty ι] : C 1 = 1

The flashlight formula

theorem Flashlight.measure_compl_le_one_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] {C : (ι → ℝ) → ℝ} (hC : IsCopula C) (hμ : ∀ u ∈ unitCube ι, C u = μ.real {x : ι → ℝ | ∀ (i : ι), x i ≤ u i}) : μ {x : ι → ℝ | ∀ (i : ι), x i ≤ 1}ᶜ = 0

The event ⋂_{i ∈ I} {U_i ≤ 1} has probability one, because P_U(⋂_{i ∈ I} {U_i ≤ 1}) = C_α(1, …, 1) = 1. This justifies replacing the events {U_i ≤ 1} by the whole space.

theorem Flashlight.measureReal_eq_kappa {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] {C : (ι → ℝ) → ℝ} (hC : IsCopula C) (hμ : ∀ u ∈ unitCube ι, C u = μ.real {x : ι → ℝ | ∀ (i : ι), x i ≤ u i}) {S A : Finset ι} (hAS : A ⊆ S) {u : ι → ℝ} (hu : u ∈ unitCube ι) : μ.real ((⋂ i ∈ A, {x : ι → ℝ | x i ≤ 1 - u i}) ∩ {x : ι → ℝ | ∀ i ∉ S, x i ≤ u i}) = C (kappa S A u)

P_U((⋂_{i ∈ A} {U_i ≤ 1 - u_i}) ∩ (⋂_{i ∈ S̄} {U_i ≤ u_i})) = C_α(κ_{S,A}(1, u), …, κ_{S,A}(d, u)). The event on the left-hand side does not contain the conditions U_i ≤ κ_{S,A}(i, u) = 1 for i ∈ S \ A, but these hold almost surely by measure_compl_le_one_eq_zero.

theorem Flashlight.flashlightMeasure_eq_flashlightSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] {C : (ι → ℝ) → ℝ} (hC : IsCopula C) (hμ : ∀ u ∈ unitCube ι, C u = μ.real {x : ι → ℝ | ∀ (i : ι), x i ≤ u i}) (S : Finset ι) {u : ι → ℝ} (hu : u ∈ unitCube ι) : flashlightMeasure μ S u = flashlightSum C S u

The flashlight formula C^F_{α,S}(u) = ∑_{A ⊆ S} (-1)^|A| C_α(κ_{S,A}(1, u), …).

C^F_{α,S} is a copula

def Flashlight.chi {ι : Type u_1} [DecidableEq ι] (A : Finset ι) (i : ι) : ℝ

χ_A(i) is 1 if i ∈ A and 0 if i ∉ A.

Equations

• Flashlight.chi A i = if i ∈ A then 1 else 0

def Flashlight.psi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (z : ι → ℝ) : ι → ℝ

ψ_S(z_k) := χ_S(k)(1 - z_k) + χ_{S̄}(k)(z_k).

Equations

• Flashlight.psi S z k = Flashlight.chi S k * (1 - z k) + Flashlight.chi Sᶜ k * z k

theorem Flashlight.kappa_self_eq_psi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (z : ι → ℝ) : kappa S S z = psi S z

theorem Flashlight.psi_mem_unitCube {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) {z : ι → ℝ} (hz : z ∈ unitCube ι) : psi S z ∈ unitCube ι

theorem Flashlight.neg_one_pow_card_compl_insert {ι : Type u_1} [Fintype ι] [DecidableEq ι] {a : ι} {t : Finset ι} (ha : a ∉ t) : (-1) ^ (insert a t)ᶜ.card = -(-1) ^ tᶜ.card

A corner z with z_{s_A} = v_{s_A} and the corner with z_{s_A} = u_{s_A} have opposite signs: (-1)^{N_I(z, u, v) - 1} and (-1)^{N_I(z, u, v)}.

theorem Flashlight.neg_one_pow_card_compl_symmDiff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s S : Finset ι) : (-1) ^ (symmDiff s S)ᶜ.card = (-1) ^ sᶜ.card * (-1) ^ S.card

(7): (-1)^{N_I(ψ_S(z), ψ_S(u), ψ_S(v))} = (-1)^{N_I(z, u, v)} (-1)^{|S|}.

theorem Flashlight.isCopula_flashlightSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : (ι → ℝ) → ℝ} (hC : IsCopula C) (S : Finset ι) : IsCopula (flashlightSum C S)

Theorem. C^F_{α,S} (here in the form of the right-hand side of the flashlight formula) is a d-copula.

theorem Flashlight.flashlight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsProbabilityMeasure μ] {C : (ι → ℝ) → ℝ} (hC : IsCopula C) (hμ : ∀ u ∈ unitCube ι, C u = μ.real {x : ι → ℝ | ∀ (i : ι), x i ≤ u i}) (S : Finset ι) : IsCopula (flashlightMeasure μ S) ∧ ∀ u ∈ unitCube ι, flashlightMeasure μ S u = ∑ A ∈ S.powerset, (-1) ^ A.card * C (kappa S A u)

Theorem. Let C_α be a d-copula, S ⊆ I and P_U a probability measure with P_U(⋂_{i ∈ I} {U_i ≤ u_i}) = C_α(u) for u ∈ [0,1]^d. Then C^F_{α,S} is a d-copula and C^F_{α,S}(u) = ∑_{A ⊆ S} (-1)^|A| C_α(κ_{S,A}(1, u), …, κ_{S,A}(d, u)) for u ∈ [0,1]^d.