Replicator dynamics

9 fully proved

Replicator

DefinitionMean fitness of a population state#✓fully proved

The mean fitness f̄(x) = ∑ i, x i * f x i of the population state x for the fitness function f.

def meanFitness (f : (ι → ℝ) → ι → ℝ) (x : ι → ℝ) : ℝ :=
  ∑ i, x i * f x i

Used by 7

Used byInvariance of the faces of the simplex · Evolution of the total frequency under replicator dynamics · Rest point of the replicator equation · Rest points in the interior are equalizers · Solution of the replicator equation · Present strategies stay present · Invariance of the simplex hyperplane

StructureSolution of the replicator equation#✓fully proved

x solves the replicator equation x_i' = x_i (f_i(x) - f̄(x)) for all times t ≥ 0.

structure IsSolution (f : (ι → ℝ) → ι → ℝ) (x : ℝ → ι → ℝ) : Prop where
  /-- Each frequency grows at the rate of its excess fitness. -/
  hasDerivAt : ∀ i t, 0 ≤ t →
    HasDerivAt (fun s => x s i) (x t i * (f (x t) i - meanFitness f (x t))) t

Uses 1 · Used by 5

Statement usesMean fitness of a population state

Used byInvariance of the faces of the simplex · Evolution of the total frequency under replicator dynamics · Invariance of the simplex (Hofbauer–Sigmund 1998, §7.1) · Present strategies stay present · Invariance of the simplex hyperplane

DefinitionRest point of the replicator equation#✓fully proved

x is a rest point of the replicator equation: x_i (f_i(x) - f̄(x)) = 0 for all i.

def IsRestPoint (f : (ι → ℝ) → ι → ℝ) (x : ι → ℝ) : Prop :=
  ∀ i, x i * (f x i - meanFitness f x) = 0

Uses 1 · Used by 1

Statement usesMean fitness of a population state

Used byRest points in the interior are equalizers

TheoremRest points in the interior are equalizers#✓fully proved

If every strategy is present (x i > 0), then x is a rest point iff every strategy has fitness equal to the mean fitness.

theorem isRestPoint_iff {f : (ι → ℝ) → ι → ℝ} {x : ι → ℝ} (hx : ∀ i, 0 < x i) :
    IsRestPoint f x ↔ ∀ i, f x i = meanFitness f x

Uses 2

Statement usesRest point of the replicator equation · Mean fitness of a population state

Is Solution

TheoremEvolution of the total frequency under replicator dynamics#✓fully proved

The total frequency ∑ x_i evolves by (∑ x_i)' = f̄(x) (1 - ∑ x_i).

theorem hasDerivAt_sum (h : IsSolution f x) {t : ℝ} (ht : 0 ≤ t) :
    HasDerivAt (fun s => ∑ i, x s i) (meanFitness f (x t) * (1 - ∑ i, x t i)) t

Uses 2 · Used by 1

Statement usesSolution of the replicator equation · Mean fitness of a population state

Used byInvariance of the simplex hyperplane

TheoremInvariance of the simplex hyperplane#✓fully proved

For continuous fitness f, a solution with ∑ x_i(0) = 1 satisfies ∑ x_i(t) = 1 for all t ≥ 0.

theorem sum_eq_one (h : IsSolution f x) (hf : Continuous f) (h0 : ∑ i, x 0 i = 1) {t : ℝ}
    (ht : 0 ≤ t) : ∑ i, x t i = 1

Uses 3 · Used by 1

Statement usesSolution of the replicator equation

Proof usesEvolution of the total frequency under replicator dynamics · Mean fitness of a population state

Used byInvariance of the simplex (Hofbauer–Sigmund 1998, §7.1)

TheoremInvariance of the faces of the simplex#✓fully proved

For continuous fitness f, a strategy absent at time 0 (x_i(0) = 0) stays absent for all t ≥ 0.

theorem eq_zero_of_eq_zero (h : IsSolution f x) (hf : Continuous f) {i : ι} (h0 : x 0 i = 0)
    {t : ℝ} (ht : 0 ≤ t) : x t i = 0

Uses 2 · Used by 1

Statement usesSolution of the replicator equation

Proof usesMean fitness of a population state

Used byInvariance of the simplex (Hofbauer–Sigmund 1998, §7.1)

TheoremPresent strategies stay present#✓fully proved

For continuous fitness f, a strategy with positive frequency at time 0 has positive frequency for all t ≥ 0.

theorem pos_of_pos (h : IsSolution f x) (hf : Continuous f) {i : ι} (h0 : 0 < x 0 i)
    {t : ℝ} (ht : 0 ≤ t) : 0 < x t i

Uses 2 · Used by 1

Statement usesSolution of the replicator equation

Proof usesMean fitness of a population state

Used byInvariance of the simplex (Hofbauer–Sigmund 1998, §7.1)

TheoremInvariance of the simplex (Hofbauer–Sigmund 1998, §7.1)#✓fully proved

For continuous fitness f, a solution starting in the standard simplex (x i ≥ 0 for all i and ∑ i, x i = 1) stays in it for all t ≥ 0.

theorem mem_simplex (h : IsSolution f x) (hf : Continuous f) (h0 : ∀ i, 0 ≤ x 0 i)
    (h1 : ∑ i, x 0 i = 1) {t : ℝ} (ht : 0 ≤ t) : (∀ i, 0 ≤ x t i) ∧ ∑ i, x t i = 1

Uses 4

Statement usesSolution of the replicator equation

Proof usesInvariance of the faces of the simplex · Present strategies stay present · Invariance of the simplex hyperplane

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.