Exponential autonomous functions

DefinitionComplete Bell polynomials#✓fully proved

For a sequence \(x = (x_0, x_1, x_2, \dots)\) of complex numbers, the complete Bell polynomials \(B_n(x)\) are defined by \(B_0(x) = 1\) and, for every \(m \ge 0\), \(B_{m+1}(x) = \sum_{i=0}^{m} \binom{m}{i} B_{m-i}(x) \, x_i\).

Writing \(x_i = y_{i+1}\), this is the usual recurrence for \(B_{m+1}(y_1, \dots, y_{m+1})\).

noncomputable def completeBellPolynomial (n : Nat) (x : Nat → Complex) : Complex :=
  Nat.strongRecOn (motive := fun _ => (Nat → Complex) → Complex) n
    (fun m ih x =>
      match m with
      | 0 => 1
      | m + 1 =>
        ∑ i ∈ Finset.range (m + 1),
          (m.choose i : Complex) * ih (m - i) (by omega) x * x i) x

Used by 1

Used byComplete exponential autonomous functions

DefinitionComplete exponential autonomous functions#✓fully proved

Let \(k \ge 1\), \(a \in \mathbb{C}\) and \(x_0, \dots, x_{k-1} \in \mathbb{C}\). The complete exponential autonomous function of order \(k\) with parameter \(a\) and variables \(x\) is the sequence \(f_0, f_1, f_2, \dots\) of complex numbers given by \(f_n = x_n\) for \(n < k\), \(f_k = a e^{x_0}\), and \(f_n = a e^{x_0} B_{n-k}(y)\) for \(n > k\), where \(B_{n-k}\) is the complete Bell polynomial and \(y\) is the sequence with \(y_i = f_{i+1}\) (so only \(f_1, \dots, f_{n-k}\) enter).

noncomputable def completeExponentialAutonomousFunction (k : Nat) (hk : 0 < k)
    (a : Complex) (x : Fin k → Complex) : Nat → Complex :=
  fun N =>
    Nat.strongRecOn (motive := fun _ => Complex) N (fun n ih =>
      if h : n < k then x ⟨n, h⟩
      else if _h2 : n = k then a * Complex.exp (x ⟨0, hk⟩)
      else
        a * Complex.exp (x ⟨0, hk⟩) *
          completeBellPolynomial (n - k) (fun i =>
            if h3 : i + 1 < n then ih (i + 1) h3 else 0))

Uses 1

Statement usesComplete Bell polynomials

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.