Posterior of the heterozygous selection coefficient

DefinitionMean PTV count at mutation-selection balance#✓fully proved

Mean PTV allele count n U / s at deterministic mutation–selection balance, for n sampled chromosomes, PTV mutation rate U and heterozygous selection coefficient s > 0.

noncomputable def balanceMean (n U s : ℝ) : ℝ := n * U / s

Used by 2

Used byBalance mean is decreasing in the selection coefficient · Cassa et al. (2017) model

TheoremBalance mean is decreasing in the selection coefficient#✓fully proved

The balance mean is antitone in s > 0 for n U ≥ 0.

theorem balanceMean_antitoneOn {n U : ℝ} (hnU : 0 ≤ n * U) :
    AntitoneOn (balanceMean n U) (Ioi 0)

Uses 1 · Used by 1

Statement usesMean PTV count at mutation-selection balance

Used byCassa et al. (2017) model

TheoremPosterior of s_het is stochastically nonincreasing in the PTV count, any antitone mean#✓fully proved

Posterior of s_het is stochastically nonincreasing in the PTV count, any antitone mean: for a prior μ on s_het concentrated on (0, ∞), a Poisson count with mean λ nonnegative and antitone on (0, ∞), integrable likelihoods and positive marginal likelihoods, P(s_het > t ∣ k') ≤ P(s_het > t ∣ k) whenever k ≤ k'.

theorem posteriorTail_antitone_of_antitoneOn {μ : Measure ℝ}
    (hμ : μ (Ioi 0)ᶜ = 0) {lam : ℝ → ℝ} (hanti : AntitoneOn lam (Ioi 0))
    (hnn : ∀ s ∈ Ioi (0 : ℝ), 0 ≤ lam s) (hint : ∀ k, Integrable (poissonLik lam k) μ)
    {k k' : ℕ} (hkk' : k ≤ k') (hk : 0 < ∫ s, poissonLik lam k s ∂μ)
    (hk' : 0 < ∫ s, poissonLik lam k' s ∂μ) (t : ℝ) :
    posteriorTail μ (poissonLik lam) k' t ≤ posteriorTail μ (poissonLik lam) k t

Uses 4 · Used by 1

Statement usesPoisson likelihood · Posterior tail probability

Proof usesPoisson family with antitone mean has antitone likelihood ratio · The posterior is stochastically nonincreasing in the observation

Used byCassa et al. (2017) model

TheoremCassa et al. (2017) model#✓fully proved

With the balance mean n U / s_het (n, U > 0) and any probability prior on s_het ∈ (0, ∞), the posterior probability P(s_het > t ∣ k) is nonincreasing in the observed PTV count k.

theorem posteriorTail_balance_antitone {μ : Measure ℝ} [IsProbabilityMeasure μ]
    (hμ : μ (Ioi 0)ᶜ = 0) {n U : ℝ} (hn : 0 < n) (hU : 0 < U) {k k' : ℕ} (hkk' : k ≤ k')
    (t : ℝ) :
    posteriorTail μ (poissonLik (balanceMean n U)) k' t ≤
      posteriorTail μ (poissonLik (balanceMean n U)) k t

Uses 5

Statement usesMean PTV count at mutation-selection balance · Poisson likelihood · Posterior tail probability

Proof usesBalance mean is decreasing in the selection coefficient · Posterior of s_het is stochastically nonincreasing in the PTV count, any antitone mean

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.