Skip to content

Runge–Kutta methods

StructureExplicit Runge–Kutta method#✓fully proved

An explicit Runge–Kutta method with \(s\) stages consists of a real \(s \times s\) Butcher tableau \(a = (a_{ij})\) that is strictly lower triangular, meaning \(a_{ij} = 0\) whenever \(i \le j\), and real weights \(b_1, \dots, b_s\).

structure ExplicitRK (s : ℕ) where
  /-- The Butcher tableau, strictly lower triangular. -/
  a : Fin s → Fin s → ℝ
  /-- The weights. -/
  b : Fin s → ℝ
  /-- Strict lower-triangularity: `a i j = 0` for `i ≤ j`. -/
  lower : ∀ i j : Fin s, i ≤ j → a i j = 0
Used by 22
Used byNodes of a Runge–Kutta method · Euler tableau · The Euler tableau satisfies the order-one condition · The Euler tableau gives the explicit Euler step · Heun's tableau · Heun's tableau satisfies the order-two conditions · Midpoint tableau · The midpoint tableau satisfies the order-two conditions · Order-four conditions · Order-one condition for Runge–Kutta methods · Order-three conditions for Runge–Kutta methods · Order-two conditions for Runge–Kutta methods · One Runge–Kutta step · Consistency of explicit Runge–Kutta methods · The classical RK4 tableau · The classical RK4 tableau satisfies all eight order-four conditions · Stability function of the classical RK4 method · Runge–Kutta stages · The defining equation of the stages · Stages computed row by row · Partial stage rows agree with the stages · Runge–Kutta stages tend to the vector field as the step shrinks

DefinitionNodes of a Runge–Kutta method#✓fully proved

For an explicit Runge–Kutta method with \(s\) stages and Butcher tableau \(a\), the node of stage \(i\) is the row sum \(c_i = \sum_j a_{ij}\), taken over all \(s\) stages \(j\).

def ExplicitRK.c {s : ℕ} (rk : ExplicitRK s) (i : Fin s) : ℝ := ∑ j, rk.a i j
Uses 1 · Used by 11
Statement usesExplicit Runge–Kutta method
Used byThe Euler tableau gives the explicit Euler step · Heun's tableau satisfies the order-two conditions · The midpoint tableau satisfies the order-two conditions · Order-four conditions · Order-three conditions for Runge–Kutta methods · Order-two conditions for Runge–Kutta methods · The classical RK4 tableau satisfies all eight order-four conditions · The defining equation of the stages · Stages computed row by row · Partial stage rows agree with the stages · Runge–Kutta stages tend to the vector field as the step shrinks

DefinitionStages computed row by row#✓fully proved

Let \(E\) be a real normed space, fix an explicit Runge–Kutta method with \(s\) stages, strictly lower-triangular tableau \(a\) and nodes \(c_i = \sum_j a_{ij}\), a vector field \(f\) assigning a vector \(f(t', x) \in E\) to each time \(t' \in \mathbb{R}\) and state \(x \in E\), a time \(t\), a state \(y \in E\) and a step \(h \in \mathbb{R}\). The rows \(K^{(n)} \in E^s\), indexed by \(0 \le i < s\), are defined by recursion on \(n\): \(K^{(0)} = 0\), and \(K^{(n+1)}_i\) equals \(f\bigl(t + c_i h,\ y + h \sum_{j < n} a_{ij} K^{(n)}_j\bigr)\) when \(i = n\) and equals \(K^{(n)}_i\) when \(i \ne n\). Only the entries of \(K^{(n)}\) with index less than \(n\) are filled in; the others are \(0\).

def stageRow : ℕ → Fin s → E
  | 0 => fun _ => 0
  | n + 1 => fun i =>
      if i.val = n then
        f (t + rk.c i * h)
          (y + h • ∑ j : Fin s, if j.val < n then rk.a i j • stageRow n j else 0)
      else stageRow n i
Uses 2 · Used by 4
Statement usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method
Used byThe Euler tableau gives the explicit Euler step · Runge–Kutta stages · The defining equation of the stages · Partial stage rows agree with the stages

DefinitionRunge–Kutta stages#✓fully proved

Let \(E\) be a real normed space, fix an explicit Runge–Kutta method with \(s\) stages, strictly lower-triangular tableau \(a\) and nodes \(c_i = \sum_j a_{ij}\), a vector field \(f\) assigning a vector \(f(t', x) \in E\) to each time \(t' \in \mathbb{R}\) and state \(x \in E\), a time \(t\), a state \(y \in E\) and a step \(h \in \mathbb{R}\). Let the rows \(K^{(n)} \in E^s\), indexed by \(0 \le i < s\), be defined by \(K^{(0)} = 0\), and \(K^{(n+1)}_i\) equal to \(f\bigl(t + c_i h,\ y + h \sum_{j < n} a_{ij} K^{(n)}_j\bigr)\) when \(i = n\) and to \(K^{(n)}_i\) when \(i \ne n\). For \(0 \le i < s\), the \(i\)-th stage \(k_i \in E\) is the entry at index \(i\) of the row \(K^{(i+1)}\).

def stage (i : Fin s) : E := stageRow rk f t y h (i.val + 1) i
Uses 2 · Used by 7
Statement usesExplicit Runge–Kutta method · Stages computed row by row
Used byThe Euler tableau gives the explicit Euler step · One Runge–Kutta step · Consistency of explicit Runge–Kutta methods · Stability function of the classical RK4 method · The defining equation of the stages · Partial stage rows agree with the stages · Runge–Kutta stages tend to the vector field as the step shrinks

TheoremPartial stage rows agree with the stages#✓fully proved

Let \(E\) be a real normed vector space and \(f(t, y)\) a vector field \(\mathbb{R} \times E \to E\), and fix an explicit Runge–Kutta method, a time \(t\), a state \(y \in E\) and a step size \(h \in \mathbb{R}\). Index the stages from \(0\). For every natural number \(m\) and every stage index \(i < m\), the \(i\)-th entry of the \(m\)-th partial row for \(f\), \(t\), \(y\) and \(h\) (the row-by-row construction that fills in the stages with index less than \(m\) and sets the rest to \(0\)) equals the \(i\)-th stage \(k_i\).

theorem stageRow_eq_of_lt : ∀ (m : ℕ) (i : Fin s), i.val < m →
    stageRow rk f t y h m i = stage rk f t y h i
Uses 4 · Used by 1
Statement usesExplicit Runge–Kutta method · Runge–Kutta stages · Stages computed row by row
Proof usesNodes of a Runge–Kutta method
Used byThe defining equation of the stages

TheoremThe defining equation of the stages#✓fully proved

Let \(E\) be a real normed vector space and \(f(t, y)\) a vector field \(\mathbb{R} \times E \to E\). For an explicit Runge–Kutta method with tableau \(a\) and nodes \(c_i = \sum_j a_{ij}\), a time \(t\), a state \(y \in E\) and a step size \(h\), the stages \(k_i\) satisfy \(k_i = f\bigl(t + c_i h, \; y + h \sum_{j < i} a_{ij} k_j\bigr)\) for every stage index \(i\).

theorem stage_eq (i : Fin s) :
    stage rk f t y h i =
      f (t + rk.c i * h)
        (y + h • ∑ j : Fin s, if j < i then rk.a i j • stage rk f t y h j else 0)
Uses 5 · Used by 2
Statement usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Runge–Kutta stages
Proof usesStages computed row by row · Partial stage rows agree with the stages
Used byStability function of the classical RK4 method · Runge–Kutta stages tend to the vector field as the step shrinks

DefinitionOne Runge–Kutta step#✓fully proved

Let \(E\) be a real normed vector space and \(f(t, y)\) a vector field \(\mathbb{R} \times E \to E\). For an explicit Runge–Kutta method with weights \(b\), a time \(t\), a state \(y \in E\) and a step size \(h \in \mathbb{R}\), one step of the method is \(y + h \sum_i b_i k_i\), where \(k_i\) is the \(i\)-th stage of the method for \(f\), \(t\), \(y\) and \(h\), and the sum runs over the stages.

def rkStep : E := y + h • ∑ i, rk.b i • stage rk f t y h i
Uses 2 · Used by 3
Statement usesExplicit Runge–Kutta method · Runge–Kutta stages
Used byThe Euler tableau gives the explicit Euler step · Consistency of explicit Runge–Kutta methods · Stability function of the classical RK4 method
23 fully proved

Order conditions

DefinitionOrder-one condition for Runge–Kutta methods#✓fully proved

An explicit Runge–Kutta method with weights \(b_i\) satisfies the order-one condition when \(\sum_i b_i = 1\), the sum running over all of its stages \(i\).

def OrderOne : Prop := ∑ i, rk.b i = 1
Uses 1 · Used by 6
Statement usesExplicit Runge–Kutta method
Used byThe Euler tableau satisfies the order-one condition · Heun's tableau satisfies the order-two conditions · The midpoint tableau satisfies the order-two conditions · Order-two conditions for Runge–Kutta methods · Consistency of explicit Runge–Kutta methods · The classical RK4 tableau satisfies all eight order-four conditions

DefinitionOrder-two conditions for Runge–Kutta methods#✓fully proved

An explicit Runge–Kutta method with tableau \(a\), weights \(b\) and nodes \(c_i = \sum_j a_{ij}\) satisfies the order-two conditions when it satisfies the order-one condition \(\sum_i b_i = 1\) and moreover \(\sum_i b_i c_i = \frac{1}{2}\), all sums running over the stages.

def OrderTwo : Prop := OrderOne rk ∧ ∑ i, rk.b i * rk.c i = 1 / 2
Uses 3 · Used by 4
Statement usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Order-one condition for Runge–Kutta methods
Used byHeun's tableau satisfies the order-two conditions · The midpoint tableau satisfies the order-two conditions · Order-three conditions for Runge–Kutta methods · The classical RK4 tableau satisfies all eight order-four conditions

DefinitionOrder-three conditions for Runge–Kutta methods#✓fully proved

An explicit Runge–Kutta method with tableau \(a\), weights \(b\) and nodes \(c_i = \sum_j a_{ij}\) satisfies the order-three conditions when it satisfies the order-two conditions \(\sum_i b_i = 1\) and \(\sum_i b_i c_i = \frac{1}{2}\), and moreover \(\sum_i b_i c_i^2 = \frac{1}{3}\) and \(\sum_{i, j} b_i a_{ij} c_j = \frac{1}{6}\), all sums running over the stages.

def OrderThree : Prop :=
  OrderTwo rk ∧ ∑ i, rk.b i * rk.c i ^ 2 = 1 / 3 ∧
    ∑ i, ∑ j, rk.b i * rk.a i j * rk.c j = 1 / 6
Uses 3 · Used by 2
Statement usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Order-two conditions for Runge–Kutta methods
Used byOrder-four conditions · The classical RK4 tableau satisfies all eight order-four conditions

DefinitionOrder-four conditions#✓fully proved

An explicit Runge–Kutta method with Butcher tableau \(a\), weights \(b\) and nodes \(c\) satisfies the order-four conditions when it satisfies the order-three conditions, namely \(\sum_i b_i = 1\), \(\sum_i b_i c_i = 1/2\), \(\sum_i b_i c_i^2 = 1/3\) and \(\sum_{i,j} b_i a_{ij} c_j = 1/6\), together with \(\sum_i b_i c_i^3 = 1/4\), \(\sum_{i,j} b_i c_i a_{ij} c_j = 1/8\), \(\sum_{i,j} b_i a_{ij} c_j^2 = 1/12\) and \(\sum_{i,j,k} b_i a_{ij} a_{jk} c_k = 1/24\). These are the eight Butcher conditions.

def OrderFour : Prop :=
  OrderThree rk ∧ ∑ i, rk.b i * rk.c i ^ 3 = 1 / 4 ∧
    ∑ i, ∑ j, rk.b i * rk.c i * rk.a i j * rk.c j = 1 / 8 ∧
    ∑ i, ∑ j, rk.b i * rk.a i j * rk.c j ^ 2 = 1 / 12 ∧
    ∑ i, ∑ j, ∑ k, rk.b i * rk.a i j * rk.a j k * rk.c k = 1 / 24
Uses 3 · Used by 1
Statement usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Order-three conditions for Runge–Kutta methods
Used byThe classical RK4 tableau satisfies all eight order-four conditions

Classical tableaux

DefinitionEuler tableau#✓fully proved

The explicit Runge–Kutta method with one stage, Butcher tableau \(a = (0)\) and weight \(b_1 = 1\).

def eulerRK : ExplicitRK 1 where
  a := !![0]
  b := ![1]
  lower := by
    intro i j _
    (fin_cases i; fin_cases j; rfl)
Uses 1 · Used by 2
Statement usesExplicit Runge–Kutta method
Used byThe Euler tableau satisfies the order-one condition · The Euler tableau gives the explicit Euler step

DefinitionMidpoint tableau#✓fully proved

The explicit Runge–Kutta method with two stages, Butcher tableau entries \(a_{21} = 1/2\) and \(a_{11} = a_{12} = a_{22} = 0\), and weights \(b_1 = 0\), \(b_2 = 1\).

noncomputable def midpointRK : ExplicitRK 2 where
  a := !![0, 0; 1 / 2, 0]
  b := ![0, 1]
  lower := by
    intro i j hij
    fin_cases i <;> fin_cases j <;> simp_all
Uses 1 · Used by 1
Statement usesExplicit Runge–Kutta method
Used byThe midpoint tableau satisfies the order-two conditions

DefinitionHeun's tableau#✓fully proved

The explicit Runge–Kutta method with two stages, Butcher tableau entries \(a_{21} = 1\) and \(a_{11} = a_{12} = a_{22} = 0\), and weights \(b_1 = b_2 = 1/2\).

noncomputable def heunRK : ExplicitRK 2 where
  a := !![0, 0; 1, 0]
  b := ![1 / 2, 1 / 2]
  lower := by
    intro i j hij
    fin_cases i <;> fin_cases j <;> simp_all
Uses 1 · Used by 1
Statement usesExplicit Runge–Kutta method
Used byHeun's tableau satisfies the order-two conditions

DefinitionThe classical RK4 tableau#✓fully proved

The classical fourth-order Runge–Kutta method is the explicit four-stage Runge–Kutta method whose tableau, with stages indexed \(1, \dots, 4\), has \(a_{21} = \frac{1}{2}\), \(a_{32} = \frac{1}{2}\), \(a_{43} = 1\) and all other \(a_{ij} = 0\), and whose weights are \(b = (\frac{1}{6}, \frac{1}{3}, \frac{1}{3}, \frac{1}{6})\).

noncomputable def rk4 : ExplicitRK 4 where
  a := !![0, 0, 0, 0; 1 / 2, 0, 0, 0; 0, 1 / 2, 0, 0; 0, 0, 1, 0]
  b := ![1 / 6, 1 / 3, 1 / 3, 1 / 6]
  lower := by
    intro i j hij
    fin_cases i <;> fin_cases j <;> simp_all
Uses 1 · Used by 2
Statement usesExplicit Runge–Kutta method
Used byThe classical RK4 tableau satisfies all eight order-four conditions · Stability function of the classical RK4 method

TheoremThe Euler tableau satisfies the order-one condition#✓fully proved

The weights of the Euler tableau sum to \(1\).

theorem eulerRK_orderOne : OrderOne eulerRK
Uses 3
Statement usesOrder-one condition for Runge–Kutta methods · Euler tableau
Proof usesExplicit Runge–Kutta method

TheoremThe midpoint tableau satisfies the order-two conditions#✓fully proved

For the midpoint tableau, with weights \(b_i\) and nodes \(c_i\), we have \(\sum_i b_i = 1\) and \(\sum_i b_i c_i = 1/2\).

theorem midpointRK_orderTwo : OrderTwo midpointRK
Uses 5
Statement usesOrder-two conditions for Runge–Kutta methods · Midpoint tableau
Proof usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Order-one condition for Runge–Kutta methods

TheoremHeun's tableau satisfies the order-two conditions#✓fully proved

For Heun's tableau, with weights \(b_i\) and nodes \(c_i\), we have \(\sum_i b_i = 1\) and \(\sum_i b_i c_i = 1/2\).

theorem heunRK_orderTwo : OrderTwo heunRK
Uses 5
Statement usesOrder-two conditions for Runge–Kutta methods · Heun's tableau
Proof usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Order-one condition for Runge–Kutta methods

TheoremThe classical RK4 tableau satisfies all eight order-four conditions#✓fully proved

The classical RK4 tableau satisfies all eight order-four conditions.

theorem rk4_orderFour : OrderFour rk4
Uses 7
Statement usesOrder-four conditions · The classical RK4 tableau
Proof usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Order-one condition for Runge–Kutta methods · Order-three conditions for Runge–Kutta methods · Order-two conditions for Runge–Kutta methods

Euler as a Runge–Kutta method

TheoremThe Euler tableau gives the explicit Euler step#✓fully proved

Let \(E\) be a real normed space and let \(f\) assign to each time \(t \in \mathbb{R}\) and state \(y \in E\) a vector \(f(t, y) \in E\). For all \(t, h \in \mathbb{R}\) and \(y \in E\), one Runge–Kutta step of size \(h\) from the state \(y\) at time \(t\) with the Euler tableau equals \(y + h f(t, y)\).

theorem euler_step : rkStep eulerRK f t y h = y + h • f t y
Uses 6
Statement usesEuler tableau · One Runge–Kutta step
Proof usesExplicit Runge–Kutta method · Nodes of a Runge–Kutta method · Runge–Kutta stages · Stages computed row by row

Consistency

TheoremRunge–Kutta stages tend to the vector field as the step shrinks#✓fully proved

Let \(E\) be a real normed space, fix an explicit Runge–Kutta method with \(s\) stages, a vector field \(f\) assigning a vector \(f(t', x) \in E\) to each time \(t' \in \mathbb{R}\) and state \(x \in E\), a time \(t\) and a state \(y \in E\), and suppose that \((t', x) \mapsto f(t', x)\) is continuous at \((t, y)\). For a step \(h \in \mathbb{R}\), let \(k_i(h)\) be the \(i\)-th stage of the method with step \(h\). Then for every natural number \(n\) and every stage index \(i < n\), \(k_i(h) \to f(t, y)\) as \(h \to 0\) with \(h \ne 0\).

The proof is by strong induction on the stage index, since earlier stages appear in later ones.

theorem stage_tendsto (hf : ContinuousAt (Function.uncurry f) (t, y)) :
    ∀ (n : ℕ) (i : Fin s), i.val < n →
      Tendsto (fun h => stage rk f t y h i) (𝓝[≠] 0) (𝓝 (f t y))
Uses 4 · Used by 1
Statement usesExplicit Runge–Kutta method · Runge–Kutta stages
Proof usesNodes of a Runge–Kutta method · The defining equation of the stages
Used byConsistency of explicit Runge–Kutta methods

TheoremConsistency of explicit Runge–Kutta methods#✓fully proved

Let \(E\) be a real normed vector space, let \(f(t, y)\) be a vector field \(\mathbb{R} \times E \to E\), let \(t \in \mathbb{R}\) and \(y \in E\), and for an explicit Runge–Kutta method with weights \(b\) let \(y_1(h)\) be the result of one step of size \(h\) from the state \(y\) at time \(t\). If \(\sum_i b_i = 1\) and \(f\) is continuous at \((t, y)\) as a function of both variables, then \(h^{-1} (y_1(h) - y) \to f(t, y)\) as \(h \to 0\) with \(h \neq 0\).

theorem rkStep_sub_inv_smul_tendsto (hOrder : OrderOne rk)
    (hf : ContinuousAt (Function.uncurry f) (t, y)) :
    Tendsto (fun h => h⁻¹ • (rkStep rk f t y h - y)) (𝓝[≠] 0) (𝓝 (f t y))
Uses 5
Statement usesExplicit Runge–Kutta method · Order-one condition for Runge–Kutta methods · One Runge–Kutta step
Proof usesRunge–Kutta stages · Runge–Kutta stages tend to the vector field as the step shrinks

Linear stability of RK4

TheoremStability function of the classical RK4 method#✓fully proved

For all real numbers \(\lambda\), \(y\) and \(h\), one step of size \(h\) of the classical fourth-order Runge–Kutta method applied to the scalar linear test equation \(u' = \lambda u\) on \(\mathbb{R}\), starting from the state \(y\) at time \(0\), gives \(y \, R(\lambda h)\), where \(R(z) = 1 + z + \frac{z^2}{2} + \frac{z^3}{6} + \frac{z^4}{24}\).

theorem rk4_stability (lam y h : ℝ) :
    rkStep rk4 (fun _ y => lam * y) 0 y h =
      y * (1 + lam * h + (lam * h) ^ 2 / 2 + (lam * h) ^ 3 / 6 + (lam * h) ^ 4 / 24)
Uses 5
Statement usesThe classical RK4 tableau · One Runge–Kutta step
Proof usesExplicit Runge–Kutta method · Runge–Kutta stages · The defining equation of the stages

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.