Gene constraint scores (pLI and LOEUF)

DefinitionPoisson likelihood of an observed count#✓fully proved

The Poisson likelihood e^{-μ} μ^o / (o!) of an observed count o at mean μ.

noncomputable def poissonLik (μ : ℝ) (o : ℕ) : ℝ := exp (-μ) * μ ^ o / (o ! : ℝ)

Used by 10

Used byPosterior class probability in the Poisson mixture · pLI is antitone in the observed count · Class posterior is strictly antitone in the observed count · The M-step maximizes Q(· | w) · Flat-prior posterior of γ · Joint likelihood of gene data and constraint class · Positivity of the Poisson mixture joint likelihood · Positivity of the Poisson likelihood · Recursion for the Poisson likelihood · Class posteriors sum to one

TheoremPositivity of the Poisson likelihood#✓fully proved

The likelihood is positive at a positive mean.

theorem poissonLik_pos {μ : ℝ} (hμ : 0 < μ) (o : ℕ) : 0 < poissonLik μ o

Uses 1 · Used by 5

Statement usesPoisson likelihood of an observed count

Used bypLI is antitone in the observed count · Class posterior is strictly antitone in the observed count · The M-step maximizes Q(· | w) · Positivity of the Poisson mixture joint likelihood · Class posteriors sum to one

TheoremFlat-prior posterior of γ#✓fully proved

The likelihood γ ↦ P(o | Poisson(γ E)) times E is the Gamma density of shape o + 1 and rate E. For E > 0 that density integrates to one, so E is the normalizing constant of the flat-prior posterior (the identity itself is algebraic and holds for every real E).

theorem flatPosterior_density (E : ℝ) {γ : ℝ} (hγ : 0 ≤ γ) (o : ℕ) :
    E * poissonLik (γ * E) o = gammaPDFReal (o + 1) E γ

Uses 1

Statement usesPoisson likelihood of an observed count

DefinitionUpper confidence bound for the observed/expected ratio#✓fully proved

The upper confidence bound for the observed/expected ratio at level α: u_α(o) / E, with u_α Garwood's bound for the Poisson mean.

noncomputable def oeUpper (α E : ℝ) (o : ℕ) : ℝ := garwoodUpper α o / E

Uses 1 · Used by 7

Statement usesGarwood's exact upper confidence bound

Used byThe flat-prior posterior quantile is Garwood's bound · LOEUF · LOEUF of a gene with no observed LoF variants · Exact coverage · Observed/expected upper bound decreases with the expected count · Observed/expected upper bound increases with the observed count · Observed/expected upper bound with no observed variants

DefinitionLOEUF#✓fully proved

The upper end of the 90% interval, oeUpper (1/20).

noncomputable def loeuf (E : ℝ) (o : ℕ) : ℝ := oeUpper (1 / 20) E o

Uses 1 · Used by 1

Statement usesUpper confidence bound for the observed/expected ratio

Used byLOEUF of a gene with no observed LoF variants

TheoremThe flat-prior posterior quantile is Garwood's bound#✓fully proved

The Gamma(o + 1, E) posterior puts mass exactly 1 - α below oeUpper α E o.

theorem gammaMeasure_real_Iic_oeUpper {α E : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (hE : 0 < E)
    (o : ℕ) : (gammaMeasure (o + 1) E).real (Iic (oeUpper α E o)) = 1 - α

Uses 6

Statement usesUpper confidence bound for the observed/expected ratio

Proof usesPoisson–Gamma duality · Garwood's exact upper confidence bound · Positivity of the Garwood upper bound · Poisson distribution function as a function of the mean · Garwood upper bound solves the distribution function equation

TheoremExact coverage#✓fully proved

For every true ratio γ ≥ 0 and E > 0, when o ~ Poisson(γ E), P(γ ≤ oeUpper α E o) ≥ 1 - α.

theorem oeUpper_coverage {α E : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (hE : 0 < E) (γ : ℝ≥0) :
    1 - α ≤ (poissonMeasure (γ * ⟨E, hE.le⟩)).real {o | (γ : ℝ) ≤ oeUpper α E o}

Uses 3

Statement usesUpper confidence bound for the observed/expected ratio

Proof usesGarwood's exact upper confidence bound · Exact coverage of Garwood's bound

TheoremObserved/expected upper bound with no observed variants#✓fully proved

With no observed variants the bound is log (1 / α) / E.

theorem oeUpper_zero {α E : ℝ} (hα0 : 0 < α) (hα1 : α < 1) :
    oeUpper α E 0 = log (1 / α) / E

Uses 3 · Used by 1

Statement usesUpper confidence bound for the observed/expected ratio

Proof usesGarwood's exact upper confidence bound · Garwood upper bound after observing zero

Used byLOEUF of a gene with no observed LoF variants

TheoremLOEUF of a gene with no observed LoF variants#✓fully proved

LOEUF of a gene with no observed LoF variants is log 20 / E.

theorem loeuf_zero (E : ℝ) : loeuf E 0 = log 20 / E

Uses 3

Statement usesLOEUF

Proof usesUpper confidence bound for the observed/expected ratio · Observed/expected upper bound with no observed variants

TheoremObserved/expected upper bound increases with the observed count#✓fully proved

The bound is strictly increasing in the observed count.

theorem oeUpper_strictMono {α E : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (hE : 0 < E) :
    StrictMono (oeUpper α E)

Uses 3

Statement usesUpper confidence bound for the observed/expected ratio

Proof usesGarwood's exact upper confidence bound · Garwood upper bound is strictly increasing in the count

TheoremObserved/expected upper bound decreases with the expected count#✓fully proved

The bound is strictly decreasing in the expected count E > 0.

theorem oeUpper_strictAntiOn {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (o : ℕ) :
    StrictAntiOn (fun E => oeUpper α E o) (Ioi 0)

Uses 3

Statement usesUpper confidence bound for the observed/expected ratio

Proof usesGarwood's exact upper confidence bound · Positivity of the Garwood upper bound

DefinitionPosterior class probability in the Poisson mixture#✓fully proved

The posterior probability of class c for a gene with o observed and E expected LoF variants, in the Poisson mixture with prior weights w and class rates rate: w_c P(o | rate_c E) / ∑_{c'} w_{c'} P(o | rate_{c'} E). pLI is this at the class with the smallest rate.

noncomputable def classPosterior (w rate : ι → ℝ) (E : ℝ) (o : ℕ) (c : ι) : ℝ :=
  w c * poissonLik (rate c * E) o / ∑ c', w c' * poissonLik (rate c' * E) o

Uses 1 · Used by 3

Statement usesPoisson likelihood of an observed count

Used bypLI is antitone in the observed count · Class posterior is strictly antitone in the observed count · Class posteriors sum to one

TheoremClass posteriors sum to one#✓fully proved

The class posteriors sum to one.

theorem sum_classPosterior {w rate : ι → ℝ} {E : ℝ} (hw : ∀ c, 0 < w c) (hrate : ∀ c, 0 < rate c)
    (hE : 0 < E) [Nonempty ι] (o : ℕ) : ∑ c, classPosterior w rate E o c = 1

Uses 3

Statement usesPosterior class probability in the Poisson mixture

Proof usesPoisson likelihood of an observed count · Positivity of the Poisson likelihood

TheoremRecursion for the Poisson likelihood#✓fully proved

The likelihood recursion P(o + 1 | μ) = P(o | μ) μ / (o + 1).

theorem poissonLik_succ (μ : ℝ) (o : ℕ) :
    poissonLik μ (o + 1) = poissonLik μ o * μ / (o + 1)

Uses 1 · Used by 2

Statement usesPoisson likelihood of an observed count

Used bypLI is antitone in the observed count · Class posterior is strictly antitone in the observed count

TheorempLI is antitone in the observed count#✓fully proved

The posterior of a class c₀ whose rate is the smallest is antitone in o, for every prior.

theorem classPosterior_antitone {w rate : ι → ℝ} {E : ℝ} (hw : ∀ c, 0 < w c)
    (hrate : ∀ c, 0 < rate c) (hE : 0 < E) {c₀ : ι} (hmin : ∀ c, rate c₀ ≤ rate c) :
    Antitone fun o => classPosterior w rate E o c₀

Uses 4

Statement usesPosterior class probability in the Poisson mixture

Proof usesPoisson likelihood of an observed count · Positivity of the Poisson likelihood · Recursion for the Poisson likelihood

TheoremClass posterior is strictly antitone in the observed count#✓fully proved

Strictly antitone when some class has a strictly larger rate.

theorem classPosterior_strictAnti {w rate : ι → ℝ} {E : ℝ} (hw : ∀ c, 0 < w c)
    (hrate : ∀ c, 0 < rate c) (hE : 0 < E) {c₀ : ι} (hmin : ∀ c, rate c₀ ≤ rate c)
    (hlt : ∃ c, rate c₀ < rate c) : StrictAnti fun o => classPosterior w rate E o c₀

Uses 4

Statement usesPosterior class probability in the Poisson mixture

Proof usesPoisson likelihood of an observed count · Positivity of the Poisson likelihood · Recursion for the Poisson likelihood

DefinitionStrictly positive class weights summing to one#✓fully proved

Strictly positive class weights summing to one.

def PosWeights (ι : Type*) [Fintype ι] : Type _ :=
  {w : ι → ℝ // (∀ c, 0 < w c) ∧ ∑ c, w c = 1}

Used by 9

Used byThe M-step maximizes Q(· | w) · EM update of the Poisson mixture class weights · Joint likelihood of gene data and constraint class · Positivity of the Poisson mixture joint likelihood · Monotonicity of the log-likelihood along the class-weight EM iterates · EM does not decrease the likelihood · Expected number of genes in a constraint class · Positivity of the class masses · Class masses sum to the number of genes

StructureLoss-of-function count data for a gene#✓fully proved

A gene's data: observed LoF count o and positive expected count E.

structure GeneData where
  /-- Observed LoF count. -/
  o : ℕ
  /-- Expected LoF count under neutrality. -/
  E : ℝ
  E_pos : 0 < E

Used by 9

Used byThe M-step maximizes Q(· | w) · EM update of the Poisson mixture class weights · Joint likelihood of gene data and constraint class · Positivity of the Poisson mixture joint likelihood · Monotonicity of the log-likelihood along the class-weight EM iterates · EM does not decrease the likelihood · Expected number of genes in a constraint class · Positivity of the class masses · Class masses sum to the number of genes

DefinitionJoint likelihood of gene data and constraint class#✓fully proved

The joint likelihood of a gene's data and class z: w_z P(o | rate_z E).

noncomputable def joint (rate : ι → ℝ) (w : PosWeights ι) (x : GeneData) (z : ι) : ℝ :=
  w.1 z * poissonLik (rate z * x.E) x.o

Uses 3 · Used by 7

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · Poisson likelihood of an observed count

Used byThe M-step maximizes Q(· | w) · Positivity of the Poisson mixture joint likelihood · Monotonicity of the log-likelihood along the class-weight EM iterates · EM does not decrease the likelihood · Expected number of genes in a constraint class · Positivity of the class masses · Class masses sum to the number of genes

TheoremPositivity of the Poisson mixture joint likelihood#✓fully proved

The joint likelihood is positive for positive rates.

theorem joint_pos {rate : ι → ℝ} (hrate : ∀ c, 0 < rate c) (w : PosWeights ι) (x : GeneData)
    (z : ι) : 0 < joint rate w x z

Uses 5 · Used by 4

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · Joint likelihood of gene data and constraint class

Proof usesPoisson likelihood of an observed count · Positivity of the Poisson likelihood

Used byMonotonicity of the log-likelihood along the class-weight EM iterates · EM does not decrease the likelihood · Positivity of the class masses · Class masses sum to the number of genes

DefinitionExpected number of genes in a constraint class#✓fully proved

The expected number of genes in class z under the posteriors at weights w: ∑_n P_w(z | o_n).

noncomputable def mass (rate : ι → ℝ) (xs : Fin N → GeneData) (w : PosWeights ι) (z : ι) : ℝ :=
  ∑ n, posterior (joint rate) w (xs n) z

Uses 4 · Used by 4

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · Joint likelihood of gene data and constraint class · Posterior of a latent-variable model

Used byThe M-step maximizes Q(· | w) · EM update of the Poisson mixture class weights · Positivity of the class masses · Class masses sum to the number of genes

TheoremPositivity of the class masses#✓fully proved

The class masses are positive when there is at least one gene.

theorem mass_pos [Nonempty ι] {rate : ι → ℝ} (hrate : ∀ c, 0 < rate c)
    (xs : Fin N → GeneData) (hN : 0 < N) (w : PosWeights ι) (z : ι) : 0 < mass rate xs w z

Uses 7 · Used by 2

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · Expected number of genes in a constraint class

Proof usesJoint likelihood of gene data and constraint class · Positivity of the Poisson mixture joint likelihood · Marginal of a latent-variable model · Posterior of a latent-variable model

Used byThe M-step maximizes Q(· | w) · EM update of the Poisson mixture class weights

TheoremClass masses sum to the number of genes#✓fully proved

The class masses add up to the number of genes.

theorem sum_mass [Nonempty ι] {rate : ι → ℝ} (hrate : ∀ c, 0 < rate c)
    (xs : Fin N → GeneData) (w : PosWeights ι) : ∑ z, mass rate xs w z = N

Uses 7 · Used by 2

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · Expected number of genes in a constraint class

Proof usesJoint likelihood of gene data and constraint class · Positivity of the Poisson mixture joint likelihood · Posteriors are probability distributions · Posterior of a latent-variable model

Used byThe M-step maximizes Q(· | w) · EM update of the Poisson mixture class weights

DefinitionEM update of the Poisson mixture class weights#✓fully proved

The EM update w'_z = (1/N) ∑_n P_w(z | o_n), for N > 0 genes and positive rates.

noncomputable def emStep [Nonempty ι] {rate : ι → ℝ} (hrate : ∀ c, 0 < rate c)
    (xs : Fin N → GeneData) (hN : 0 < N) (w : PosWeights ι) : PosWeights ι :=
  ⟨fun z => mass rate xs w z / N, fun z => div_pos (mass_pos hrate xs hN w z)
    (by exact_mod_cast hN), by
    rw [← Finset.sum_div, sum_mass hrate xs w]
    exact div_self (by exact_mod_cast hN.ne')⟩

Uses 5 · Used by 3

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · Expected number of genes in a constraint class · Positivity of the class masses · Class masses sum to the number of genes

Used byThe M-step maximizes Q(· | w) · Monotonicity of the log-likelihood along the class-weight EM iterates · EM does not decrease the likelihood

TheoremThe M-step maximizes Q(· | w)#✓fully proved

The M-step maximizes Q(· | w) over admissible weights.

theorem emQ_le_emStep [Nonempty ι] {rate : ι → ℝ} (hrate : ∀ c, 0 < rate c)
    (xs : Fin N → GeneData) (hN : 0 < N) (w' w : PosWeights ι) :
    emQ (joint rate) xs w' w ≤ emQ (joint rate) xs (emStep hrate xs hN w) w

Uses 12 · Used by 2

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · EM update of the Poisson mixture class weights · Joint likelihood of gene data and constraint class · The EM objective

Proof usesExpected number of genes in a constraint class · Positivity of the class masses · Class masses sum to the number of genes · The weighted log-likelihood is bounded by its value at the normalized counts · Posterior of a latent-variable model · Poisson likelihood of an observed count · Positivity of the Poisson likelihood

Used byMonotonicity of the log-likelihood along the class-weight EM iterates · EM does not decrease the likelihood

TheoremEM does not decrease the likelihood#✓fully proved

EM does not decrease the likelihood of the class weights.

theorem logLik_le_logLik_emStep [Nonempty ι] {rate : ι → ℝ} (hrate : ∀ c, 0 < rate c)
    (xs : Fin N → GeneData) (hN : 0 < N) (w : PosWeights ι) :
    logLik (joint rate) xs w ≤ logLik (joint rate) xs (emStep hrate xs hN w)

Uses 8

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · EM update of the Poisson mixture class weights · Joint likelihood of gene data and constraint class · Log-likelihood of a latent-variable model

Proof usesThe M-step maximizes Q(· | w) · Positivity of the Poisson mixture joint likelihood · The EM theorem

TheoremMonotonicity of the log-likelihood along the class-weight EM iterates#✓fully proved

The log-likelihood is monotone along the EM iterates.

theorem logLik_iterate_emStep_monotone [Nonempty ι] {rate : ι → ℝ} (hrate : ∀ c, 0 < rate c)
    (xs : Fin N → GeneData) (hN : 0 < N) (w₀ : PosWeights ι) :
    Monotone fun k => logLik (joint rate) xs ((emStep hrate xs hN)^[k] w₀)

Uses 8

Statement usesLoss-of-function count data for a gene · Strictly positive class weights summing to one · EM update of the Poisson mixture class weights · Joint likelihood of gene data and constraint class · Log-likelihood of a latent-variable model

Proof usesThe M-step maximizes Q(· | w) · Positivity of the Poisson mixture joint likelihood · EM iterates have monotone likelihood

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.