Fisher–KPP travelling waves

DefinitionTraveling-wave profile of the Fisher–KPP equation#✓fully proved

U is a traveling-wave profile of speed c for ∂u/∂t = D ∂²u/∂x² + r u (1 - u): it is twice differentiable with first derivative U' and U'' = -(c U' + r U (1 - U)) / D, which for D ≠ 0 is the profile equation D U'' + c U' + r U (1 - U) = 0.

def IsWaveProfile (D r c : ℝ) (U U' : ℝ → ℝ) : Prop :=
  ∀ z, HasDerivAt U (U' z) z ∧
    HasDerivAt U' ((-(c * U' z) - r * U z * (1 - U z)) / D) z

Used by 7

Used byTime derivative of a traveling wave · Space derivative of a traveling wave · Traveling wave solves the Fisher–KPP equation · Traveling front of the Fisher–KPP equation · The Ablowitz–Zeppetella front · No traveling wave with c² < 4 r D · Minimal speed of Fisher–KPP traveling fronts

DefinitionTraveling front of the Fisher–KPP equation#✓fully proved

A traveling front of speed c: a wave profile with 0 < U < 1, U → 1 at -∞ and U → 0 at +∞.

def IsFront (D r c : ℝ) (U U' : ℝ → ℝ) : Prop :=
  IsWaveProfile D r c U U' ∧ (∀ z, 0 < U z ∧ U z < 1) ∧ Tendsto U atBot (𝓝 1) ∧
    Tendsto U atTop (𝓝 0)

Uses 1 · Used by 3

Statement usesTraveling-wave profile of the Fisher–KPP equation

Used byKolmogorov–Petrovsky–Piskunov: fronts exist at every speed c ≥ 2 √(r D) · The Ablowitz–Zeppetella front · Minimal speed of Fisher–KPP traveling fronts

TheoremTime derivative of a traveling wave#✓fully proved

Time derivative of the wave u(x, t) = U(x - c t): ∂u/∂t = -c U'(x - c t).

theorem hasDerivAt_wave_t (h : IsWaveProfile D r c U U') (x t : ℝ) :
    HasDerivAt (fun s => U (x - c * s)) (-c * U' (x - c * t)) t

Uses 1

Statement usesTraveling-wave profile of the Fisher–KPP equation

TheoremSpace derivative of a traveling wave#✓fully proved

Space derivative of the wave: ∂u/∂x = U'(x - c t).

theorem hasDerivAt_wave_x (h : IsWaveProfile D r c U U') (x t : ℝ) :
    HasDerivAt (fun y => U (y - c * t)) (U' (x - c * t)) x

Uses 1

Statement usesTraveling-wave profile of the Fisher–KPP equation

TheoremTraveling wave solves the Fisher–KPP equation#✓fully proved

Second space derivative of the wave; with hD : D ≠ 0 it gives the PDE -c U' = D U'' + r U (1 - U), i.e. ∂u/∂t = D ∂²u/∂x² + r u (1 - u).

theorem hasDerivAt_wave_xx (h : IsWaveProfile D r c U U') (hD : D ≠ 0) (x t : ℝ) :
    ∃ U'' : ℝ, HasDerivAt (fun y => U' (y - c * t)) U'' x ∧
      -c * U' (x - c * t) = D * U'' + r * U (x - c * t) * (1 - U (x - c * t))

Uses 1

Statement usesTraveling-wave profile of the Fisher–KPP equation

TheoremNo traveling wave with c² < 4 r D#✓fully proved

If D, r > 0 and c² < 4 r D, a wave profile tending to 0 at +∞ is not eventually positive. (This excludes |c| < 2 √(r D), not c < 2 √(r D) for negative c.)

theorem not_eventually_pos_of_sq_lt {D r c : ℝ} {U U' : ℝ → ℝ} (hD : 0 < D) (hr : 0 < r)
    (hc : c ^ 2 < 4 * r * D) (hU : IsWaveProfile D r c U U') (hlim : Tendsto U atTop (𝓝 0)) :
    ¬ ∀ᶠ z in atTop, 0 < U z

Uses 1 · Used by 1

Statement usesTraveling-wave profile of the Fisher–KPP equation

Used byMinimal speed of Fisher–KPP traveling fronts

TheoremMinimal speed of Fisher–KPP traveling fronts#✓fully proved

A front of speed c needs c² ≥ 4 r D; for c ≥ 0 this is c ≥ 2 √(r D).

theorem not_isFront_of_sq_lt {D r c : ℝ} {U U' : ℝ → ℝ} (hD : 0 < D) (hr : 0 < r)
    (hc : c ^ 2 < 4 * r * D) : ¬ IsFront D r c U U'

Uses 3

Statement usesTraveling front of the Fisher–KPP equation

Proof usesTraveling-wave profile of the Fisher–KPP equation · No traveling wave with c² < 4 r D

DefinitionRate of the Ablowitz–Zeppetella wave#✓fully proved

The rate κ = √(r / (6 D)) of the Ablowitz–Zeppetella wave.

noncomputable def azRate (D r : ℝ) : ℝ := √(r / (6 * D))

Used by 3

Used byAblowitz–Zeppetella wave profile · Derivative of the Ablowitz–Zeppetella profile · The Ablowitz–Zeppetella front

DefinitionSpeed of the Ablowitz–Zeppetella wave#✓fully proved

The Ablowitz–Zeppetella speed c = 5 √(r D / 6) (5 / √6 when D = r = 1).

noncomputable def azSpeed (D r : ℝ) : ℝ := 5 * √(r * D / 6)

Used by 2

Used byThe Ablowitz–Zeppetella front · Ablowitz–Zeppetella speed exceeds the minimal front speed

DefinitionAblowitz–Zeppetella wave profile#✓fully proved

The Ablowitz–Zeppetella profile U(z) = (1 + C exp (κ z))⁻².

noncomputable def azWave (D r C : ℝ) (z : ℝ) : ℝ := (1 + C * exp (azRate D r * z))⁻¹ ^ 2

Uses 1 · Used by 1

Statement usesRate of the Ablowitz–Zeppetella wave

Used byThe Ablowitz–Zeppetella front

DefinitionDerivative of the Ablowitz–Zeppetella profile#✓fully proved

The derivative of the Ablowitz–Zeppetella profile, -2 κ C e^{κ z} (1 + C e^{κ z})⁻³.

noncomputable def azWaveDeriv (D r C : ℝ) (z : ℝ) : ℝ :=
  -2 * azRate D r * C * exp (azRate D r * z) * (1 + C * exp (azRate D r * z))⁻¹ ^ 3

Uses 1 · Used by 1

Statement usesRate of the Ablowitz–Zeppetella wave

Used byThe Ablowitz–Zeppetella front

TheoremThe Ablowitz–Zeppetella front#✓fully proved

For D, r, C > 0, (1 + C exp (z √(r / (6 D))))⁻² is a front of speed 5 √(r D / 6).

theorem isFront_azWave {D r C : ℝ} (hD : 0 < D) (hr : 0 < r) (hC : 0 < C) :
    IsFront D r (azSpeed D r) (azWave D r C) (azWaveDeriv D r C)

Uses 6

Statement usesTraveling front of the Fisher–KPP equation · Speed of the Ablowitz–Zeppetella wave · Ablowitz–Zeppetella wave profile · Derivative of the Ablowitz–Zeppetella profile

Proof usesTraveling-wave profile of the Fisher–KPP equation · Rate of the Ablowitz–Zeppetella wave

TheoremAblowitz–Zeppetella speed exceeds the minimal front speed#✓fully proved

The Ablowitz–Zeppetella speed exceeds the minimal speed: 2 √(r D) < 5 √(r D / 6).

theorem two_mul_sqrt_lt_azSpeed {D r : ℝ} (hD : 0 < D) (hr : 0 < r) :
    2 * √(r * D) < azSpeed D r

Uses 1

Statement usesSpeed of the Ablowitz–Zeppetella wave

TheoremKolmogorov–Petrovsky–Piskunov: fronts exist at every speed c ≥ 2 √(r D)#●ready to prove

Kolmogorov–Petrovsky–Piskunov: fronts exist at every speed c ≥ 2 √(r D), and they are strictly decreasing.

theorem_wanted exists_isFront_of_le {D r c : ℝ} (hD : 0 < D) (hr : 0 < r)
    (hc : 2 * √(r * D) ≤ c) : ∃ U U' : ℝ → ℝ, IsFront D r c U U' ∧ StrictAnti U

Uses 1

Statement usesTraveling front of the Fisher–KPP equation

13 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.