Differential identities for the inverse flow of a construction stream.
theorem
AVenhance.constructionFlowInv_hasDerivAt
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
(m : ℕ)
(t s : ℝ)
(x : Homogenization.Vec 2)
:
HasDerivAt (fun (r : ℝ) => constructionFlowInv hseq m r x s)
(-(constructionFlowInvJacobian hseq m (t - s) s x) (streamVel (Φ m) t x)) t
The inverse flow satisfies the backwards transport equation. This is the
source identity e.PDE.backwards, derived from the initial-time derivative of
the forward flow.