PublishedFlowInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional ODE input used by the transport step.

Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, AMS GSM 140 (2012), Theorem 2.10, equations (2.49)--(2.51), Lemma 2.7, and Lemma 3.11. We retain only dimension three, four spatial derivatives, and the closed time interval [0,1]. Uniform derivative bounds follow by applying Gronwall to the four variational equations.

def OAI.ContinuumCoulomb.flowJacobian line 19
def OAI.ContinuumCoulomb.fieldDivergence line 22
def OAI.ContinuumCoulomb.IsUnitTimeFlow line 25
structure OAI.ContinuumCoulomb.PublishedC4FlowInput line 31
Source documentation
Smooth dependence, Liouville's equation and a uniform finite-order variational estimate.
```
structure PublishedC4FlowInput : Prop where
…
```