Lander–Waterman coverage model

DefinitionRead covering a base of a circular genome#✓fully proved

A read of length L starting at position s of a circular genome of length G covers base x when x is one of s, s + 1, …, s + L - 1 (mod G), i.e. (x - s) mod G < L.

def Covers (G L : ℕ) (s x : Fin G) : Prop :=
  (x.val + G - s.val) % G < L

Used by 5

Used byExact depth law (count form) · Exact coverage count · Depth of coverage of a base · Exact uncovered probability · Lander–Waterman limit for the uncovered fraction

DefinitionDepth of coverage of a base#✓fully proved

The depth of coverage of base x: the number of reads covering it.

def depth {G N : ℕ} (L : ℕ) (starts : Fin N → Fin G) (x : Fin G) : ℕ :=
  (Finset.univ.filter fun j => Covers G L (starts j) x).card

Uses 1 · Used by 3

Statement usesRead covering a base of a circular genome

Used byExact depth law (count form) · Exact depth law · The coverage depth tends to Poisson(c)

DefinitionNormalized count of read start tuples#✓fully proved

The totalized normalized count |E| / G ^ N of a set of start tuples. For 0 < G, this is the probability when the N start positions are independent and uniform on Fin G. If G = 0 and N > 0, the sample space is empty and this value is zero, so it is not a probability law. For N = 0, there is one empty start tuple, even when G = 0.

noncomputable def normalizedCount {G N : ℕ} (E : Finset (Fin N → Fin G)) : ℝ :=
  (E.card : ℝ) / (G : ℝ) ^ N

Used by 6

Used byExpected number of no-successor reads (exact) · Exact depth law · Normalized count agrees with the totalized uniform measure · Exact uncovered probability · The coverage depth tends to Poisson(c) · Lander–Waterman limit for the uncovered fraction

TheoremNormalized count agrees with the totalized uniform measure#✓fully proved

normalizedCount agrees with Mathlib's totalized uniform measure on all start tuples. This measure is a probability law only when the sample space is nonempty.

theorem normalizedCount_eq_uniformOfFinset {G N : ℕ} (E : Finset (Fin N → Fin G)) :
    normalizedCount E =
      (MeasureTheory.Measure.uniformOfFinset (Finset.univ : Finset (Fin N → Fin G))
        (E : Set (Fin N → Fin G))).toReal

Uses 1

Statement usesNormalized count of read start tuples

TheoremExact coverage count#✓fully proved

For L ≤ G, base x is uncovered by all N reads for exactly (G - L) ^ N of the G ^ N start tuples.

theorem card_uncovered {G L N : ℕ} (hL : L ≤ G) (x : Fin G) :
    (Finset.univ.filter fun starts : Fin N → Fin G => ∀ j, ¬ Covers G L (starts j) x).card =
      (G - L) ^ N

Uses 1 · Used by 1

Statement usesRead covering a base of a circular genome

Used byExact uncovered probability

TheoremExact depth law (count form)#✓fully proved

For L ≤ G, base x is covered by exactly k reads for N.choose k * L ^ k * (G - L) ^ (N - k) of the start tuples.

theorem card_depth_eq {G L N : ℕ} (hL : L ≤ G) (x : Fin G) (k : ℕ) :
    (Finset.univ.filter fun starts : Fin N → Fin G => depth L starts x = k).card =
      N.choose k * L ^ k * (G - L) ^ (N - k)

Uses 2 · Used by 1

Statement usesDepth of coverage of a base

Proof usesRead covering a base of a circular genome

Used byExact depth law

TheoremExact uncovered probability#✓fully proved

Exact uncovered probability (Clarke–Carbon, Lander–Waterman, circular genome): (1 - L / G) ^ N for L ≤ G.

theorem normalizedCount_uncovered {G L N : ℕ} (hL : L ≤ G) (x : Fin G) :
    normalizedCount (Finset.univ.filter fun starts : Fin N → Fin G =>
        ∀ j, ¬ Covers G L (starts j) x) = (1 - (L : ℝ) / G) ^ N

Uses 3 · Used by 1

Statement usesRead covering a base of a circular genome · Normalized count of read start tuples

Proof usesExact coverage count

Used byLander–Waterman limit for the uncovered fraction

TheoremExact depth law#✓fully proved

The depth at a fixed base is binomial with N trials and success probability L / G, for L ≤ G.

theorem normalizedCount_depth_eq {G L N : ℕ} (hL : L ≤ G) (x : Fin G) (k : ℕ) :
    normalizedCount (Finset.univ.filter fun starts : Fin N → Fin G => depth L starts x = k) =
      (N.choose k : ℝ) * ((L : ℝ) / G) ^ k * (1 - (L : ℝ) / G) ^ (N - k)

Uses 3 · Used by 1

Statement usesDepth of coverage of a base · Normalized count of read start tuples

Proof usesExact depth law (count form)

Used byThe coverage depth tends to Poisson(c)

TheoremLander–Waterman limit for the uncovered fraction#✓fully proved

With read length L fixed, genome lengths G N ≥ L, and coverage N L / G_N → c as the number of reads N → ∞, the probability that a given base is uncovered tends to e^{-c}.

theorem tendsto_normalizedCount_uncovered (L : ℕ) (G : ℕ → ℕ) (hL : ∀ N, L ≤ G N) (c : ℝ)
    (hc : Tendsto (fun N : ℕ => (N : ℝ) * L / G N) atTop (𝓝 c)) (x : ∀ N, Fin (G N)) :
    Tendsto (fun N => normalizedCount (Finset.univ.filter fun starts : Fin N → Fin (G N) =>
        ∀ j, ¬ Covers (G N) L (starts j) (x N))) atTop (𝓝 (Real.exp (-c)))

Uses 3

Statement usesRead covering a base of a circular genome · Normalized count of read start tuples

Proof usesExact uncovered probability

TheoremThe coverage depth tends to Poisson(c)#✓fully proved

Under the hypotheses of tendsto_normalizedCount_uncovered, the probability that a given base is covered by exactly k reads tends to e^{-c} c^k / k.factorial.

theorem tendsto_normalizedCount_depth (L : ℕ) (G : ℕ → ℕ) (hL : ∀ N, L ≤ G N) (c : ℝ)
    (hc : Tendsto (fun N : ℕ => (N : ℝ) * L / G N) atTop (𝓝 c)) (x : ∀ N, Fin (G N)) (k : ℕ) :
    Tendsto (fun N => normalizedCount (Finset.univ.filter fun starts : Fin N → Fin (G N) =>
        depth L starts (x N) = k)) atTop
      (𝓝 (Real.exp (-c) * c ^ k / k.factorial))

Uses 3

Statement usesDepth of coverage of a base · Normalized count of read start tuples

Proof usesExact depth law

DefinitionRead with no successor#✓fully proved

Read j has no successor when no other read starts in the L - 1 positions after it, starts j + 1, …, starts j + L - 1 (mod G) (reads starting at the same position are not successors of each other). In Lander and Waterman's terms such a read is counted as ending an island, but several no-successor reads can lie in one island, so this is not the island count.

def NoSuccessor {G N : ℕ} (L : ℕ) (starts : Fin N → Fin G) (j : Fin N) : Prop :=
  ∀ j' ≠ j, ¬ (0 < ((starts j').val + G - (starts j).val) % G ∧
    ((starts j').val + G - (starts j).val) % G < L)

Used by 2

Used byExpected number of no-successor reads (exact) · Count of no-successor reads (exact)

TheoremCount of no-successor reads (exact)#✓fully proved

For L ≤ G, summed over the reads, the number of start tuples in which read j has no successor is N * G * (G - (L - 1)) ^ (N - 1). This counts no-successor reads, not island ends: a start tuple can have several no-successor reads in one island.

theorem sum_card_noSuccessor {G L N : ℕ} (hL : L ≤ G) :
    ∑ j : Fin N, (Finset.univ.filter fun starts : Fin N → Fin G =>
        NoSuccessor L starts j).card = N * G * (G - (L - 1)) ^ (N - 1)

Uses 1 · Used by 1

Statement usesRead with no successor

Used byExpected number of no-successor reads (exact)

TheoremExpected number of no-successor reads (exact)#✓fully proved

For 0 < G and L ≤ G, the expected number of reads with no successor is N (1 - (L - 1) / G) ^ (N - 1). The 0 < G hypothesis is essential: at G = 0 and N > 0, the right-hand expression is N while the sum of totalized normalized counts is zero.

theorem expected_noSuccessor {G L N : ℕ} (hG : 0 < G) (hL : L ≤ G) :
    ∑ j : Fin N, normalizedCount (Finset.univ.filter fun starts : Fin N → Fin G =>
        NoSuccessor L starts j) =
      (N : ℝ) * (1 - ((L - 1 : ℕ) : ℝ) / G) ^ (N - 1)

Uses 3

Statement usesRead with no successor · Normalized count of read start tuples

Proof usesCount of no-successor reads (exact)

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.