ARACNE gene network reconstruction

DefinitionARACNE gene network reconstruction#✓fully proved

The network ARACNE reconstructs from symmetric pairwise mutual informations I with independence threshold I₀ and DPI tolerance zero (Margolin et al. 2006): {i, k} is an edge iff i ≠ k, I₀ < I i k, and no third gene j with I₀ < I i j and I₀ < I j k has I i k < min (I i j) (I j k).

def aracne (I : V → V → ℝ) (hI : ∀ i k, I i k = I k i) (I₀ : ℝ) : SimpleGraph V where
  Adj i k := i ≠ k ∧ I₀ < I i k ∧
    ∀ j, j ≠ i → j ≠ k → I₀ < I i j → I₀ < I j k → min (I i j) (I j k) ≤ I i k
  symm := ⟨by
    rintro i k ⟨hik, h0, h⟩
    refine ⟨hik.symm, hI i k ▸ h0, fun j hjk hji hkj hji' ↦ ?_⟩
    rw [hI k j, hI j i] at *
    rw [hI k i, min_comm]
    exact h j hji hjk hji' hkj⟩
  loopless := ⟨fun _ h ↦ h.1 rfl⟩

Used by 4

Used byARACNE recovers tree networks exactly · No false positives · No false negatives · Chow–Liu trees survive ARACNE

TheoremNo false negatives#✓fully proved

If the true network T is a forest whose edges all carry mutual information above I₀, and I a b ≤ min (I a c) (I c b) whenever c separates a from b in T (every walk from a to b visits c), then ARACNE keeps every edge of T.

theorem le_aracne_of_isAcyclic (T : SimpleGraph V) (hT : T.IsAcyclic) (I : V → V → ℝ)
    (hI : ∀ i k, I i k = I k i) (I₀ : ℝ) (hedge : ∀ i k, T.Adj i k → I₀ < I i k)
    (hdpi : ∀ a b c, c ≠ a → c ≠ b → (∀ p : T.Walk a b, c ∈ p.support) →
      I a b ≤ min (I a c) (I c b)) :
    T ≤ aracne I hI I₀

Uses 1 · Used by 1

Statement usesARACNE gene network reconstruction

Used byARACNE recovers tree networks exactly

TheoremNo false positives#✓fully proved

If the true network T is a tree and I a b < min (I a c) (I c b) whenever c separates a from b in T, then every edge ARACNE keeps is an edge of T.

theorem aracne_le_of_isTree (T : SimpleGraph V) (hT : T.IsTree) (I : V → V → ℝ)
    (hI : ∀ i k, I i k = I k i) (I₀ : ℝ)
    (hdpi : ∀ a b c, c ≠ a → c ≠ b → (∀ p : T.Walk a b, c ∈ p.support) →
      I a b < min (I a c) (I c b)) :
    aracne I hI I₀ ≤ T

Uses 1 · Used by 1

Statement usesARACNE gene network reconstruction

Used byARACNE recovers tree networks exactly

TheoremARACNE recovers tree networks exactly#✓fully proved

ARACNE recovers tree networks exactly (Margolin et al. 2006, Theorem 1): if the true network T is a tree whose edges all carry mutual information above I₀, and the strict data-processing inequality holds on every separated triple, then ARACNE returns T. Strictness is the explicit form of the paper's exclusion of exact cancellations; with equality ARACNE can keep an indirect edge (see the tests).

theorem aracne_eq_of_isTree (T : SimpleGraph V) (hT : T.IsTree) (I : V → V → ℝ)
    (hI : ∀ i k, I i k = I k i) (I₀ : ℝ) (hedge : ∀ i k, T.Adj i k → I₀ < I i k)
    (hdpi : ∀ a b c, c ≠ a → c ≠ b → (∀ p : T.Walk a b, c ∈ p.support) →
      I a b < min (I a c) (I c b)) :
    aracne I hI I₀ = T

Uses 3

Statement usesARACNE gene network reconstruction

Proof usesNo false positives · No false negatives

TheoremChow–Liu trees survive ARACNE#✓fully proved

Chow–Liu trees survive ARACNE (Margolin et al. 2006, Theorem 2): a spanning tree T of maximum total weight ∑_{{i, k} ∈ T} I i k among all spanning trees, whose edges all carry mutual information above I₀, is a subnetwork of the ARACNE network.

theorem le_aracne_of_isMaxWeightSpanningTree [Fintype V] (I : V → V → ℝ)
    (hI : ∀ i k, I i k = I k i) (I₀ : ℝ) (T : SimpleGraph V) [DecidableRel T.Adj]
    (hT : T.IsTree)
    (hmax : ∀ (T' : SimpleGraph V) [DecidableRel T'.Adj], T'.IsTree →
      ∑ e ∈ T'.edgeFinset, Sym2.lift ⟨I, hI⟩ e ≤ ∑ e ∈ T.edgeFinset, Sym2.lift ⟨I, hI⟩ e)
    (hedge : ∀ i k, T.Adj i k → I₀ < I i k) :
    T ≤ aracne I hI I₀

Uses 1

Statement usesARACNE gene network reconstruction

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.