McCaskill partition function for RNA folding

DefinitionComplementary base pairing of two positions#✓fully proved

Positions i and j of s both lie in s and carry complementary bases.

def CanPair (i j : ℕ) : Prop :=
  ∃ a b, s[i]? = some a ∧ s[j]? = some b ∧ pair a b

Used by 8

Used byCounting semiring · Inside recursion · Inside algorithm · Outside recursion · Outside algorithm · McCaskill's base-pair probabilities · Zuker's algorithm · Zuker's recursion

DefinitionInside recursion#✓fully proved

Inside recursion over a commutative semiring R: inside pair m s w i len is the weighted sum over the secondary structures supported in the interval [i, i + len) (proved in inside_eq_sum). Base i is either unpaired, or paired with i + 1 + k for some k ≥ m with CanPair pair s i (i + 1 + k), which contributes w i (i + 1 + k) times the inside values of the enclosed interval [i + 1, i + 1 + k) and of the outer interval [i + k + 2, i + len + 1).

def inside [DecidableRel pair] {R : Type*} [CommSemiring R] (w : ℕ → ℕ → R) :
    ℕ → ℕ → R
  | _, 0 => 1
  | i, len + 1 =>
      inside w (i + 1) len +
        ∑ k : Fin len, if m ≤ k.val ∧ CanPair pair s i (i + 1 + k.val) then
          w i (i + 1 + k.val) * inside w (i + 1) k.val *
            inside w (i + k.val + 2) (len - 1 - k.val)
        else 0
  termination_by _ len => len
  decreasing_by all_goals omega

Uses 1 · Used by 8

Statement usesComplementary base pairing of two positions

Used byCounting semiring · McCaskill's algorithm · Inside algorithm · Inside value sums the weights of all secondary structures · Tropical semiring · Outside recursion · Outside algorithm · McCaskill's base-pair probabilities

DefinitionOutside recursion#✓fully proved

Outside recursion (McCaskill 1990) over a commutative semiring R, for a sequence of length n = s.length: outside pair m s w i j is the weighted sum of the parts outside the pair (i, j) of all structures containing it (proved in outside_mul_eq_sum). Either no pair encloses (i, j), leaving independent structures on [0, i) and [j + 1, n), or there is a unique innermost enclosing pair (a, b) (a < i, j < b < n), contributing the outside value of (a, b), its weight, and the inside values of [a + 1, i) and [j + 1, b).

def outside [DecidableRel pair] {R : Type*} [CommSemiring R] (w : ℕ → ℕ → R) (i j : ℕ) : R :=
  inside pair m s w 0 i * inside pair m s w (j + 1) (s.length - (j + 1)) +
    ∑ a : Fin i, ∑ c : Fin (s.length - (j + 1)),
      if a.val + m < j + 1 + c.val ∧ CanPair pair s a.val (j + 1 + c.val) then
        outside w a.val (j + 1 + c.val) * w a.val (j + 1 + c.val) *
          inside pair m s w (a.val + 1) (i - (a.val + 1)) * inside pair m s w (j + 1) c.val
      else 0
  termination_by s.length - (j - i)
  decreasing_by omega

Uses 2 · Used by 2

Statement usesComplementary base pairing of two positions · Inside recursion

Used byOutside algorithm · McCaskill's base-pair probabilities

DefinitionSecondary structures within an interval#✓fully proved

The secondary structures on s (IsStructure pair m s) all of whose pairs lie in the interval [i, i + len).

noncomputable def structuresIn (i len : ℕ) : Finset (Finset (ℕ × ℕ)) :=
  ((Finset.Ico i (i + len) ×ˢ Finset.Ico i (i + len)).powerset).filter
    fun P => IsStructure pair m s P

Uses 1 · Used by 4

Statement usesRNA secondary structure

Used byInside algorithm · Outside algorithm · Set of all secondary structures of a sequence · Zuker's algorithm

DefinitionSet of all secondary structures of a sequence#✓fully proved

All secondary structures on s with minimum hairpin m (see mem_structures).

noncomputable def structures : Finset (Finset (ℕ × ℕ)) :=
  structuresIn pair m s 0 s.length

Uses 1 · Used by 14

Statement usesSecondary structures within an interval

Used byCounting semiring · McCaskill's algorithm · Inside value sums the weights of all secondary structures · Tropical semiring · Membership in the set of secondary structures · Total structure weight is at least one · Outside algorithm · Base-pair probability · McCaskill's base-pair probabilities · Nonnegativity of base-pair probabilities · McCaskill partition function of RNA secondary structures · Each base pairs at most once · Zuker's algorithm · Minimum free energy is at most zero

DefinitionWeight of a secondary structure#✓fully proved

The weight of a structure: the product of the weights of its base pairs.

def weight {R : Type*} [CommMonoid R] (w : ℕ → ℕ → R) (P : Finset (ℕ × ℕ)) : R :=
  ∏ p ∈ P, w p.1 p.2

Used by 11

Used byCounting semiring · McCaskill's algorithm · Inside algorithm · Inside value sums the weights of all secondary structures · Tropical semiring · Total structure weight is at least one · Outside algorithm · Base-pair probability · McCaskill's base-pair probabilities · Nonnegativity of base-pair probabilities · Each base pairs at most once

TheoremMembership in the set of secondary structures#✓fully proved

structures is exactly the set of secondary structures on s.

theorem mem_structures (P : Finset (ℕ × ℕ)) :
    P ∈ structures pair m s ↔ IsStructure pair m s P

Uses 2 · Used by 5

Statement usesRNA secondary structure · Set of all secondary structures of a sequence

Used byTropical semiring · Total structure weight is at least one · Outside algorithm · Each base pairs at most once · Minimum free energy is at most zero

TheoremInside algorithm#✓fully proved

The inside recursion sums the weights of all secondary structures supported in the interval [i, i + len), over any commutative semiring.

theorem inside_eq_sum [DecidableRel pair] {R : Type*} [CommSemiring R] (w : ℕ → ℕ → R)
    (i len : ℕ) :
    inside pair m s w i len = ∑ P ∈ structuresIn pair m s i len, weight w P

Uses 5 · Used by 2

Statement usesInside recursion · Secondary structures within an interval · Weight of a secondary structure

Proof usesRNA secondary structure · Complementary base pairing of two positions

Used byInside value sums the weights of all secondary structures · Outside algorithm

TheoremInside value sums the weights of all secondary structures#✓fully proved

The inside value of the whole sequence sums the weights of all its secondary structures.

theorem inside_eq_sum_structures [DecidableRel pair] {R : Type*} [CommSemiring R]
    (w : ℕ → ℕ → R) :
    inside pair m s w 0 s.length = ∑ P ∈ structures pair m s, weight w P

Uses 4 · Used by 4

Statement usesInside recursion · Set of all secondary structures of a sequence · Weight of a secondary structure

Proof usesInside algorithm

Used byCounting semiring · McCaskill's algorithm · Tropical semiring · McCaskill's base-pair probabilities

TheoremOutside algorithm#✓fully proved

Outside algorithm (McCaskill 1990): for a candidate pair (i, j) (i + m < j and CanPair pair s i j), the outside value times the pair's weight times the inside value of the enclosed interval [i + 1, j) sums the weights of all secondary structures containing (i, j).

theorem outside_mul_eq_sum [DecidableRel pair] {R : Type*} [CommSemiring R]
    (w : ℕ → ℕ → R) (i j : ℕ) (hij : i + m < j) (hc : CanPair pair s i j) :
    outside pair m s w i j * w i j * inside pair m s w (i + 1) (j - (i + 1)) =
      ∑ P ∈ structures pair m s with (i, j) ∈ P, weight w P

Uses 9 · Used by 1

Statement usesComplementary base pairing of two positions · Inside recursion · Outside recursion · Set of all secondary structures of a sequence · Weight of a secondary structure

Proof usesRNA secondary structure · Inside algorithm · Membership in the set of secondary structures · Secondary structures within an interval

Used byMcCaskill's base-pair probabilities

22 fully proved

Min-plus: the Nussinov maximum

TheoremTropical semiring#✓fully proved

With every base pair weighted -1 in the min-plus semiring MinTropical (WithTop ℤ) (addition min, multiplication +), a structure with k pairs has weight -k, so the inside value of the whole sequence is minus the Nussinov maximum number of base pairs.

theorem inside_minTropical [DecidableRel pair] :
    inside pair m s (fun _ _ => MinTropical.trop ((-1 : ℤ) : WithTop ℤ)) 0 s.length =
      MinTropical.trop ((-(nussinov pair m s : ℤ) : ℤ) : WithTop ℤ)

Uses 9

Statement usesThe Nussinov recursion · Inside recursion

Proof usesRNA secondary structure · Soundness bound · Optimality · Inside value sums the weights of all secondary structures · Membership in the set of secondary structures · Set of all secondary structures of a sequence · Weight of a secondary structure

Counting: Waterman, Motzkin, Stein–Waterman

DefinitionWaterman's recursion#✓fully proved

Waterman's recursion for the number S_m(n) of secondary structures on n points with minimum hairpin m when every pair is allowed: S(0) = 1 and S(n + 1) = S(n) + ∑_{m ≤ k < n} S(k) S(n - 1 - k) (Waterman 1978; Stein–Waterman 1979). For m = 0 these are the Motzkin numbers (watermanNumber_zero_eq_motzkinNumber); for m = 1 the Stein–Waterman numbers 1, 1, 1, 2, 4, 8, 17, 37, … (OEIS A004148).

def watermanNumber (m : ℕ) : ℕ → ℕ
  | 0 => 1
  | n + 1 =>
      watermanNumber m n +
        ∑ k : Fin n, if m ≤ k.val then
          watermanNumber m k.val * watermanNumber m (n - 1 - k.val) else 0
  termination_by n => n
  decreasing_by all_goals omega

Used by 2

Used byCounting semiring · Waterman numbers with no hairpin constraint are Motzkin numbers

TheoremCounting semiring#✓fully proved

The number of secondary structures on n points with minimum hairpin m, when every pair of positions may pair, is Waterman's number S_m(n).

theorem card_structures_eq_watermanNumber (m n : ℕ) :
    (structures (fun _ _ : Unit => True) m (List.replicate n ())).card =
      watermanNumber m n

Uses 6

Statement usesSet of all secondary structures of a sequence · Waterman's recursion

Proof usesComplementary base pairing of two positions · Inside recursion · Inside value sums the weights of all secondary structures · Weight of a secondary structure

TheoremWaterman numbers with no hairpin constraint are Motzkin numbers#✓fully proved

For m = 0 (no hairpin constraint) Waterman's numbers are the Motzkin numbers M(n) = ∑_k C(n, 2k) C(k): the number of non-crossing partial matchings on n points.

theorem watermanNumber_zero_eq_motzkinNumber (n : ℕ) :
    watermanNumber 0 n = MetaMathlibExt.motzkinNumber n

Uses 3

Statement usesWaterman's recursion · Motzkin numbers as a Catalan-weighted binomial sum

Proof usesThe Motzkin recurrence

Sum-product: the McCaskill partition function

DefinitionAdditive base-pair energy model#✓fully proved

An additive base-pair energy model: the free energy of a structure is the sum of the energies e i j of its base pairs (in the same units as RT).

def energy (e : ℕ → ℕ → ℝ) (P : Finset (ℕ × ℕ)) : ℝ :=
  ∑ p ∈ P, e p.1 p.2

Used by 2

Used byMcCaskill's algorithm · McCaskill partition function of RNA secondary structures

DefinitionMcCaskill partition function of RNA secondary structures#✓fully proved

The partition function Z = ∑_S exp (-E(S) / RT) over all secondary structures S on s with minimum hairpin m, for the additive energy e at thermal energy RT (physically 0 < RT; the identities below hold for every real RT).

noncomputable def partitionFunction (e : ℕ → ℕ → ℝ) (RT : ℝ) : ℝ :=
  ∑ P ∈ structures pair m s, Real.exp (-energy e P / RT)

Uses 2 · Used by 1

Statement usesAdditive base-pair energy model · Set of all secondary structures of a sequence

Used byMcCaskill's algorithm

TheoremMcCaskill's algorithm#✓fully proved

McCaskill's algorithm (inside part): over the sum-product semiring ℝ with Boltzmann weights exp (-e i j / RT), the inside value of the whole sequence is the partition function. This is an algebraic identity valid for every real RT.

theorem inside_boltzmann_eq_partitionFunction [DecidableRel pair] (e : ℕ → ℕ → ℝ) (RT : ℝ) :
    inside pair m s (fun i j => Real.exp (-e i j / RT)) 0 s.length =
      partitionFunction pair m s e RT

Uses 6

Statement usesInside recursion · McCaskill partition function of RNA secondary structures

Proof usesAdditive base-pair energy model · Inside value sums the weights of all secondary structures · Set of all secondary structures of a sequence · Weight of a secondary structure

DefinitionBase-pair probability#✓fully proved

The base-pair probability P(i, j): the total weight of the structures containing the pair (i, j), divided by the total weight Z of all structures. For nonnegative weights Z ≥ 1 (the empty structure has weight 1), so the denominator is positive; for Boltzmann weights this is the probability of (i, j) under the Boltzmann distribution on structures.

noncomputable def pairProb (w : ℕ → ℕ → ℝ) (i j : ℕ) : ℝ :=
  (∑ P ∈ structures pair m s with (i, j) ∈ P, weight w P) /
    ∑ P ∈ structures pair m s, weight w P

Uses 2 · Used by 3

Statement usesSet of all secondary structures of a sequence · Weight of a secondary structure

Used byMcCaskill's base-pair probabilities · Nonnegativity of base-pair probabilities · Each base pairs at most once

TheoremMcCaskill's base-pair probabilities#✓fully proved

For a candidate pair (i, j), P(i, j) = outside(i, j) · w(i, j) · inside(i + 1, j) / inside(0, n).

theorem pairProb_eq_outside [DecidableRel pair] (w : ℕ → ℕ → ℝ) (i j : ℕ) (hij : i + m < j)
    (hc : CanPair pair s i j) :
    pairProb pair m s w i j =
      outside pair m s w i j * w i j * inside pair m s w (i + 1) (j - (i + 1)) /
        inside pair m s w 0 s.length

Uses 8

Statement usesComplementary base pairing of two positions · Inside recursion · Outside recursion · Base-pair probability

Proof usesInside value sums the weights of all secondary structures · Outside algorithm · Set of all secondary structures of a sequence · Weight of a secondary structure

TheoremTotal structure weight is at least one#✓fully proved

For nonnegative weights the total weight of all structures is at least 1, the weight of the empty structure; so the denominator of pairProb is positive.

theorem one_le_sum_weight (w : ℕ → ℕ → ℝ) (hw : ∀ i j, 0 ≤ w i j) :
    1 ≤ ∑ P ∈ structures pair m s, weight w P

Uses 4 · Used by 1

Statement usesSet of all secondary structures of a sequence · Weight of a secondary structure

Proof usesRNA secondary structure · Membership in the set of secondary structures

Used byEach base pairs at most once

TheoremNonnegativity of base-pair probabilities#✓fully proved

Base-pair probabilities are nonnegative for nonnegative weights.

theorem pairProb_nonneg (w : ℕ → ℕ → ℝ) (hw : ∀ i j, 0 ≤ w i j) (i j : ℕ) :
    0 ≤ pairProb pair m s w i j

Uses 3

Statement usesBase-pair probability

Proof usesSet of all secondary structures of a sequence · Weight of a secondary structure

TheoremEach base pairs at most once#✓fully proved

For nonnegative weights, the probabilities that base i pairs with some later base j or some earlier base j sum to at most 1 (∑_j (P(i, j) + P(j, i)) ≤ 1).

theorem sum_pairProb_le_one (w : ℕ → ℕ → ℝ) (hw : ∀ i j, 0 ≤ w i j) (i : ℕ) :
    ∑ j ∈ Finset.range s.length, (pairProb pair m s w i j + pairProb pair m s w j i) ≤ 1

Uses 6

Statement usesBase-pair probability

Proof usesRNA secondary structure · Membership in the set of secondary structures · Total structure weight is at least one · Set of all secondary structures of a sequence · Weight of a secondary structure

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.