Distribution of fitness effects

23 fully proved

A bound on the expected spectrum

TheoremUniform bound on the expected site-frequency spectrum#✓fully proved

The expected number of sites with i derived copies in a sample of n, 1 ≤ i < n, is bounded uniformly in the selection coefficient: |E ξ_i(σ)| ≤ |θ| C(n, i).

theorem abs_expectedSFS_le (θ σ : ℝ) {n i : ℕ} (hi : 0 < i) (hin : i < n) :
    |expectedSFS θ σ n i| ≤ |θ| * n.choose i

Uses 7 · Used by 1

Statement usesExpected site frequency spectrum under the Poisson random field

Proof usesKimura's fixation probability · Kimura's fixation probability is at most one · Nonnegativity of Kimura's fixation probability · Kimura's fixation probability equals one at frequency one · Kimura's fixation probability vanishes at frequency zero · Sawyer–Hartl Poisson random field density

Used byIntegrability of the expected spectrum in the selection coefficient

Spectra under a distribution of fitness effects

DefinitionSite-frequency spectrum under a distribution of fitness effects#✓fully proved

The expected unfolded site-frequency spectrum under the distribution of fitness effects μ (a law on the scaled selection coefficient σ = 2Ns): ∫ E ξ_i(σ) dμ(σ), where each new mutation draws its own σ from μ.

noncomputable def dfeSFS (μ : Measure ℝ) (θ : ℝ) (n i : ℕ) : ℝ :=
  ∫ σ, expectedSFS θ σ n i ∂μ

Uses 1 · Used by 5

Statement usesExpected site frequency spectrum under the Poisson random field

Used byDFE spectrum is additive in the measure · Spectrum under a point-mass DFE is the single-selection spectrum · Mixture identity · Site-frequency spectrum under the gamma DFE · DFE spectrum is homogeneous in the measure

DefinitionFrequency density averaged over a distribution of fitness effects#✓fully proved

The Poisson-random-field frequency density averaged over the distribution of fitness effects μ: ∫ φ_σ(x) dμ(σ).

noncomputable def dfeDensity (μ : Measure ℝ) (θ x : ℝ) : ℝ :=
  ∫ σ, prfDensity θ σ x ∂μ

Uses 1 · Used by 1

Statement usesSawyer–Hartl Poisson random field density

Used byMixture identity

TheoremIntegrability of the expected spectrum in the selection coefficient#✓fully proved

For 1 ≤ i < n, the expected spectrum E ξ_i(σ) is integrable in σ against every finite measure.

theorem integrable_expectedSFS (μ : Measure ℝ) [IsFiniteMeasure μ] (θ : ℝ) {n i : ℕ}
    (hi : 0 < i) (hin : i < n) : Integrable (fun σ => expectedSFS θ σ n i) μ

Uses 4 · Used by 1

Statement usesExpected site frequency spectrum under the Poisson random field

Proof usesKimura's fixation probability · Sawyer–Hartl Poisson random field density · Uniform bound on the expected site-frequency spectrum

Used byDFE spectrum is additive in the measure

TheoremMixture identity#✓fully proved

For a finite measure μ of selection coefficients and a segregating class 1 ≤ i < n, the DFE-averaged spectrum is the binomial sampling integral of the DFE-averaged frequency density: ∫ E ξ_i(σ) dμ(σ) = ∫₀¹ C(n, i) x ^ i (1 - x) ^ (n - i) (∫ φ_σ(x) dμ(σ)) dx.

theorem dfeSFS_eq_integral_dfeDensity (μ : Measure ℝ) [IsFiniteMeasure μ] (θ : ℝ) {n i : ℕ}
    (hi : 0 < i) (hin : i < n) :
    dfeSFS μ θ n i =
      ∫ x in (0 : ℝ)..1, (n.choose i : ℝ) * x ^ i * (1 - x) ^ (n - i) * dfeDensity μ θ x

Uses 9

Statement usesFrequency density averaged over a distribution of fitness effects · Site-frequency spectrum under a distribution of fitness effects

Proof usesExpected site frequency spectrum under the Poisson random field · Kimura's fixation probability · Kimura's fixation probability is at most one · Nonnegativity of Kimura's fixation probability · Kimura's fixation probability equals one at frequency one · Kimura's fixation probability vanishes at frequency zero · Sawyer–Hartl Poisson random field density

TheoremSpectrum under a point-mass DFE is the single-selection spectrum#✓fully proved

A DFE concentrated on one selection coefficient gives the single-σ spectrum.

theorem dfeSFS_dirac (σ θ : ℝ) (n i : ℕ) :
    dfeSFS (Measure.dirac σ) θ n i = expectedSFS θ σ n i

Uses 2

Statement usesExpected site frequency spectrum under the Poisson random field · Site-frequency spectrum under a distribution of fitness effects

TheoremDFE spectrum is additive in the measure#✓fully proved

The spectrum is additive in the (finite) DFE.

theorem dfeSFS_add_measure (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (θ : ℝ)
    {n i : ℕ} (hi : 0 < i) (hin : i < n) :
    dfeSFS (μ + ν) θ n i = dfeSFS μ θ n i + dfeSFS ν θ n i

Uses 3

Statement usesSite-frequency spectrum under a distribution of fitness effects

Proof usesExpected site frequency spectrum under the Poisson random field · Integrability of the expected spectrum in the selection coefficient

TheoremDFE spectrum is homogeneous in the measure#✓fully proved

The spectrum is homogeneous in the DFE.

theorem dfeSFS_smul_measure (c : ℝ≥0∞) (μ : Measure ℝ) (θ : ℝ) (n i : ℕ) :
    dfeSFS (c • μ) θ n i = c.toReal * dfeSFS μ θ n i

Uses 2

Statement usesSite-frequency spectrum under a distribution of fitness effects

Proof usesExpected site frequency spectrum under the Poisson random field

The gamma DFE

DefinitionGamma distribution of fitness effects#✓fully proved

The gamma distribution of fitness effects (Boyko et al. 2008): the scaled selection coefficient is σ = -T with T ~ Gamma(a, r), shape a > 0 and rate r > 0 (scale 1 / r), so new mutations are deleterious with mean strength a / r.

noncomputable def gammaDFE (a r : ℝ) : Measure ℝ :=
  (gammaMeasure a r).map Neg.neg

Used by 8

Used bySite-frequency spectrum under the gamma DFE · No mutation is beneficial under the gamma DFE · Rescaling a gamma DFE divides its rate · Fraction of mutations in a strength interval under the gamma DFE · Fraction of strongly deleterious mutations · Mean selection coefficient under the gamma DFE · Gamma DFE is a probability measure · Variance of the selection coefficient under the gamma DFE

TheoremGamma DFE is a probability measure#✓fully proved

The gamma DFE is a probability law.

theorem isProbabilityMeasure_gammaDFE {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    IsProbabilityMeasure (gammaDFE a r)

Uses 1

Statement usesGamma distribution of fitness effects

TheoremNo mutation is beneficial under the gamma DFE#✓fully proved

Under the gamma DFE no mutation is beneficial.

theorem gammaDFE_Ioi_zero (a r : ℝ) : gammaDFE a r (Ioi 0) = 0

Uses 1

Statement usesGamma distribution of fitness effects

TheoremMean selection coefficient under the gamma DFE#✓fully proved

The mean scaled selection coefficient under the gamma DFE is -a / r.

theorem integral_id_gammaDFE {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    ∫ σ, σ ∂gammaDFE a r = -(a / r)

Uses 2

Statement usesGamma distribution of fitness effects

Proof usesMean of the gamma law

TheoremVariance of the selection coefficient under the gamma DFE#✓fully proved

The variance of the scaled selection coefficient under the gamma DFE is a / r ^ 2.

theorem variance_id_gammaDFE {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    variance id (gammaDFE a r) = a / r ^ 2

Uses 2

Statement usesGamma distribution of fitness effects

Proof usesVariance of the gamma law

TheoremRescaling a gamma DFE divides its rate#✓fully proved

Rescaling a gamma DFE by c > 0 (for example from s to σ = 2Ns, c = 2N) keeps the shape and divides the rate by c.

theorem gammaDFE_map_const_mul {a r c : ℝ} (ha : 0 < a) (hr : 0 < r) (hc : 0 < c) :
    (gammaDFE a r).map (fun σ => c * σ) = gammaDFE a (r / c)

Uses 2

Statement usesGamma distribution of fitness effects

Proof usesScaling a gamma random variable

TheoremFraction of strongly deleterious mutations#✓fully proved

Under the gamma DFE the fraction of new mutations with σ < -c, c ≥ 0, is the gamma tail Γ(a, r c) / Γ(a).

theorem gammaDFE_real_Iio {a r c : ℝ} (ha : 0 < a) (hr : 0 < r) (hc : 0 ≤ c) :
    (gammaDFE a r).real (Iio (-c)) = upperIncompleteGamma a (r * c) / Gamma a

Uses 3

Statement usesGamma distribution of fitness effects · Upper incomplete gamma function

Proof usesUpper tail of the gamma law

TheoremFraction of mutations in a strength interval under the gamma DFE#✓fully proved

The fraction of new mutations whose strength -σ lies in (c₁, c₂], 0 ≤ c₁ ≤ c₂, is (Γ(a, r c₁) - Γ(a, r c₂)) / Γ(a).

theorem gammaDFE_real_Ico {a r c₁ c₂ : ℝ} (ha : 0 < a) (hr : 0 < r) (hc₁ : 0 ≤ c₁)
    (hc : c₁ ≤ c₂) :
    (gammaDFE a r).real (Ico (-c₂) (-c₁)) =
      (upperIncompleteGamma a (r * c₁) - upperIncompleteGamma a (r * c₂)) / Gamma a

Uses 3

Statement usesGamma distribution of fitness effects · Upper incomplete gamma function

Proof usesUpper tail of the gamma law

TheoremSite-frequency spectrum under the gamma DFE#✓fully proved

The spectrum under the gamma DFE as an integral against the gamma law of the strength.

theorem dfeSFS_gammaDFE (a r θ : ℝ) (n i : ℕ) :
    dfeSFS (gammaDFE a r) θ n i = ∫ t, expectedSFS θ (-t) n i ∂gammaMeasure a r

Uses 3

Statement usesExpected site frequency spectrum under the Poisson random field · Site-frequency spectrum under a distribution of fitness effects · Gamma distribution of fitness effects

The Poisson likelihood of the spectrum

DefinitionPoisson log-likelihood of counts#✓fully proved

The Poisson log-likelihood ∑ (k_i log E_i - E_i - log k_i!) of counts k_i with means E_i. Meaningful for E_i > 0; at E_i = 0 Lean's log 0 = 0 gives a junk value.

noncomputable def poissonLogLik (E : ι → ℝ) (k : ι → ℕ) : ℝ :=
  ∑ i, ((k i : ℝ) * log (E i) - E i - log (Nat.factorial (k i)))

Used by 4

Used byDerivative of the Poisson log-likelihood · The Poisson-random-field log-likelihood · Profile maximum in θ · Score equations

TheoremProbability of a count vector under independent Poisson laws#✓fully proved

The joint law of independent Poisson counts with means E_i gives the count vector k the probability ∏ e^{-E_i} E_i ^ {k_i} / (k_i!).

theorem pi_poissonMeasure_real_singleton (E : ι → ℝ≥0) (k : ι → ℕ) :
    (Measure.pi fun i => poissonMeasure (E i)).real {k} =
      ∏ i, exp (-(E i : ℝ)) * (E i : ℝ) ^ k i / Nat.factorial (k i)

Used by 1

Used byThe Poisson-random-field log-likelihood

TheoremThe Poisson-random-field log-likelihood#✓fully proved

For independent Poisson counts with positive means E_i, the log-probability of the observed counts k is poissonLogLik E k.

theorem log_pi_poissonMeasure_real_singleton (E : ι → ℝ≥0) (hE : ∀ i, 0 < E i) (k : ι → ℕ) :
    log ((Measure.pi fun i => poissonMeasure (E i)).real {k}) =
      poissonLogLik (fun i => (E i : ℝ)) k

Uses 2

Statement usesPoisson log-likelihood of counts

Proof usesProbability of a count vector under independent Poisson laws

TheoremDerivative of the Poisson log-likelihood#✓fully proved

The derivative of the log-likelihood in the parameter ψ, when the means E_i(ψ) are positive and differentiable at ψ: ∑ (k_i / E_i(ψ) - 1) · DE_i(ψ).

theorem hasFDerivAt_poissonLogLik {E : ι → V → ℝ} {ψ : V}
    (hE : ∀ i, DifferentiableAt ℝ (E i) ψ) (hpos : ∀ i, 0 < E i ψ) (k : ι → ℕ) :
    HasFDerivAt (fun φ => poissonLogLik (fun i => E i φ) k)
      (∑ i, ((k i : ℝ) / E i ψ - 1) • fderiv ℝ (E i) ψ) ψ

Uses 1 · Used by 1

Statement usesPoisson log-likelihood of counts

Used byScore equations

TheoremScore equations#✓fully proved

If ψ maximizes the Poisson log-likelihood over a parameter set S that is a neighborhood of ψ, and the means are positive and differentiable at ψ, then ∑ (k_i / E_i(ψ) - 1) · DE_i(ψ) = 0.

theorem score_eq_zero_of_isMaxOn {E : ι → V → ℝ} {ψ : V} {S : Set V} (k : ι → ℕ)
    (hS : S ∈ 𝓝 ψ) (hmax : IsMaxOn (fun φ => poissonLogLik (fun i => E i φ) k) S ψ)
    (hE : ∀ i, DifferentiableAt ℝ (E i) ψ) (hpos : ∀ i, 0 < E i ψ) :
    ∑ i, ((k i : ℝ) / E i ψ - 1) • fderiv ℝ (E i) ψ = 0

Uses 2

Statement usesPoisson log-likelihood of counts

Proof usesDerivative of the Poisson log-likelihood

TheoremProfile maximum in θ#✓fully proved

With means E_i = θ f_i linear in the mutation parameter, positive f_i and at least one count, every θ > 0 has likelihood at most that of θ̂ = ∑ k_i / ∑ f_i.

theorem poissonLogLik_le_profile {f : ι → ℝ} (hf : ∀ i, 0 < f i) (k : ι → ℕ)
    (hk : 0 < ∑ i, k i) {θ : ℝ} (hθ : 0 < θ) :
    poissonLogLik (fun i => θ * f i) k ≤
      poissonLogLik (fun i => (∑ j, (k j : ℝ)) / (∑ j, f j) * f i) k

Uses 1

Statement usesPoisson log-likelihood of counts

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.