Discovery.LiNGAM
Linear non-Gaussian acyclic model identification: permutation uniqueness, generalized-permutation algebra, kurtosis-based column support, and the LiNGAM identifiability theorem.
Kurtosis 3 core · 0 supporting This is the Marcinkiewicz-free route to LiNGAM identifiability. ★ kurt★ cross_fourth_cumulant_eq_sum★ colSupport_of_kurtosis
Kurtosis-based column support for ICA / LiNGAM
This is the Marcinkiewicz-free route to LiNGAM identifiability. Instead of the
general Darmois–Skitovich theorem (which needs Marcinkiewicz), we assume the
sources have non-zero fourth cumulant of one common sign (a standard ICA
assumption: all super-Gaussian or all sub-Gaussian). Then the key column-support
fact Wᵢⱼ · Wₖⱼ = 0 — the input to genPerm_of_det_ne_zero_of_colSupport — follows
from a single fourth-cumulant identity and a sum-of-same-sign argument, with no
characteristic-function functional equation at all.
cross_fourth_cumulant_eq_sum is the multilinear identity
cum(yᵢ,yᵢ,yₖ,yₖ) = Σⱼ Wᵢⱼ² Wₖⱼ² κ₄(eⱼ) for yᵢ = Σⱼ Wᵢⱼ eⱼ with independent
centered sources; colSupport_of_kurtosis combines it with independence of yᵢ, yₖ
(which makes the cross-cumulant vanish) and the same-sign assumption.
Excess kurtosis, the fourth cumulant of a real random variable. For a centered variable X it is E[X⁴] − 3 · (E[X²])²; Gaussian variables have zero excess kurtosis, while LiNGAM's kurtosis route assumes every source has nonzero excess kurtosis of one common sign.
Fourth cross-cumulant identity (Isserlis / cumulant multilinearity). Let e be a family of real sources on a probability space such that each coordinate eⱼ is measurable, the coordinates are mutually independent, each has finite fourth moment, and each is centered. Then for any coefficient vectors a, b and the linear forms yₐ = Σⱼ aⱼ eⱼ, y_b = Σⱼ bⱼ eⱼ, the joint fourth cumulant cum(yₐ,yₐ,y_b,y_b) equals Σⱼ aⱼ² bⱼ² κ₄(eⱼ).
Formal statement
Proof (Lean source)
Kurtosis-based column support. Let e be a family of real sources on a probability space such that each coordinate eⱼ is measurable, the coordinates are mutually independent, each has finite fourth moment, each is centered, and the fourth cumulant (excess kurtosis) of every coordinate is nonzero and of one common sign, all positive or all negative. For two distinct row indices i ≠ k of a mixing matrix W, if the linear forms Σⱼ Wᵢⱼ eⱼ and Σⱼ Wₖⱼ eⱼ are independent, then every column j satisfies Wᵢⱼ · Wₖⱼ = 0. This is the input required by genPerm_of_det_ne_zero_of_colSupport.
Formal statement
Proof (Lean source)
Identifiability 1 core · 0 supporting This is the structural linear-algebra step in the LiNGAM identification argument (Shimizu et al. ★ lingam_identifiable
LiNGAM structural identifiability
This is the structural linear-algebra step in the LiNGAM identification argument (Shimizu et al. 2006): once two coefficient matrices are related by a generalized permutation, acyclicity and unit-diagonal normalization pin the coefficient matrix uniquely.
Write C = I − B for the coefficient matrix of a LiNGAM model x = B x + e
(so x = C⁻¹ e, C has unit diagonal because Bᵢᵢ = 0, and C is lower
triangular in the causal order because B is acyclic). ICA identifiability says
that two observationally-equivalent models have mixing matrices related by a
generalized permutation, i.e. C' = W C with W a permutation composed with a
non-zero diagonal scaling: C' i j = d i · C (τ i) j with d i ≠ 0.
The public theorem lingam_identifiable specializes
Causalean.Mathlib.LinearAlgebra.eq_of_genPerm_triangular_unitDiag to C = I − B.
The kurtosis route in LiNGAMKurtosis.lean supplies the generalized-permutation
relation through column support, so this file isolates the deterministic
acyclicity-and-unit-diagonal pinning step.
LiNGAM coefficient identifiability (modulo ICA). Let B and B' be two n × n real coefficient matrices such that B has zero diagonal, B' has zero diagonal, B is acyclic with respect to a causal order σ: B i j = 0 whenever σ i < σ j, and the matrices I − B and I − B' are related by a generalized permutation — a permutation τ composed with a nonzero diagonal scale d, so (I − B') i j = d i · (I − B) (τ i) j (as delivered by ICA identifiability). Then B equals B'. This packages eq_of_genPerm_triangular_unitDiag for C = I − B.
Formal statement
Proof (Lean source)
LiNGAMKurtosis 2 core · 0 supporting This file assembles a LiNGAM identification theorem under the standard ICA assumption that the disturbances have non-zero fourth cumulant of one common sign (all super-Gaussian or all sub-Gaussian). ★ ica_genPerm_relation★ lingam_identifiability_kurtosis
LiNGAM identification, kurtosis route
This file assembles a LiNGAM identification theorem under the standard ICA assumption that the disturbances have non-zero fourth cumulant of one common sign (all super-Gaussian or all sub-Gaussian). This kurtosis route bypasses the general Darmois–Skitovich theorem and Marcinkiewicz's theorem on entire functions:
* colSupport_of_kurtosis (Kurtosis.lean) supplies the column support Wᵢⱼ·Wₖⱼ = 0
from fourth cumulants instead of from Darmois–Skitovich;
* ica_genPerm_relation (here) is the purely linear-algebraic core: column support plus
invertibility give the generalized permutation relation between A⁻¹ and A'⁻¹;
* eq_of_genPerm_triangular_unitDiag (Mathlib/LinearAlgebra/MonomialMatrix.lean) then forces
A⁻¹ = A'⁻¹.
Let A, A' be n × n real matrices such that A is invertible and A' is invertible. If the matrix A'⁻¹ A has at most one non-zero entry per column — the column-support fact — then there exist a permutation τ and a nowhere-zero scale vector d such that A'⁻¹ and A⁻¹ agree up to that generalized permutation: A'⁻¹ i j = d i · A⁻¹ (τ i) j for every i, j.
Formal statement
Proof (Lean source)
LiNGAM identification theorem (kurtosis route, Marcinkiewicz-free). Let A, A' be n × n real mixing matrices, both invertible, with coefficient matrices A⁻¹ = I − B, A'⁻¹ = I − B' both having unit diagonal, and with A⁻¹ acyclic with respect to a causal order σ: (A⁻¹) i j = 0 whenever σ i < σ j. Let e, e' be families of real disturbances on a probability space, each coordinate measurable, each family's coordinates mutually independent, each coordinate of e with finite fourth moment, each coordinate of e centered, and the fourth cumulant of every coordinate of e nonzero and of one common sign. If the structural equations A·e and A'·e' produce the same observed law, then the coefficient matrices coincide, A⁻¹ = A'⁻¹ (i.e. B = B').