Jointly smooth spatially compact families define smooth time fields. The compact support is common to the time slices, so compact joint continuity upgrades to continuity in the uniform spatial norm at every derivative order.

theorem EulerCompactSmoothTimeField.contDiffOn_spatial_fderiv {P E V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set P} {u : P × E → V} (hu : ContDiffOn ℝ (↑⊤) u (s ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (fun (z : P × E) => fderiv ℝ (fun (x : E) => u (z.1, x)) z.2) (s ×ˢ Set.univ)

Taking a spatial derivative preserves joint smoothness on an arbitrary parameter set. Only the spatial domain needs unique derivatives.

theorem EulerCompactSmoothTimeField.contDiffOn_spatial_jet {P E V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set P} {u : P × E → V} (hu : ContDiffOn ℝ (↑⊤) u (s ×ˢ Set.univ)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : P × E) => iteratedFDeriv ℝ n (fun (x : E) => u (z.1, x)) z.2) (s ×ˢ Set.univ)

Every actual spatial jet is jointly smooth, including at the boundary of the parameter set.

noncomputable def SmoothTimeField.reparametrize {K L E V : Type} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (r : C(L, K)) : SmoothTimeField L E V

Pulling back time by a continuous map preserves all uniform spatial jets.

Equations

• A.reparametrize r = { field := A.field.comp r, smooth := ⋯, jet := fun (n : ℕ) => (A.jet n).comp r, jet_eq := ⋯ }

@[simp]

theorem SmoothTimeField.reparametrize_apply {K L E V : Type} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (r : C(L, K)) (t : L) (x : E) : ((A.reparametrize r).field t) x = (A.field (r t)) x

@[simp]

theorem SmoothTimeField.reparametrize_jet_apply {K L E V : Type} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K E V) (r : C(L, K)) (n : ℕ) (t : L) (x : E) : (((A.reparametrize r).jet n) t) x = ((A.jet n) (r t)) x

@[instance_reducible]

noncomputable def SmoothTimeField.instCompactSmoothTimeField1 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] V)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instCompactSmoothTimeField1 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instCompactSmoothTimeField2 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] V)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instCompactSmoothTimeField2 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instCompactSmoothTimeField3 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] V))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instCompactSmoothTimeField3 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instCompactSmoothTimeField4 {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] V))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• SmoothTimeField.instCompactSmoothTimeField4 n = inferInstance

noncomputable def SmoothTimeField.ofCompactSupportJets {A E V : Type} [TopologicalSpace A] [CompactSpace A] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (u : A × E → V) (hu : Continuous u) (hsmooth : ∀ (t : A), ContDiff ℝ ↑⊤ fun (x : E) => u (t, x)) (hjet : ∀ (n : ℕ), Continuous fun (z : A × E) => iteratedFDeriv ℝ n (fun (x : E) => u (z.1, x)) z.2) (K : Set E) (hK : IsCompact K) (hsupp : ∀ (t : A), (tsupport fun (x : E) => u (t, x)) ⊆ K) : SmoothTimeField A E V

Continuous spatial jets with one common compact support yield a bounded smooth coefficient path. The support condition on derivatives is derived.

Equations

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

@[simp]

theorem SmoothTimeField.ofCompactSupportJets_apply {A E V : Type} [TopologicalSpace A] [CompactSpace A] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (u : A × E → V) (hu : Continuous u) (hsmooth : ∀ (t : A), ContDiff ℝ ↑⊤ fun (x : E) => u (t, x)) (hjet : ∀ (n : ℕ), Continuous fun (z : A × E) => iteratedFDeriv ℝ n (fun (x : E) => u (z.1, x)) z.2) (K : Set E) (hK : IsCompact K) (hsupp : ∀ (t : A), (tsupport fun (x : E) => u (t, x)) ⊆ K) (t : A) (x : E) : ((ofCompactSupportJets u hu hsmooth hjet K hK hsupp).field t) x = u (t, x)

noncomputable def SmoothTimeField.ofContDiffOnCompactSupport {P E V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set P) [CompactSpace ↑s] (u : P × E → V) (hu : ContDiffOn ℝ (↑⊤) u (s ×ˢ Set.univ)) (K : Set E) (hK : IsCompact K) (hsupp : ∀ t ∈ s, (tsupport fun (x : E) => u (t, x)) ⊆ K) : SmoothTimeField (↑s) E V

A jointly smooth family on a compact parameter set with common compact spatial support has all spatial jets continuous in the uniform norm.

Equations

• SmoothTimeField.ofContDiffOnCompactSupport s u hu K hK hsupp = SmoothTimeField.ofCompactSupportJets (fun (z : ↑s × E) => u (↑z.1, z.2)) ⋯ ⋯ ⋯ K hK ⋯

@[simp]

theorem SmoothTimeField.ofContDiffOnCompactSupport_apply {P E V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set P) [CompactSpace ↑s] (u : P × E → V) (hu : ContDiffOn ℝ (↑⊤) u (s ×ˢ Set.univ)) (K : Set E) (hK : IsCompact K) (hsupp : ∀ t ∈ s, (tsupport fun (x : E) => u (t, x)) ⊆ K) (t : ↑s) (x : E) : ((ofContDiffOnCompactSupport s u hu K hK hsupp).field t) x = u (↑t, x)

@[simp]

theorem SmoothTimeField.ofContDiffOnCompactSupport_jet_apply {P E V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set P) [CompactSpace ↑s] (u : P × E → V) (hu : ContDiffOn ℝ (↑⊤) u (s ×ˢ Set.univ)) (K : Set E) (hK : IsCompact K) (hsupp : ∀ t ∈ s, (tsupport fun (x : E) => u (t, x)) ⊆ K) (n : ℕ) (t : ↑s) (x : E) : (((ofContDiffOnCompactSupport s u hu K hK hsupp).jet n) t) x = iteratedFDeriv ℝ n (fun (y : E) => u (↑t, y)) x