Flashlight transformation in Lean 4

A Lean 4 / Mathlib formalization of the theorem on the flashlight transformation of copulas from

A. Onken, S. Grünewälder, M. H. J. Munk, K. Obermayer (2009). Analyzing Short-Term Noise Dependencies of Spike-Counts in Macaque Prefrontal Cortex Using Copulas and the Flashlight Transformation. PLoS Computational Biology 5(11): e1000577. https://doi.org/10.1371/journal.pcbi.1000577

The informal proof is given in the supplementary Text S1.

The theorem

Let C be a d-copula that is the distribution function of a random vector U on [0,1]^d, and let S ⊆ {1, …, d}. Then the flashlight transformation

C^F_S(u) := P((⋂_{i ∈ S} {U_i > 1 - u_i}) ∩ (⋂_{i ∉ S} {U_i ≤ u_i}))

is again a copula, and

C^F_S(u) = ∑_{A ⊆ S} (-1)^|A| C(κ_{S,A}(1, u), …, κ_{S,A}(d, u)),

where κ_{S,A}(i, u) is 1 - u_i for i ∈ A, 1 for i ∈ S \ A, and u_i for i ∉ S.

In Lean, this is Flashlight.flashlight in Flashlight.lean:

theorem flashlight (μ : Measure (ι → ℝ)) [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)

The index set {1, …, d} is modelled by an arbitrary finite type ι. IsCopula requires the function to be grounded, to have uniform margins and to be d-increasing on [0,1]^ι.

Proof structure

The formalization follows the proof in Text S1:

• Lemma (restrictMeasure): P^A := P(• ∩ A) is a measure.
• Flashlight formula (flashlightMeasure_eq_flashlightSum): a calc chain.
• Copula properties (isCopula_flashlightSum): groundedness, uniform margins, and d-increasing property.

One step of the original proof is made explicit. Identifying P_U((⋂_{i ∈ A} {U_i ≤ 1 - u_i}) ∩ (⋂_{i ∈ S̄} {U_i ≤ u_i})) with C(κ_{S,A}(1, u), …) replaces the events {U_i ≤ 1}, i ∈ S \ A, by the whole space. This is justified in measure_compl_le_one_eq_zero and measureReal_eq_kappa: since C(1, …, 1) = 1, the event ⋂_i {U_i ≤ 1} has probability one.

The proof uses no axioms beyond the standard ones (propext, Classical.choice, Quot.sound).

Building

Install Lean via elan, then run:

git clone https://github.com/asnelt/flashlight.git
cd flashlight
lake exe cache get
lake build

Documentation

The API documentation is generated by CI and published at https://asnelt.github.io/flashlight/docs.

Citation

If you use this formalization, please cite the original paper (see CITATION.cff).

License

Apache License 2.0