Logistic growth equation

DefinitionExplicit solution of the logistic equation#✓fully proved

Explicit solution of the logistic equation x' = r x (1 - x / K) with x 0 = x₀: K x₀ e^{r t} / (K + x₀ (e^{r t} - 1)).

noncomputable def logistic (r K x₀ t : ℝ) : ℝ :=
  K * x₀ * exp (r * t) / (K + x₀ * (exp (r * t) - 1))

Used by 9

Used byUniqueness of the logistic solution · The explicit solution solves the logistic equation · Exact deterministic transit time · Logistic transit time from \(1/(2N)\) to \(1 - 1/(2N)\) · Initial value of the logistic solution · Log-odds grow linearly · Logistic solution is strictly increasing · Convergence to the carrying capacity · Exponential limit

TheoremInitial value of the logistic solution#✓fully proved

The logistic solution starts at x₀ (for K ≠ 0).

theorem logistic_zero {r K : ℝ} (x₀ : ℝ) (hK : K ≠ 0) : logistic r K x₀ 0 = x₀

Uses 1 · Used by 1

Statement usesExplicit solution of the logistic equation

Used byUniqueness of the logistic solution

TheoremPositivity of the logistic solution's denominator#✓fully proved

In the biological domain (K > 0, x₀ > 0, r t ≥ 0, or x₀ ≤ K) the denominator of the logistic solution is positive.

theorem logistic_denom_pos {r K x₀ t : ℝ} (hK : 0 < K) (hx₀ : 0 < x₀)
    (h : 0 ≤ r * t ∨ x₀ ≤ K) : 0 < K + x₀ * (exp (r * t) - 1)

Used by 2

Used byUniqueness of the logistic solution · Logistic solution is strictly increasing

TheoremThe explicit solution solves the logistic equation#✓fully proved

Wherever the denominator K + x₀ (e^{r t} - 1) is nonzero, x' = r x (1 - x / K) (all real parameters, K ≠ 0).

theorem hasDerivAt_logistic {r K x₀ t : ℝ} (hK : K ≠ 0)
    (hden : K + x₀ * (exp (r * t) - 1) ≠ 0) :
    HasDerivAt (logistic r K x₀)
      (r * logistic r K x₀ t * (1 - logistic r K x₀ t / K)) t

Uses 1 · Used by 2

Statement usesExplicit solution of the logistic equation

Used byUniqueness of the logistic solution · Logistic solution is strictly increasing

TheoremUniqueness of the logistic solution#✓fully proved

Uniqueness of the logistic solution on [0, T]: in the biological domain (K > 0, x₀ > 0, r ≥ 0), any function continuous on [0, T], with right derivative r x (1 - x / K) on [0, T) and x 0 = x₀, equals the explicit solution on [0, T].

theorem eqOn_logistic_of_hasDerivWithinAt {r K x₀ T : ℝ} (hK : 0 < K) (hx₀ : 0 < x₀)
    (hr : 0 ≤ r) {x : ℝ → ℝ} (hc : ContinuousOn x (Icc 0 T))
    (hd : ∀ t ∈ Ico 0 T, HasDerivWithinAt x (r * x t * (1 - x t / K)) (Ici t) t)
    (h0 : x 0 = x₀) : EqOn x (logistic r K x₀) (Icc 0 T)

Uses 4

Statement usesExplicit solution of the logistic equation

Proof usesThe explicit solution solves the logistic equation · Positivity of the logistic solution's denominator · Initial value of the logistic solution

TheoremConvergence to the carrying capacity#✓fully proved

For r > 0 and x₀ > 0, x(t) → K as t → ∞ (the identity needs no sign condition on K; biologically K > 0).

theorem tendsto_logistic_atTop {r K x₀ : ℝ} (hr : 0 < r) (hx₀ : 0 < x₀) :
    Tendsto (logistic r K x₀) atTop (𝓝 K)

Uses 1

Statement usesExplicit solution of the logistic equation

TheoremExponential limit#✓fully proved

For fixed r, x₀, t, the logistic solution tends to the exponential-growth solution x₀ e^{r t} as the carrying capacity K → ∞.

theorem tendsto_logistic_carryingCapacity_atTop (r x₀ t : ℝ) :
    Tendsto (fun K => logistic r K x₀ t) atTop (𝓝 (x₀ * exp (r * t)))

Uses 1

Statement usesExplicit solution of the logistic equation

TheoremLog-odds grow linearly#✓fully proved

Log-odds grow linearly for a frequency (K = 1): for 0 < x₀ < 1 and all r, t, log (x(t) / (1 - x(t))) = log (x₀ / (1 - x₀)) + r t.

theorem logit_logistic {x₀ : ℝ} (hx₀ : 0 < x₀) (hx₁ : x₀ < 1) (r t : ℝ) :
    log (logistic r 1 x₀ t / (1 - logistic r 1 x₀ t)) = log (x₀ / (1 - x₀)) + r * t

Uses 1

Statement usesExplicit solution of the logistic equation

TheoremExact deterministic transit time#✓fully proved

Starting from frequency a ∈ (0, 1) with r ≠ 0, the logistic frequency reaches 1 - a at time (2 / r) log ((1 - a) / a).

theorem logistic_transitTime {a r : ℝ} (ha : 0 < a) (ha1 : a < 1) (hr : r ≠ 0) :
    logistic r 1 a (2 / r * log ((1 - a) / a)) = 1 - a

Uses 1 · Used by 1

Statement usesExplicit solution of the logistic equation

Used byLogistic transit time from \(1/(2N)\) to \(1 - 1/(2N)\)

TheoremLogistic transit time from \(1/(2N)\) to \(1 - 1/(2N)\)#✓fully proved

The transit time from 1 / (2N) to 1 - 1 / (2N) is (2 / r) log (2N - 1), for N ≥ 1 and r ≠ 0.

theorem logistic_transitTime_twoN {N : ℕ} (hN : 1 ≤ N) {r : ℝ} (hr : r ≠ 0) :
    logistic r 1 (1 / (2 * N)) (2 / r * log (2 * N - 1)) = 1 - 1 / (2 * N)

Uses 2

Statement usesExplicit solution of the logistic equation

Proof usesExact deterministic transit time

TheoremLogistic solution is strictly increasing#✓fully proved

For r > 0 and 0 < x₀ < K the logistic solution is strictly increasing, so the transit time of logistic_transitTime is the unique time at which 1 - a is reached.

theorem strictMono_logistic {r K x₀ : ℝ} (hr : 0 < r) (hK : 0 < K) (hx₀ : 0 < x₀)
    (hx₀K : x₀ < K) : StrictMono (logistic r K x₀)

Uses 3

Statement usesExplicit solution of the logistic equation

Proof usesThe explicit solution solves the logistic equation · Positivity of the logistic solution's denominator

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.