The genuine invertible Jacobian of the constructed nonlinear flow

Differentiating the path-space equation identifies its derivative with the actual homogeneous linear evolution. The already constructed inverse flow is therefore differentiable and smooth; its derivative is the actual inverse fundamental operator, without an independent inverse assumption.

noncomputable def EulerSmoothBanachFlow.jacobianEvolution {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) : EulerLinearDuhamel.Evolution T hT (A.derivative.superposition ((pathFamily T hT A) x))

Jacobian evolution, given by constructedEvolution T hT (A.derivative.superposition (pathFamily T hT A x)).

Equations

• EulerSmoothBanachFlow.jacobianEvolution T hT A x = EulerLinearDuhamel.constructedEvolution T hT (A.derivative.superposition ((EulerSmoothBanachFlow.pathFamily T hT A) x))

theorem EulerSmoothBanachFlow.pathFamily_fderiv {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) : fderiv ℝ (⇑(pathFamily T hT A)) x = (jacobianEvolution T hT A x).initialOperator

theorem EulerSmoothBanachFlow.jacobianEvolution_backward_initial {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) : (jacobianEvolution T hT A x).backward ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ E

theorem EulerSmoothBanachFlow.initialOperator_evaluation {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) (t : ↑(Set.Icc 0 T)) : ContinuousMap.evalCLM ℝ t ∘SL (jacobianEvolution T hT A x).initialOperator = (jacobianEvolution T hT A x).forward t

theorem EulerSmoothBanachFlow.forward_hasFDerivAt_label {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : HasFDerivAt (fun (y : E) => (flowData T hT A).forward (↑t) y) ((jacobianEvolution T hT A x).forward t) x

theorem EulerSmoothBanachFlow.forward_fderiv {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : fderiv ℝ (fun (y : E) => (flowData T hT A).forward (↑t) y) x = (jacobianEvolution T hT A x).forward t

noncomputable def EulerSmoothBanachFlow.jacobianEquiv {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : E ≃L[ℝ] E

Jacobian equiv, constructed using ContinuousLinearEquiv.equivOfInverse.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSmoothBanachFlow.backward_hasFDerivAt_label {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : HasFDerivAt (fun (y : E) => (flowData T hT A).backward (↑t) y) ((jacobianEvolution T hT A ((flowData T hT A).backward (↑t) x)).backward t) x

theorem EulerSmoothBanachFlow.backward_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ ↑⊤ fun (y : E) => (flowData T hT A).backward (↑t) y