Lande's selection gradient

TheoremStein's lemma#✓fully proved

Stein's lemma for the normal law N(μ, v), v > 0: if g is differentiable with derivative g' and g, (z - μ) g z and g' are integrable, then 𝔼[(z - μ) g z] = v 𝔼[g' z] (Stein 1981, Lemma 1).

theorem integral_sub_mul_gaussianReal {μ : ℝ} {v : ℝ≥0} (hv : v ≠ 0) {g g' : ℝ → ℝ}
    (hg : ∀ x, HasDerivAt g (g' x) x) (hgi : Integrable g (gaussianReal μ v))
    (hxg : Integrable (fun x => (x - μ) * g x) (gaussianReal μ v))
    (hg' : Integrable g' (gaussianReal μ v)) :
    ∫ x, (x - μ) * g x ∂gaussianReal μ v = v * ∫ x, g' x ∂gaussianReal μ v

Used by 1

Used byThe Lande–Arnold selection gradient

DefinitionMean fitness of a normally distributed trait#✓fully proved

The mean fitness w̄(μ) = 𝔼[W z] of a population whose trait is distributed as N(μ, v).

noncomputable def meanFitness (W : ℝ → ℝ) (μ : ℝ) (v : ℝ≥0) : ℝ :=
  ∫ z, W z ∂gaussianReal μ v

Used by 4

Used byDerivative of mean fitness with respect to the trait mean · Directional selection differential · The Lande–Arnold selection gradient · Lande's equation

DefinitionDirectional selection differential#✓fully proved

The directional selection differential S = 𝔼[(z - μ) W z] / w̄: the mean trait of the selected parents, weighting each individual by its fitness, minus the mean trait μ before selection. If w̄ = 0 the division returns the junk value 0.

noncomputable def selectionDifferential (W : ℝ → ℝ) (μ : ℝ) (v : ℝ≥0) : ℝ :=
  (∫ z, (z - μ) * W z ∂gaussianReal μ v) / meanFitness W μ v

Uses 1 · Used by 2

Statement usesMean fitness of a normally distributed trait

Used byThe Lande–Arnold selection gradient · Lande's equation

TheoremDerivative of mean fitness with respect to the trait mean#✓fully proved

The derivative of mean fitness with respect to the trait mean is d/dμ w̄(μ) = 𝔼[(z - μ) W z] / v, for bounded measurable fitness and v > 0.

theorem hasDerivAt_meanFitness {W : ℝ → ℝ} (hWm : Measurable W) (hWb : ∃ C, ∀ z, |W z| ≤ C)
    {v : ℝ≥0} (hv : v ≠ 0) (μ : ℝ) :
    HasDerivAt (fun m => meanFitness W m v)
      ((∫ z, (z - μ) * W z ∂gaussianReal μ v) / v) μ

Uses 1 · Used by 1

Statement usesMean fitness of a normally distributed trait

Used byLande's equation

TheoremLande's equation#✓fully proved

Lande's equation for one normally distributed trait (Lande 1979): the selection differential is the phenotypic variance times the derivative of log mean fitness with respect to the trait mean, S = v · d/dμ log w̄(μ).

theorem selectionDifferential_eq_mul_deriv_log {W : ℝ → ℝ} (hWm : Measurable W)
    (hWb : ∃ C, ∀ z, |W z| ≤ C) {v : ℝ≥0} (hv : v ≠ 0) {μ : ℝ} (hw : meanFitness W μ v ≠ 0) :
    selectionDifferential W μ v = v * deriv (fun m => Real.log (meanFitness W m v)) μ

Uses 3

Statement usesMean fitness of a normally distributed trait · Directional selection differential

Proof usesDerivative of mean fitness with respect to the trait mean

TheoremThe Lande–Arnold selection gradient#✓fully proved

The Lande–Arnold selection gradient for one normally distributed trait: for a differentiable bounded fitness function with integrable derivative, β = S / v = 𝔼[W' z] / w̄, the average slope of relative fitness W / w̄ (Lande–Arnold 1983).

theorem selectionDifferential_div_eq {W W' : ℝ → ℝ} (hW : ∀ z, HasDerivAt W (W' z) z)
    (hWb : ∃ C, ∀ z, |W z| ≤ C) {μ : ℝ} {v : ℝ≥0} (hv : v ≠ 0)
    (hW' : Integrable W' (gaussianReal μ v)) :
    selectionDifferential W μ v / v = (∫ z, W' z ∂gaussianReal μ v) / meanFitness W μ v

Uses 3

Statement usesMean fitness of a normally distributed trait · Directional selection differential

Proof usesStein's lemma

DefinitionMean fitness of a multivariate normal trait#✓fully proved

The mean fitness w̄(μ) = 𝔼[W z] of a population whose trait vector is distributed as N(μ, P).

noncomputable def meanFitnessMV (W : EuclideanSpace ℝ ι → ℝ) (P : Matrix ι ι ℝ)
    (μ : EuclideanSpace ℝ ι) : ℝ :=
  ∫ z, W z ∂multivariateGaussian μ P

Used by 3

Used byLande's gradient of mean fitness for multivariate traits · Multivariate directional selection differential · Lande's equation

DefinitionMultivariate directional selection differential#✓fully proved

The directional selection differential S = 𝔼[W z · (z - μ)] / w̄ of a trait vector distributed as N(μ, P): the fitness-weighted mean trait vector of the selected parents minus the mean μ before selection. If w̄ = 0 it is the junk value 0.

noncomputable def selectionDifferentialMV (W : EuclideanSpace ℝ ι → ℝ) (P : Matrix ι ι ℝ)
    (μ : EuclideanSpace ℝ ι) : EuclideanSpace ℝ ι :=
  (meanFitnessMV W P μ)⁻¹ • ∫ z, W z • (z - μ) ∂multivariateGaussian μ P

Uses 1 · Used by 1

Statement usesMean fitness of a multivariate normal trait

Used byLande's equation

TheoremLande's gradient of mean fitness for multivariate traits#✓fully proved

The gradient of mean fitness with respect to the vector of trait means is ∇_μ w̄(μ) = P⁻¹ 𝔼[W z · (z - μ)], for positive definite P and bounded measurable W.

theorem hasGradientAt_meanFitnessMV {W : EuclideanSpace ℝ ι → ℝ} (hWm : Measurable W)
    (hWb : ∃ C, ∀ z, |W z| ≤ C) {P : Matrix ι ι ℝ} (hP : P.PosDef) (μ : EuclideanSpace ℝ ι) :
    HasGradientAt (meanFitnessMV W P)
      (toEuclideanCLM (𝕜 := ℝ) P⁻¹ (∫ z, W z • (z - μ) ∂multivariateGaussian μ P)) μ

Uses 6 · Used by 1

Statement usesMean fitness of a multivariate normal trait

Proof usesThe affine change of variables as a measurable equivalence · Lebesgue measure under an invertible affine map · Multivariate Gaussian density function · The multivariate Gaussian density · Quadratic form of the inverse square root

Used byLande's equation

TheoremLande's equation#✓fully proved

Lande's equation (Lande 1979): for a multivariate normal trait vector, the selection differential is the phenotypic covariance matrix applied to the gradient of log mean fitness with respect to the trait means, S = P ∇_μ log w̄(μ).

theorem selectionDifferentialMV_eq {W : EuclideanSpace ℝ ι → ℝ} (hWm : Measurable W)
    (hWb : ∃ C, ∀ z, |W z| ≤ C) {P : Matrix ι ι ℝ} (hP : P.PosDef) {μ : EuclideanSpace ℝ ι}
    (hw : meanFitnessMV W P μ ≠ 0) :
    selectionDifferentialMV W P μ =
      toEuclideanCLM (𝕜 := ℝ) P (gradient (fun m => Real.log (meanFitnessMV W P m)) μ)

Uses 3

Statement usesMean fitness of a multivariate normal trait · Multivariate directional selection differential

Proof usesLande's gradient of mean fitness for multivariate traits

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.