Lotka–Volterra predator–prey model

DefinitionFirst integral of the Lotka–Volterra system#✓fully proved

The Lotka–Volterra first integral V(x, y) = δ x - γ log x + β y - α log y for the system x' = α x - β x y, y' = δ x y - γ y. It is meaningful on the open positive quadrant x, y > 0; elsewhere Real.log takes junk values (log 0 = 0, log (-x) = log x).

noncomputable def firstIntegral (α β γ δ x y : ℝ) : ℝ :=
  δ * x - γ * log x + β * y - α * log y

Used by 3

Used byPositive solutions lie on level curves · The coexistence equilibrium minimizes the first integral · Lotka–Volterra first integral

TheoremLotka–Volterra first integral#✓fully proved

If x' = α x - β x y and y' = δ x y - γ y at time t and x t, y t > 0, then t ↦ V(x t, y t) has derivative 0 at t.

theorem hasDerivAt_firstIntegral {α β γ δ : ℝ} {x y : ℝ → ℝ} {t : ℝ}
    (hx : HasDerivAt x (α * x t - β * x t * y t) t)
    (hy : HasDerivAt y (δ * x t * y t - γ * y t) t) (hx0 : 0 < x t) (hy0 : 0 < y t) :
    HasDerivAt (fun s => firstIntegral α β γ δ (x s) (y s)) 0 t

Uses 1 · Used by 1

Statement usesFirst integral of the Lotka–Volterra system

Used byPositive solutions lie on level curves

TheoremPositive solutions lie on level curves#✓fully proved

If (x, y) solves the Lotka–Volterra system on [0, ∞) and both populations stay positive there, then V(x t, y t) = V(x 0, y 0) for all t ≥ 0.

theorem firstIntegral_eq {α β γ δ : ℝ} {x y : ℝ → ℝ}
    (hx : ∀ t, 0 ≤ t → HasDerivAt x (α * x t - β * x t * y t) t)
    (hy : ∀ t, 0 ≤ t → HasDerivAt y (δ * x t * y t - γ * y t) t)
    (hx0 : ∀ t, 0 ≤ t → 0 < x t) (hy0 : ∀ t, 0 ≤ t → 0 < y t) {t : ℝ} (ht : 0 ≤ t) :
    firstIntegral α β γ δ (x t) (y t) = firstIntegral α β γ δ (x 0) (y 0)

Uses 2

Statement usesFirst integral of the Lotka–Volterra system

Proof usesLotka–Volterra first integral

TheoremThe coexistence equilibrium minimizes the first integral#✓fully proved

For positive parameters and x, y > 0, V(γ / δ, α / β) ≤ V(x, y).

theorem firstIntegral_equilibrium_le {α β γ δ x y : ℝ} (hα : 0 < α) (hβ : 0 < β) (hγ : 0 < γ)
    (hδ : 0 < δ) (hx : 0 < x) (hy : 0 < y) :
    firstIntegral α β γ δ (γ / δ) (α / β) ≤ firstIntegral α β γ δ x y

Uses 1

Statement usesFirst integral of the Lotka–Volterra system

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.