The actual inverse parent flow needs only continuity as an input. Its differentiability, smooth spatial slices, and jointly continuous spatial jets follow from the prescribed Jacobian and inverse identities.

Joint continuity of the spatial jets of an inverse map

The parameter may range over an arbitrary topological space. Joint continuity of the map itself and of the prescribed coefficient jets, plus the actual equation DY = A ∘ Y, determines joint continuity of every spatial derivative of Y.

theorem EulerGevreyComposition.continuous_iteratedFDeriv_of_fderiv_eq_comp {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (Y : K → E → F) (A : K → F → E →L[ℝ] F) (hY : Continuous (Function.uncurry Y)) (hYdiff : ∀ (t : K), Differentiable ℝ (Y t)) (hA : ∀ (t : K), ContDiff ℝ (↑⊤) (A t)) (hAjet : ∀ (n : ℕ), Continuous fun (p : K × F) => iteratedFDeriv ℝ n (A p.1) p.2) (hDY : ∀ (t : K) (x : E), fderiv ℝ (Y t) x = A t (Y t x)) (n : ℕ) : Continuous fun (p : K × E) => iteratedFDeriv ℝ n (Y p.1) p.2

No continuity of inverse-map derivatives is an input: it follows from the prescribed differential identity and the coefficient's actual jets.

Joint spatial-jet continuity for the prescribed inverse parent flow

The smooth bounded coefficient paths already carry genuine continuous spatial jets. Their evaluation, together with the actual inverse identity, supplies all inverse-flow continuity hypotheses used by Sobolev transport.

theorem EulerMeanCoefficients.SmoothCoefficientPath.jet_joint_continuous {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (n : ℕ) : Continuous fun (p : K × EulerSmoothLimit.Space) => iteratedFDeriv ℝ n (⇑(A.field p.1)) p.2

theorem EulerPacketInverseFlowGevrey.inverseFlow_jet_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hYjoint : Continuous (Function.uncurry Y)) (n : ℕ) : Continuous fun (p : ↑(Set.Icc 0 D.T) × EulerSmoothLimit.Space) => iteratedFDeriv ℝ n (Y p.1) p.2

Every spatial inverse-flow jet is jointly continuous in time and space, derived from the original coefficient path and actual inverse relation.

theorem EulerPacketInverseFlowGevrey.continuousInverse_hasFDerivAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : HasFDerivAt (Y t) ((D.FInv.field t) (Y t x)) x

theorem EulerPacketInverseFlowGevrey.continuousInverse_differentiable {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ↑(Set.Icc 0 D.T)) : Differentiable ℝ (Y t)

theorem EulerPacketInverseFlowGevrey.continuousInverse_contDiff {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ↑(Set.Icc 0 D.T)) : ContDiff ℝ (↑⊤) (Y t)

theorem EulerPacketInverseFlowGevrey.continuousInverse_jet_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (n : ℕ) : Continuous fun (p : ↑(Set.Icc 0 D.T) × EulerSmoothLimit.Space) => iteratedFDeriv ℝ n (Y p.1) p.2