@[reducible, inline]

abbrev MultiIndex' (n : ℕ) : Type

A multi-index in $n$ variables is a function $\alpha : \{1, \ldots, n\} \to \mathbb{N}$ recording the order of differentiation in each coordinate.

def multiIndexOrder {n : ℕ} (α : MultiIndex' n) : ℕ

The order of a multi-index $\alpha = (\alpha_1, \ldots, \alpha_n)$ is $|\alpha| = \sum_i \alpha_i$, i.e. the total number of derivatives it represents.

noncomputable def partialDerivFin {n : ℕ} (i : Fin n) (f : (Fin n → ℝ) → ℝ) : (Fin n → ℝ) → ℝ

The $i$-th partial derivative $\partial_{x^i} f$ of $f : \mathbb{R}^n \to \mathbb{R}$, defined via the Fréchet derivative applied to the $i$-th standard basis vector.

noncomputable def iteratedPartialDeriv {n : ℕ} : List (Fin n) → ((Fin n → ℝ) → ℝ) → (Fin n → ℝ) → ℝ

Iterated partial derivative along a list of coordinate indices: applies the partial derivatives $\partial_{x^{i_1}} \partial_{x^{i_2}} \cdots$ from outermost to innermost.

noncomputable def multiIndexToList {n : ℕ} (α : Fin n → ℕ) : List (Fin n)

Convert a multi-index $\alpha$ to a list of coordinate indices in which each $i$ is repeated $\alpha_i$ times — the sequence of partial derivatives encoded by $\alpha$.

noncomputable def multiIndexDeriv {n : ℕ} (α : Fin n → ℕ) (f : (Fin n → ℝ) → ℝ) : (Fin n → ℝ) → ℝ

The multi-index derivative $\partial^{\alpha} f = \partial_{x^1}^{\alpha_1} \cdots \partial_{x^n}^{\alpha_n} f$, obtained by iterating partial derivatives according to the list encoding of the multi-index $\alpha$.

@[implicit_reducible]

noncomputable instance multiIndexFintype (n N : ℕ) : Fintype { α : MultiIndex' n // multiIndexOrder α ≤ N }

The set of multi-indices of order at most $N$ in $n$ variables is finite.

structure PDEJet (n N : ℕ) : Type

The $N$-jet of a function at a point: stores the base point $x \in \mathbb{R}^n$ and the values of all partial derivatives $\partial^{\alpha} u(x)$ with $|\alpha| \le N$. This is the data on which a PDE of order $N$ acts (Definition 1.0.1).

• point : Fin n → ℝ
• derivatives : { α : MultiIndex' n // multiIndexOrder α ≤ N } → ℝ

noncomputable def jetOf {n : ℕ} (N : ℕ) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : PDEJet n N

The $N$-jet of the function $u$ at the point $x$: bundles $x$ together with $\{\partial^{\alpha} u(x)\}_{|\alpha| \le N}$.

structure PDE (n N : ℕ) : Type

A PDE of order $N$ in $n$ variables (Definition 1.0.1): an equation $F(\text{jet}) = 0$ where $F$ is a real-valued function of the $N$-jet $(u, \partial^{\alpha} u, x)$.

• F : PDEJet n N → ℝ

structure LinearDifferentialOperator (n N : ℕ) : Type

A linear differential operator of order at most $N$ on $\mathbb{R}^n$ (Definition 4.0.2): specified by coefficient functions $a_{\alpha}(x)$ for each multi-index $\alpha$ with $|\alpha| \le N$, acting on a function $u$ as $\mathcal{L} u = \sum_{|\alpha| \le N} a_{\alpha}(x) \partial^{\alpha} u$.

• coeff : { α : MultiIndex' n // multiIndexOrder α ≤ N } → (Fin n → ℝ) → ℝ

noncomputable def LinearDifferentialOperator.apply {n N : ℕ} (L : LinearDifferentialOperator n N) (u : (Fin n → ℝ) → ℝ) : (Fin n → ℝ) → ℝ

Action of a linear differential operator on a function: $(\mathcal{L} u)(x) = \sum_{|\alpha| \le N} a_{\alpha}(x) \, \partial^{\alpha} u(x)$.

noncomputable def LinearDifferentialOperator.toLinearMap {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) : ((Fin n → ℝ) → ℝ) →ₗ[ℝ] (Fin n → ℝ) → ℝ

Repackage a linear differential operator as a genuine $\mathbb{R}$-linear map $\mathcal{L} : C^{\infty}(\mathbb{R}^n) \to C^{\infty}(\mathbb{R}^n)$, given the linearity of each multi-index derivative supplied via hlin.

@[simp]

theorem LinearDifferentialOperator.toLinearMap_apply {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) (f : (Fin n → ℝ) → ℝ) : (L.toLinearMap hlin) f = L.apply f

The underlying function of L.toLinearMap agrees with L.apply.

theorem LinearDifferentialOperator.apply_add {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) (u v : (Fin n → ℝ) → ℝ) : L.apply (u + v) = L.apply u + L.apply v

Additivity: $\mathcal{L}(u + v) = \mathcal{L} u + \mathcal{L} v$.

theorem LinearDifferentialOperator.apply_smul {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) (c : ℝ) (u : (Fin n → ℝ) → ℝ) : L.apply (c • u) = c • L.apply u

Homogeneity: $\mathcal{L}(c u) = c \mathcal{L} u$ for any scalar $c \in \mathbb{R}$.

theorem LinearDifferentialOperator.apply_sum {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) {ι : Type u_1} (s : Finset ι) (f : ι → (Fin n → ℝ) → ℝ) : L.apply (∑ i ∈ s, f i) = ∑ i ∈ s, L.apply (f i)

A linear operator commutes with finite sums: $\mathcal{L}\left(\sum_{i \in s} f_i\right) = \sum_{i \in s} \mathcal{L} f_i$.

theorem LinearDifferentialOperator.apply_sub {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) (u v : (Fin n → ℝ) → ℝ) : L.apply (u - v) = L.apply u - L.apply v

Subtractivity: $\mathcal{L}(u - v) = \mathcal{L} u - \mathcal{L} v$.

theorem LinearDifferentialOperator.linearity {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : L.apply (a • u + b • v) x = a * L.apply u x + b * L.apply v x

Defining linearity of a linear differential operator (Definition 4.0.2, pointwise form): $\mathcal{L}(a u + b v)(x) = a \, \mathcal{L} u(x) + b \, \mathcal{L} v(x)$ for all constants $a, b \in \mathbb{R}$, all functions $u, v$, and all $x$.

structure LinearPDE (n N : ℕ) : Type

A linear PDE of order $N$ on $\mathbb{R}^n$ (Definition 4.0.3): an equation $\mathcal{L} u = f(x)$ specified by a linear differential operator $\mathcal{L}$ and a source function $f$.

• L : LinearDifferentialOperator n N
• f : (Fin n → ℝ) → ℝ

def LinearPDE.IsHomogeneous {n N : ℕ} (P : LinearPDE n N) : Prop

A linear PDE is homogeneous (Definition 4.0.4) iff its source term $f$ is identically zero; otherwise it is called inhomogeneous.

theorem superposition_principle {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) {M : ℕ} (u : Fin M → (Fin n → ℝ) → ℝ) (c : Fin M → ℝ) (hsol : ∀ (i : Fin M), L.apply (u i) = 0) : L.apply (∑ i : Fin M, c i • u i) = 0

Superposition principle (Proposition 4.0.1): if $u_1, \ldots, u_M$ are solutions to the homogeneous linear PDE $\mathcal{L} u = 0$ and $c_1, \ldots, c_M \in \mathbb{R}$ are any scalars, then $\sum_{i=1}^{M} c_i u_i$ is also a solution.

theorem inhomogeneous_solution_set {n N : ℕ} (L : LinearDifferentialOperator n N) (hlin : ∀ (α : { α : MultiIndex' n // multiIndexOrder α ≤ N }) (a b : ℝ) (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ), multiIndexDeriv (↑α) (a • u + b • v) x = a * multiIndexDeriv (↑α) u x + b * multiIndexDeriv (↑α) v x) (f u_I : (Fin n → ℝ) → ℝ) (hI : L.apply u_I = f) : {w : (Fin n → ℝ) → ℝ | L.apply w = f} = {w : (Fin n → ℝ) → ℝ | ∃ (u_H : (Fin n → ℝ) → ℝ), L.apply u_H = 0 ∧ w = u_I + u_H}

Relationship between inhomogeneous and homogeneous solutions (Proposition 4.0.2): given a fixed inhomogeneous solution $u_I$ with $\mathcal{L} u_I = f$, the set $S_I$ of all solutions to $\mathcal{L} u = f$ equals the translate of the homogeneous solution set $S_H = \{u_H \mid \mathcal{L} u_H = 0\}$ by $u_I$, i.e. $S_I = \{u_I + u_H \mid u_H \in S_H\}$.