Composite selection scores

15 fully proved

The composite of multiple signals

StructureComposite selection score model#✓fully proved

A composite-score model (Grossman et al. 2010): a prior probability prior that the site is under selection, and for each of the k component statistics a positive score function sel under selection and neut under neutrality (unnormalized densities: only positivity is assumed). Conditionally on the hypothesis the components are independent, which is what makes the joint scores the products below. The Bayes/posterior reading of posterior requires the additional normalization hypothesis of sum_joint_eq_one.

MathlibExt.Biology.PopulationGenetics.SelectionScan.CompositeModel · 15 lines

structure CompositeModel (k : ℕ) (σ : Fin k → Type*) where
  /-- The prior probability that the site is under selection. -/
  prior : ℝ
  /-- The prior is a probability strictly between `0` and `1`. -/
  prior_pos : 0 < prior
  /-- The prior is a probability strictly between `0` and `1`. -/
  prior_lt_one : prior < 1
  /-- The unnormalized score function of component `i` under selection. -/
  sel : ∀ i, σ i → ℝ
  /-- The unnormalized score function of component `i` under neutrality. -/
  neut : ∀ i, σ i → ℝ
  /-- Component score functions under selection are positive. -/
  sel_pos : ∀ i x, 0 < sel i x
  /-- Component score functions under neutrality are positive. -/
  neut_pos : ∀ i x, 0 < neut i x

Used by 9

Used byBayes factor of a component statistic · Positivity of component Bayes factors · Composite of multiple signals (CMS) score · CMS score as a ratio of joint densities · Additivity of evidence on the log-odds scale · Normalized composite score · Posterior probability is strictly increasing in the CMS score · Posterior odds equal prior odds times the CMS score · Normalization of the composite score model

DefinitionBayes factor of a component statistic#✓fully proved

The Bayes factor of component i at the observed value: the ratio of its score function under selection to its score function under neutrality.

noncomputable def bayesFactor (i : Fin k) (y : σ i) : ℝ := M.sel i y / M.neut i y

Uses 1 · Used by 5

Statement usesComposite selection score model

Used byPositivity of component Bayes factors · Composite of multiple signals (CMS) score · CMS score as a ratio of joint densities · Additivity of evidence on the log-odds scale · Posterior probability is strictly increasing in the CMS score

DefinitionComposite of multiple signals (CMS) score#✓fully proved

The CMS score: the product of the component Bayes factors.

noncomputable def cms : ℝ := ∏ i, M.bayesFactor i (x i)

Uses 2 · Used by 4

Statement usesComposite selection score model · Bayes factor of a component statistic

Used byCMS score as a ratio of joint densities · Additivity of evidence on the log-odds scale · Posterior probability is strictly increasing in the CMS score · Posterior odds equal prior odds times the CMS score

DefinitionNormalized composite score#✓fully proved

The normalized composite score: the normalized ratio of the products of the component score functions. This is the posterior probability of selection given the observed component values when the score functions are normalized densities (see sum_joint_eq_one for the normalization hypothesis).

noncomputable def posterior : ℝ :=
  M.prior * (∏ i, M.sel i (x i)) /
    (M.prior * (∏ i, M.sel i (x i)) + (1 - M.prior) * ∏ i, M.neut i (x i))

Uses 1 · Used by 3

Statement usesComposite selection score model

Used byAdditivity of evidence on the log-odds scale · Posterior probability is strictly increasing in the CMS score · Posterior odds equal prior odds times the CMS score

TheoremPositivity of component Bayes factors#✓fully proved

Every component Bayes factor is positive.

theorem bayesFactor_pos (i : Fin k) (y : σ i) : 0 < M.bayesFactor i y

Uses 2 · Used by 2

Statement usesComposite selection score model · Bayes factor of a component statistic

Used byAdditivity of evidence on the log-odds scale · Posterior probability is strictly increasing in the CMS score

TheoremCMS score as a ratio of joint densities#✓fully proved

The CMS score is the ratio of the two joint densities.

theorem cms_eq_div : M.cms x = (∏ i, M.sel i (x i)) / ∏ i, M.neut i (x i)

Uses 3 · Used by 2

Statement usesComposite selection score model · Composite of multiple signals (CMS) score

Proof usesBayes factor of a component statistic

Used byPosterior probability is strictly increasing in the CMS score · Posterior odds equal prior odds times the CMS score

TheoremPosterior odds equal prior odds times the CMS score#✓fully proved

Bayes-rule identity for conditionally independent components: the posterior odds of selection are the prior odds times the CMS score. This is an algebraic identity for the normalized score; it is a genuine Bayes rule only under the normalization hypothesis of sum_joint_eq_one.

theorem posterior_odds :
    M.posterior x / (1 - M.posterior x) = M.prior / (1 - M.prior) * M.cms x

Uses 4 · Used by 1

Statement usesComposite selection score model · Composite of multiple signals (CMS) score · Normalized composite score

Proof usesCMS score as a ratio of joint densities

Used byAdditivity of evidence on the log-odds scale

TheoremAdditivity of evidence on the log-odds scale#✓fully proved

On the log scale the evidence is additive: the log posterior odds are the log prior odds plus the sum of the log Bayes factors of the component statistics.

theorem log_posterior_odds :
    log (M.posterior x / (1 - M.posterior x))
      = log (M.prior / (1 - M.prior)) + ∑ i, log (M.bayesFactor i (x i))

Uses 6

Statement usesComposite selection score model · Bayes factor of a component statistic · Normalized composite score

Proof usesPositivity of component Bayes factors · Composite of multiple signals (CMS) score · Posterior odds equal prior odds times the CMS score

TheoremPosterior probability is strictly increasing in the CMS score#✓fully proved

The posterior probability is a strictly increasing function of the CMS score, so the two rankings of sites agree.

theorem posterior_lt_posterior_of_cms_lt (y : ∀ i, σ i) (h : M.cms x < M.cms y) :
    M.posterior x < M.posterior y

Uses 6

Statement usesComposite selection score model · Composite of multiple signals (CMS) score · Normalized composite score

Proof usesBayes factor of a component statistic · Positivity of component Bayes factors · CMS score as a ratio of joint densities

TheoremNormalization of the composite score model#✓fully proved

The model is a probability model: with normalised component score functions (each a density with respect to a common base measure), the joint distribution of the observations sums to one. This is the validity hypothesis that makes posterior a genuine Bayes posterior.

theorem sum_joint_eq_one [∀ i, Fintype (σ i)]
    (hsel : ∀ i, ∑ y, M.sel i y = 1) (hneut : ∀ i, ∑ y, M.neut i y = 1) :
    ∑ z : (∀ i, σ i),
      (M.prior * (∏ i, M.sel i (z i)) + (1 - M.prior) * ∏ i, M.neut i (z i)) = 1

Uses 1

Statement usesComposite selection score model

Identifiability of a sweep location and strength

DefinitionProbability of escaping a selective sweep#✓fully proved

The probability that a lineage at position y escapes a sweep located at x, with compound strength parameter α > 0: 1 - exp (-α |y - x|) (Kim and Stephan 2002; Nielsen et al. 2005). The parameter α is proportional to the recombination rate per unit distance divided by the selection coefficient.

noncomputable def escapeProb (α x y : ℝ) : ℝ := 1 - exp (-α * |y - x|)

Used by 3

Used byEscape probability vanishes only at the swept site · Escape profile determines sweep location and strength · Identifiability of sweep parameters from frequency spectra

TheoremEscape probability vanishes only at the swept site#✓fully proved

No lineage escapes at the swept site itself, and nowhere else.

theorem escapeProb_eq_zero_iff {α : ℝ} (hα : 0 < α) (x y : ℝ) :
    escapeProb α x y = 0 ↔ y = x

Uses 1 · Used by 1

Statement usesProbability of escaping a selective sweep

Used byEscape profile determines sweep location and strength

TheoremEscape profile determines sweep location and strength#✓fully proved

The escape-probability profile determines the sweep location and its strength. Positivity of one of the two strength parameters is enough: the location is the unique zero of that profile, and the strengths then agree by injectivity of exp.

theorem escapeProb_inj {α₁ α₂ x₁ x₂ : ℝ} (hα₂ : 0 < α₂)
    (h : ∀ y, escapeProb α₁ x₁ y = escapeProb α₂ x₂ y) : x₁ = x₂ ∧ α₁ = α₂

Uses 2 · Used by 1

Statement usesProbability of escaping a selective sweep

Proof usesEscape probability vanishes only at the swept site

Used byIdentifiability of sweep parameters from frequency spectra

TheoremUniqueness of the mixing weight of a two-component mixture#✓fully proved

A mixture of two distinct laws determines its mixing weight.

theorem mixture_weight_unique {β : Type*} {f g : β → ℝ} (hfg : f ≠ g) {p q : ℝ}
    (h : ∀ b, p * f b + (1 - p) * g b = q * f b + (1 - q) * g b) : p = q

Used by 1

Used byIdentifiability of sweep parameters from frequency spectra

TheoremIdentifiability of sweep parameters from frequency spectra#✓fully proved

Identifiability of the sweep parameters from the per-site frequency spectra. If the neutral spectrum f and the post-sweep spectrum g differ, and two sweep parameter pairs give the same mixture at every position, then the parameters coincide. This is what the composite likelihood of SweepFinder maximises over.

theorem sweep_param_unique {β : Type*} {f g : β → ℝ} (hfg : f ≠ g) {α₁ α₂ x₁ x₂ : ℝ}
    (hα₂ : 0 < α₂)
    (h : ∀ y b, escapeProb α₁ x₁ y * f b + (1 - escapeProb α₁ x₁ y) * g b
      = escapeProb α₂ x₂ y * f b + (1 - escapeProb α₂ x₂ y) * g b) :
    x₁ = x₂ ∧ α₁ = α₂

Uses 3

Statement usesProbability of escaping a selective sweep

Proof usesEscape profile determines sweep location and strength · Uniqueness of the mixing weight of a two-component mixture

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.