The Moran process and the isothermal theorem (MOR-1, MOR-2)

Birth–death Moran process on a finite graph: mutants have fitness r > 0, residents fitness 1. In each step a parent is chosen with probability proportional to its fitness, and its offspring replaces a uniformly random neighbour (an isolated parent replaces itself, so nothing changes).

On a regular graph, in every configuration a step increases the number of mutants with exactly r times the probability that it decreases it. Hence (1/r)^(#mutants) is invariant in expectation, and on a connected regular graph the fixation probability from k mutants is Moran's formula (1 - r^{-k}) / (1 - r^{-n}) (for r ≠ 1), or k/n in the neutral case. This is the "if" direction of the isothermal theorem of Lieberman, Hauert and Nowak (2005); the complete graph gives Moran's classical formula (1958).

@[reducible, inline]

abbrev Moran.Config (V : Type u_2) : Type u_2

A configuration marks each vertex as mutant (true) or resident (false).

Equations

• Moran.Config V = (V → Bool)

def Moran.mutants {V : Type u_1} [Fintype V] (s : Config V) : ℕ

Number of mutants.

Equations

• Moran.mutants s = {i : V | s i = true}.card

def Moran.fitness {V : Type u_1} (r : ℝ) (s : Config V) (u : V) : ℝ

Fitness: r for mutants, 1 for residents.

Equations

• Moran.fitness r s u = if s u = true then r else 1

def Moran.totalFitness {V : Type u_1} [Fintype V] (r : ℝ) (s : Config V) : ℝ

Total fitness of the population.

Equations

• Moran.totalFitness r s = ∑ u : V, Moran.fitness r s u

noncomputable def Moran.target {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u w : V) : ℝ

Offspring placement: a uniformly random neighbour of the parent u, or u itself if it has no neighbour.

Equations

• Moran.target G u w = if G.degree u = 0 then if w = u then 1 else 0 else if G.Adj u w then (↑(G.degree u))⁻¹ else 0

theorem Moran.fitness_pos {V : Type u_1} {r : ℝ} (hr : 0 < r) (s : Config V) (u : V) : 0 < fitness r s u

theorem Moran.totalFitness_nonneg {V : Type u_1} [Fintype V] {r : ℝ} (hr : 0 < r) (s : Config V) : 0 ≤ totalFitness r s

theorem Moran.totalFitness_pos {V : Type u_1} [Fintype V] [Nonempty V] {r : ℝ} (hr : 0 < r) (s : Config V) : 0 < totalFitness r s

theorem Moran.target_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u w : V) : 0 ≤ target G u w

theorem Moran.target_sum_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u : V) : ∑ w : V, target G u w = 1

theorem Moran.pair_weight_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (s : Config V) (p : V × V) : 0 ≤ fitness r s p.1 / totalFitness r s * target G p.1 p.2

The weights of (parent, offspring position) pairs are nonnegative.

theorem Moran.pair_weight_sum_one {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (s : Config V) : ∑ p : V × V, fitness r s p.1 / totalFitness r s * target G p.1 p.2 = 1

The weights of (parent, offspring position) pairs sum to one.

noncomputable def Moran.pairDist {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℝ) (hr : 0 < r) (s : Config V) : Dynamics.Distribution (V × V)

Distribution of the (parent, offspring position) pair in one Birth–death step.

Equations

• Moran.pairDist G r hr s = { weight := fun (p : V × V) => Moran.fitness r s p.1 / Moran.totalFitness r s * Moran.target G p.1 p.2, nonneg := ⋯, sum_one := ⋯ }

noncomputable def Moran.moranKernel {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℝ) (hr : 0 < r) : Dynamics.Kernel (Config V)

The Birth–death Moran kernel: the offspring copies the parent's type.

Equations

• Moran.moranKernel G r hr s = (Moran.pairDist G r hr s).map fun (p : V × V) => Function.update s p.2 (s p.1)

def Moran.allMutant {V : Type u_1} [Fintype V] (s : Config V) : ℝ

Indicator of fixation (every vertex is a mutant).

Equations

• Moran.allMutant s = if s = fun (x : V) => true then 1 else 0

noncomputable def Moran.unfixed {V : Type u_1} [Fintype V] (s : Config V) : ℝ

Indicator that neither type has taken over yet.

Equations

• Moran.unfixed s = if ∃ (c : Bool), s = fun (x : V) => c then 0 else 1

noncomputable def Moran.fixation {V : Type u_1} [Fintype V] [DecidableEq V] (K : Dynamics.Kernel (Config V)) (s : Config V) : ℝ

Fixation probability: the supremum of the finite-time fixation probabilities.

Equations

• Moran.fixation K s = ⨆ (t : ℕ), K.iterate t Moran.allMutant s

theorem Moran.mutants_le_card {V : Type u_1} [Fintype V] (s : Config V) : mutants s ≤ Fintype.card V

theorem Moran.mutants_true {V : Type u_1} [Fintype V] {s : Config V} (h : s = fun (x : V) => true) : mutants s = Fintype.card V

theorem Moran.mutants_false {V : Type u_1} [Fintype V] {s : Config V} (h : s = fun (x : V) => false) : mutants s = 0

theorem Moran.config_of_mutants_eq_card {V : Type u_1} [Fintype V] {s : Config V} (h : mutants s = Fintype.card V) : s = fun (x : V) => true

theorem Moran.mutants_update_gain {V : Type u_1} [Fintype V] [DecidableEq V] (s : Config V) {w : V} (hw : s w = false) : mutants (Function.update s w true) = mutants s + 1

theorem Moran.mutants_update_loss {V : Type u_1} [Fintype V] [DecidableEq V] (s : Config V) {w : V} (hw : s w = true) : mutants (Function.update s w false) = mutants s - 1

theorem Moran.mutants_pos_of_true {V : Type u_1} [Fintype V] {s : Config V} {w : V} (hw : s w = true) : 1 ≤ mutants s

theorem Moran.div_mul_inv_eq (a b c : ℝ) : a / b * c⁻¹ = a / (b * c)

theorem Moran.one_div_pow_pred {r : ℝ} (hr : r ≠ 0) {k : ℕ} (hk : 1 ≤ k) : (1 / r) ^ (k - 1) = (1 / r) ^ k * r

def Moran.upInd {V : Type u_1} (s : Config V) (p : V × V) : ℝ

1 when a mutant parent replaces a resident, else 0.

Equations

• Moran.upInd s p = if s p.1 = true ∧ s p.2 = false then 1 else 0

def Moran.downInd {V : Type u_1} (s : Config V) (p : V × V) : ℝ

1 when a resident parent replaces a mutant, else 0.

Equations

• Moran.downInd s p = if s p.1 = false ∧ s p.2 = true then 1 else 0

def Moran.orientedCut {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : Config V) (b : Bool) : ℝ

Number of oriented edges from type b to the opposite type.

Equations

• Moran.orientedCut G s b = ∑ p : V × V, if s p.1 = b ∧ s p.2 = !b ∧ G.Adj p.1 p.2 then 1 else 0

theorem Moran.orientedCut_symm {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : Config V) (b : Bool) : orientedCut G s b = orientedCut G s !b

@[simp]

theorem Moran.pairDist_weight {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℝ) (hr : 0 < r) (s : Config V) (p : V × V) : (pairDist G r hr s).weight p = fitness r s p.1 / totalFitness r s * target G p.1 p.2

noncomputable def Moran.birthMass {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℝ) (hr : 0 < r) (s : Config V) : ℝ

Total weight of mutant-increasing steps.

Equations

• Moran.birthMass G r hr s = ∑ p : V × V, (Moran.pairDist G r hr s).weight p * Moran.upInd s p

noncomputable def Moran.deathMass {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℝ) (hr : 0 < r) (s : Config V) : ℝ

Total weight of mutant-decreasing steps.

Equations

• Moran.deathMass G r hr s = ∑ p : V × V, (Moran.pairDist G r hr s).weight p * Moran.downInd s p

theorem Moran.mass_isolated {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (s : Config V) (hdeg : ∀ (i : V), G.degree i = 0) (b : Bool) : (∑ p : V × V, (pairDist G r hr s).weight p * if s p.1 = b ∧ s p.2 = !b then 1 else 0) = 0

theorem Moran.typed_mass {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hd : d ≠ 0) (hreg : ∀ (i : V), G.degree i = d) {r : ℝ} (hr : 0 < r) (s : Config V) (b : Bool) (c : ℝ) (hfit : ∀ (u : V), s u = b → fitness r s u = c) : (∑ p : V × V, (pairDist G r hr s).weight p * if s p.1 = b ∧ s p.2 = !b then 1 else 0) = c / (totalFitness r s * ↑d) * orientedCut G s b

theorem Moran.birth_indicator {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℝ) (hr : 0 < r) (s : Config V) : birthMass G r hr s = ∑ p : V × V, (pairDist G r hr s).weight p * if s p.1 = true ∧ s p.2 = !true then 1 else 0

theorem Moran.death_indicator {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℝ) (hr : 0 < r) (s : Config V) : deathMass G r hr s = ∑ p : V × V, (pairDist G r hr s).weight p * if s p.1 = false ∧ s p.2 = !false then 1 else 0

theorem Moran.birth_eq_r_death {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (hreg : ∀ (i : V), G.degree i = d) {r : ℝ} (hr : 0 < r) (s : Config V) : birthMass G r hr s = r * deathMass G r hr s

On a regular graph the probability of gaining a mutant is r times the probability of losing one.

theorem Moran.pot_after {V : Type u_1} [Fintype V] [DecidableEq V] {r : ℝ} (hr0 : r ≠ 0) (s : Config V) (u w : V) : (1 / r) ^ mutants (Function.update s w (s u)) = (1 / r) ^ mutants s + (1 / r) ^ mutants s * (1 / r - 1) * upInd s (u, w) + (1 / r) ^ mutants s * (r - 1) * downInd s (u, w)

theorem Moran.mutants_after {V : Type u_1} [Fintype V] [DecidableEq V] (s : Config V) (u w : V) : ↑(mutants (Function.update s w (s u))) = ↑(mutants s) + 1 * upInd s (u, w) + -1 * downInd s (u, w)

theorem Moran.apply_affine {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (s : Config V) (f : Config V → ℝ) (cUp cDown : ℝ) (hupd : ∀ (u w : V), f (Function.update s w (s u)) = f s + cUp * upInd s (u, w) + cDown * downInd s (u, w)) : (moranKernel G r hr).apply f s = f s + cUp * birthMass G r hr s + cDown * deathMass G r hr s

theorem Moran.moran_potential_invariant {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (hreg : ∀ (i : V), G.degree i = d) {r : ℝ} (hr : 0 < r) (s : Config V) : (moranKernel G r hr).apply (fun (t : Config V) => (1 / r) ^ mutants t) s = (1 / r) ^ mutants s

Invariance. On a regular graph, (1/r)^(#mutants) is preserved in expectation by one Moran step.

theorem Moran.moran_mutants_invariant {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (hreg : ∀ (i : V), G.degree i = d) (s : Config V) : (moranKernel G 1 ⋯).apply (fun (t : Config V) => ↑(mutants t)) s = ↑(mutants s)

Neutral invariance. On a regular graph with r = 1, the number of mutants is preserved in expectation by one Moran step.

theorem Moran.unfixed_binary {V : Type u_1} [Fintype V] (s : Config V) : unfixed s = 0 ∨ unfixed s = 1

theorem Moran.unfixed_const {V : Type u_1} [Fintype V] (c : Bool) : (unfixed fun (x : V) => c) = 0

theorem Moran.unfixed_of_mixed {V : Type u_1} [Fintype V] (s : Config V) (h : ¬∃ (c : Bool), s = fun (x : V) => c) : unfixed s = 1

theorem Moran.unfixed_le_one {V : Type u_1} [Fintype V] (s : Config V) : unfixed s ≤ 1

theorem Moran.allMutant_nonneg {V : Type u_1} [Fintype V] (s : Config V) : 0 ≤ allMutant s

theorem Moran.allMutant_true {V : Type u_1} [Fintype V] : (allMutant fun (x : V) => true) = 1

theorem Moran.moran_constant {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (c : Bool) (f : Config V → ℝ) : ((moranKernel G r hr).apply f fun (x : V) => c) = f fun (x : V) => c

theorem Moran.expect_lt_one {α : Type u_2} [Fintype α] (p : Dynamics.Distribution α) (f : α → ℝ) (hf : ∀ (a : α), f a ≤ 1) (b : α) (hb : 0 < p.weight b) (hfb : f b < 1) : p.expect f < 1

theorem Moran.map_weight_pos {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (p : Dynamics.Distribution α) (f : α → β) (a : α) (ha : 0 < p.weight a) : 0 < (p.map f).weight (f a)

theorem Moran.moran_weight_pos {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (s : Config V) {u w : V} (hadj : G.Adj u w) (hu : s u = true) : 0 < (moranKernel G r hr s).weight (Function.update s w true)

theorem Moran.unfixed_step {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (s : Config V) : (moranKernel G r hr).apply unfixed s ≤ unfixed s

theorem Moran.unfixed_access {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) {r : ℝ} (hr : 0 < r) (s : Config V) : ∃ (n : ℕ), (moranKernel G r hr).iterate n unfixed s < 1

theorem Moran.moran_unfixed_tendsto {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) {r : ℝ} (hr : 0 < r) (s : Config V) : Filter.Tendsto (fun (t : ℕ) => (moranKernel G r hr).iterate t unfixed s) Filter.atTop (nhds 0)

Absorption. On a connected graph, the probability that neither type has fixed tends to zero.

theorem Moran.allMutant_step {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℝ} (hr : 0 < r) (s : Config V) : allMutant s ≤ (moranKernel G r hr).apply allMutant s

theorem Moran.iterate_allMutant {V : Type u_1} [Fintype V] [DecidableEq V] (K : Dynamics.Kernel (Config V)) (n : ℕ) (s : Config V) : K.iterate n allMutant s = K.event (fun (x : Config V) => x = fun (x : V) => true) n s

Finite-time fixation is the event that every vertex is a mutant.

theorem Moran.unfixed_eq {V : Type u_1} [Fintype V] (s : Config V) : unfixed s = if (¬s = fun (x : V) => true) ∧ ¬s = fun (x : V) => false then 1 else 0

unfixed indicates the configurations that are neither all-mutant nor all-resident.

theorem Moran.iterate_unfixed {V : Type u_1} [Fintype V] [DecidableEq V] (K : Dynamics.Kernel (Config V)) (n : ℕ) (s : Config V) : K.iterate n unfixed s = K.event (fun (t : Config V) => (¬t = fun (x : V) => true) ∧ ¬t = fun (x : V) => false) n s

Finite-time survival (no fixation yet) as an event.

theorem Moran.fixation_eq_of_invariant {V : Type u_1} [Fintype V] [DecidableEq V] (K : Dynamics.Kernel (Config V)) (ψ : Config V → ℝ) (hinv : K.apply ψ = ψ) (hone : (ψ fun (x : V) => true) = 1) (hzero : (ψ fun (x : V) => false) = 0) (habs : ∀ (t : Config V), allMutant t ≤ K.apply allMutant t) (s : Config V) (hsurv : Filter.Tendsto (fun (n : ℕ) => K.iterate n unfixed s) Filter.atTop (nhds 0)) : fixation K s = ψ s

Fixation probability from an invariant (finite-horizon optional stopping, roadmap FND-4). If ψ is harmonic for K, equals 1 on the all-mutant and 0 on the all-resident configuration, all-mutant is absorbing, and the probability that neither type has fixed tends to zero, then ψ is the fixation probability. This is Dynamics.Kernel.iSup_event_of_invariant for the two consensus configurations.

theorem Moran.one_div_pow_ne_one {r : ℝ} (hr : 0 < r) (hr1 : r ≠ 1) {n : ℕ} (hn : n ≠ 0) : (1 / r) ^ n ≠ 1

noncomputable def Moran.moranPsi {V : Type u_1} [Fintype V] (r : ℝ) (t : Config V) : ℝ

Equations

• Moran.moranPsi r t = (1 - (1 / r) ^ Moran.mutants t) / (1 - (1 / r) ^ Fintype.card V)

noncomputable def Moran.neutralPsi {V : Type u_1} [Fintype V] (t : Config V) : ℝ

Equations

• Moran.neutralPsi t = ↑(Moran.mutants t) / ↑(Fintype.card V)

theorem Moran.moranPsi_all {V : Type u_1} [Fintype V] [Nonempty V] {r : ℝ} (hr : 0 < r) (hr1 : r ≠ 1) : (moranPsi r fun (x : V) => true) = 1

theorem Moran.moranPsi_none {V : Type u_1} [Fintype V] {r : ℝ} : (moranPsi r fun (x : V) => false) = 0

theorem Moran.moranPsi_invariant {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (hreg : ∀ (i : V), G.degree i = d) {r : ℝ} (hr : 0 < r) (s : Config V) : (moranKernel G r hr).apply (moranPsi r) s = moranPsi r s

theorem Moran.neutralPsi_all {V : Type u_1} [Fintype V] [Nonempty V] : (neutralPsi fun (x : V) => true) = 1

theorem Moran.neutralPsi_none {V : Type u_1} [Fintype V] : (neutralPsi fun (x : V) => false) = 0

theorem Moran.neutralPsi_invariant {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (hreg : ∀ (i : V), G.degree i = d) (s : Config V) : (moranKernel G 1 ⋯).apply neutralPsi s = neutralPsi s

theorem Moran.isothermal {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (d : ℕ) (hreg : ∀ (i : V), G.degree i = d) {r : ℝ} (hr : 0 < r) (hr1 : r ≠ 1) (s : Config V) : fixation (moranKernel G r hr) s = (1 - (1 / r) ^ mutants s) / (1 - (1 / r) ^ Fintype.card V)

Isothermal theorem ("if" direction). On a connected regular graph, the fixation probability from k mutants is Moran's formula (1 - r^{-k}) / (1 - r^{-n}).

theorem Moran.isothermal_neutral {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (d : ℕ) (hreg : ∀ (i : V), G.degree i = d) (s : Config V) : fixation (moranKernel G 1 ⋯) s = ↑(mutants s) / ↑(Fintype.card V)

Neutral case. On a connected regular graph with r = 1, the fixation probability is the initial fraction of mutants.

theorem Moran.moran_formula {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] {r : ℝ} (hr : 0 < r) (hr1 : r ≠ 1) (s : Config V) : fixation (moranKernel ⊤ r hr) s = (1 - (1 / r) ^ mutants s) / (1 - (1 / r) ^ Fintype.card V)

Moran's formula (1958). On the complete graph, the fixation probability from k mutants is (1 - r^{-k}) / (1 - r^{-n}).