The actual flow displacement and material velocity, with every spatial jet in the uniform continuous-time bounded-field space.

Genuine joint time-space regularity of the constructed flow and its inverse. Interior C² uses only the actual first time derivative of the velocity coefficient, together with its existing smooth spatial jets.

Joint time-space differentiability of a genuine smooth family of continuous paths, and the actual mixed derivative of its spatial Jacobian.

noncomputable def EulerSmoothPathJoint.timeSlice {E : Type u_1} {V : Type u_2} [NormedAddCommGroup V] (T : ℝ) (hT : 0 ≤ T) (f : E → C(↑(Set.Icc 0 T), V)) (t : ℝ) (x : E) : V

Time slice, given by extendPath T hT (f x) t.

Equations

• EulerSmoothPathJoint.timeSlice T hT f t x = EulerVolterraConvolution.extendPath T hT (f x) t

theorem EulerSmoothPathJoint.timeSlice_joint_continuous {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] (T : ℝ) (hT : 0 ≤ T) (f : E → C(↑(Set.Icc 0 T), V)) (hf : Continuous f) : Continuous (Function.uncurry (timeSlice T hT f))

noncomputable def EulerSmoothPathJoint.spatialDerivative {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (f : E → C(↑(Set.Icc 0 T), V)) (x : E) : C(↑(Set.Icc 0 T), E →L[ℝ] V)

Spatial derivative as an element of C(Icc (0 : ℝ) T,E →L[ℝ] V).

Equations

• EulerSmoothPathJoint.spatialDerivative T f x = (ContinuousLinearMap.compLeftContinuous ℝ ↑(Set.Icc 0 T) ↑↑(continuousMultilinearCurryFin1 ℝ E V)) (EulerSmoothPathTimeJets.jetFamily T f 1 x)

theorem EulerSmoothPathJoint.spatialDerivative_contDiff {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (f : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spatialDerivative T f)

theorem EulerSmoothPathJoint.spatialDerivative_apply {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (f : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (x : E) (t : ↑(Set.Icc 0 T)) : (spatialDerivative T f x) t = fderiv ℝ (fun (y : E) => (f y) t) x

theorem EulerSmoothPathJoint.timeSlice_hasFDerivAt {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (t : ℝ) (x : E) : HasFDerivAt (timeSlice T hT f t) ((spatialDerivative T f x) (Set.projIcc 0 T hT t)) x

noncomputable def EulerSmoothPathJoint.jointDerivative {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (t : ℝ) (x : E) : ℝ × E →L[ℝ] V

Joint derivative, given by (ContinuousLinearMap.toSpanSingleton ℝ (timeSlice T hT q t x)).coprod (timeSlice T hT (spatialDerivative T f) t x).

Equations

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

theorem EulerSmoothPathJoint.jointDerivative_continuous {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : Continuous q) : Continuous (Function.uncurry (jointDerivative T hT f q))

theorem EulerSmoothPathJoint.joint_hasFDerivAt {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : HasFDerivAt (Function.uncurry (timeSlice T hT f)) (jointDerivative T hT f q t x) (t, x)

theorem EulerSmoothPathJoint.joint_contDiffAt_one {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 1 (Function.uncurry (timeSlice T hT f)) (t, x)

theorem EulerSmoothPathJoint.spatialDerivative_time {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (spatialDerivative T f x)) ((spatialDerivative T q x) t) (Set.Icc 0 T) ↑t

The actual acceleration of the constructed nonlinear flow is the material derivative of its velocity, including the one-sided endpoint identities. All coefficient time derivatives are literal hypotheses.

noncomputable def EulerSmoothBanachFlow.accelerationFamily {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) : C(↑(Set.Icc 0 T), E)

Acceleration family, given by A₁.superposition (pathFamily T hT A x) + multiplier (A.derivative.superposition (pathFamily T hT A x)) (velocityFamily T hT A x).

Equations

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

theorem EulerSmoothBanachFlow.accelerationFamily_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) (t : ↑(Set.Icc 0 T)) : (accelerationFamily T hT A A₁ x) t = (A₁.field t) ((flowData T hT A).forward (↑t) x) + (fderiv ℝ (⇑(A.field t)) ((flowData T hT A).forward (↑t) x)) ((A.field t) ((flowData T hT A).forward (↑t) x))

theorem EulerSmoothBanachFlow.pathFamily_time_derivative {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((pathFamily T hT A) x)) ((velocityFamily T hT A x) t) (Set.Icc 0 T) ↑t

theorem EulerSmoothBanachFlow.velocityFamily_time_derivative_interior {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (x : E) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T hT (velocityFamily T hT A x)) ((accelerationFamily T hT A A₁ x) ⟨t, ⋯⟩) t

theorem EulerSmoothBanachFlow.velocityFamily_time_derivative {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (velocityFamily T hT A x)) ((accelerationFamily T hT A A₁ x) t) (Set.Icc 0 T) ↑t

theorem EulerSmoothBanachFlow.forward_second_time_derivative {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (s : ℝ) => deriv (fun (r : ℝ) => (flowData T hT A).forward r x) s) ((accelerationFamily T hT A A₁ x) t) (Set.Icc 0 T) ↑t

theorem EulerSmoothBanachFlow.accelerationFamily_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) : ContDiff ℝ (↑⊤) (accelerationFamily T hT A A₁)

theorem EulerSmoothBanachFlow.forward_joint_hasFDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : HasFDerivAt (Function.uncurry (flowData T hT A).forward) (EulerSmoothPathJoint.jointDerivative T hT (⇑(pathFamily T hT A)) (velocityFamily T hT A) t x) (t, x)

theorem EulerSmoothBanachFlow.forward_joint_contDiffAt_one {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 1 (Function.uncurry (flowData T hT A).forward) (t, x)

theorem EulerSmoothBanachFlow.forward_jointDerivative_contDiffAt_one {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 1 (Function.uncurry (EulerSmoothPathJoint.jointDerivative T hT (⇑(pathFamily T hT A)) (velocityFamily T hT A))) (t, x)

theorem EulerSmoothBanachFlow.forward_joint_contDiffAt_two {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 2 (Function.uncurry (flowData T hT A).forward) (t, x)

def EulerSmoothBanachFlow.timeLiftEquiv {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (J : E ≃L[ℝ] E) (v : E) : (ℝ × E) ≃L[ℝ] ℝ × E

Time lift equiv, constructed using ContinuousLinearEquiv.equivOfInverse.

Equations

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

noncomputable def EulerSmoothBanachFlow.liftForward {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (p : ℝ × E) : ℝ × E

Lift forward, given by (p.1, (flowData T hT A).forward p.1 p.2).

Equations

• EulerSmoothBanachFlow.liftForward T hT A p = (p.1, (EulerSmoothBanachFlow.flowData T hT A).forward p.1 p.2)

noncomputable def EulerSmoothBanachFlow.liftBackward {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (p : ℝ × E) : ℝ × E

Lift backward, given by (p.1, (flowData T hT A).backward p.1 p.2).

Equations

• EulerSmoothBanachFlow.liftBackward T hT A p = (p.1, (EulerSmoothBanachFlow.flowData T hT A).backward p.1 p.2)

theorem EulerSmoothBanachFlow.liftForward_hasFDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : HasFDerivAt (liftForward T hT A) ↑(timeLiftEquiv (jacobianEquiv T hT A ⟨t, ⋯⟩ x) ((velocityFamily T hT A x) ⟨t, ⋯⟩)) (t, x)

theorem EulerSmoothBanachFlow.liftBackward_contDiffAt_two {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 2 (liftBackward T hT A) (t, x)

theorem EulerSmoothBanachFlow.backward_joint_contDiffAt_two {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : E) : ContDiffAt ℝ 2 (Function.uncurry (flowData T hT A).backward) (t, x)

Constructing literal bounded smooth coefficient paths from an actual smooth path family and uniform bounds on its differentiated evolution.

Uniform bounds on a genuine time derivative turn a continuous family of paths into a continuous path of bounded fields.

def EulerBoundedPathFamily.boundedSlice {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (f : X → C(↑(Set.Icc 0 T), V)) (hf : Continuous f) (C : ℝ) (hC : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(f x) t‖ ≤ C) (t : ↑(Set.Icc 0 T)) : BoundedContinuousFunction X V

Bounded slice, given by BoundedContinuousFunction.ofNormedAddCommGroup (fun x => f x t) ((ContinuousMap.evalCLM ℝ t).continuous.comp hf) C (hC t).

Equations

• EulerBoundedPathFamily.boundedSlice T f hf C hC t = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : X) => (f x) t) ⋯ C ⋯

theorem EulerBoundedPathFamily.boundedSlice_lipschitz {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : X → C(↑(Set.Icc 0 T), V)) (hf : Continuous f) (C D : ℝ) (hC : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(f x) t‖ ≤ C) (hD : 0 ≤ D) (hq : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(q x) t‖ ≤ D) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) : LipschitzWith ⟨D, hD⟩ (boundedSlice T f hf C hC)

def EulerBoundedPathFamily.boundedPath {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : X → C(↑(Set.Icc 0 T), V)) (hf : Continuous f) (C D : ℝ) (hC : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(f x) t‖ ≤ C) (hD : 0 ≤ D) (hq : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(q x) t‖ ≤ D) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) : C(↑(Set.Icc 0 T), BoundedContinuousFunction X V)

Bounded path, bundling toFun, continuous_toFun.

Equations

• EulerBoundedPathFamily.boundedPath T hT f q hf C D hC hD hq hd = { toFun := EulerBoundedPathFamily.boundedSlice T f hf C hC, continuous_toFun := ⋯ }

@[simp]

theorem EulerBoundedPathFamily.boundedPath_apply {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : X → C(↑(Set.Icc 0 T), V)) (hf : Continuous f) (C D : ℝ) (hC : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(f x) t‖ ≤ C) (hD : 0 ≤ D) (hq : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(q x) t‖ ≤ D) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) (x : X) : ((boundedPath T hT f q hf C D hC hD hq hd) t) x = (f x) t

theorem EulerBoundedPathFamily.boundedPath_norm {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : X → C(↑(Set.Icc 0 T), V)) (hf : Continuous f) (C D : ℝ) (hC : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(f x) t‖ ≤ C) (hD : 0 ≤ D) (hq : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖(q x) t‖ ≤ D) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (hCnonneg : 0 ≤ C) : ‖boundedPath T hT f q hf C D hC hD hq hd‖ ≤ C

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldFromPaths1 {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.instSmoothTimeFieldFromPaths1 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldFromPaths2 {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.instSmoothTimeFieldFromPaths2 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldFromPaths3 {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.instSmoothTimeFieldFromPaths3 n = inferInstance

@[instance_reducible]

noncomputable def SmoothTimeField.instSmoothTimeFieldFromPaths4 {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.instSmoothTimeFieldFromPaths4 n = inferInstance

theorem SmoothTimeField.value_bound {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (f : E → C(↑(Set.Icc 0 T), V)) (C : ℕ → ℝ) (hC : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x‖ ≤ C n) (t : ↑(Set.Icc 0 T)) (x : E) : ‖(f x) t‖ ≤ C 0

theorem SmoothTimeField.derivativeBound_nonneg {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (q : E → C(↑(Set.Icc 0 T), V)) (D : ℕ → ℝ) (hD : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (q y) t) x‖ ≤ D n) (n : ℕ) : 0 ≤ D n

noncomputable def SmoothTimeField.ofPathFamily {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (C D : ℕ → ℝ) (hC : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x‖ ≤ C n) (hD : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (q y) t) x‖ ≤ D n) : SmoothTimeField (↑(Set.Icc 0 T)) E V

Of path family, bundling field, smooth, change, jet and the required compatibility proofs.

Equations

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

@[simp]

theorem SmoothTimeField.ofPathFamily_apply {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (C D : ℕ → ℝ) (hC : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x‖ ≤ C n) (hD : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (q y) t) x‖ ≤ D n) (t : ↑(Set.Icc 0 T)) (x : E) : ((ofPathFamily T hT f q hf hq hd C D hC hD).field t) x = (f x) t

@[simp]

theorem SmoothTimeField.ofPathFamily_jet_apply {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (C D : ℕ → ℝ) (hC : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x‖ ≤ C n) (hD : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (q y) t) x‖ ≤ D n) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : (((ofPathFamily T hT f q hf hq hd C D hC hD).jet n) t) x = iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x

theorem SmoothTimeField.ofPathFamily_jet_norm {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (C D : ℕ → ℝ) (hC : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x‖ ≤ C n) (hD : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (q y) t) x‖ ≤ D n) (n : ℕ) : ‖(ofPathFamily T hT f q hf hq hd C D hC hD).jet n‖ ≤ C n

theorem SmoothTimeField.ofPathFamily_field_norm {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (T : ℝ) (hT : 0 ≤ T) (f q : E → C(↑(Set.Icc 0 T), V)) (hf : ContDiff ℝ (↑⊤) f) (hq : ContDiff ℝ (↑⊤) q) (hd : ∀ (x : E) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (f x)) ((q x) t) (Set.Icc 0 T) ↑t) (C D : ℕ → ℝ) (hC : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (f y) t) x‖ ≤ C n) (hD : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => (q y) t) x‖ ≤ D n) : ‖(ofPathFamily T hT f q hf hq hd C D hC hD).field‖ ≤ C 0

@[instance_reducible]

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

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

Equations

• EulerSmoothBanachFlow.instSmoothFlowCoefficientPaths1 n = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSmoothBanachFlow.instSmoothFlowCoefficientPaths2 n = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSmoothBanachFlow.instSmoothFlowCoefficientPaths3 n = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSmoothBanachFlow.instSmoothFlowCoefficientPaths4 n = inferInstance

theorem EulerSmoothBanachFlow.displacementFamily_time_derivative {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (x : E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (displacementFamily T hT A x)) ((velocityFamily T hT A x) t) (Set.Icc 0 T) ↑t

theorem EulerSmoothBanachFlow.displacementFamily_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => (displacementFamily T hT A y) t) x‖ ≤ B * T * (4 * R) ^ n * ↑n.factorial ^ 2

theorem EulerSmoothBanachFlow.velocityFamily_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => (velocityFamily T hT A y) t) x‖ ≤ B * EulerSmoothFlowGevrey.flowRadius B R T R ^ n * ↑n.factorial ^ 2

noncomputable def EulerSmoothBanachFlow.displacementCoefficient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) : SmoothTimeField (↑(Set.Icc 0 T)) E E

Displacement coefficient, constructed using SmoothTimeField.ofPathFamily.

Equations

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

@[simp]

theorem EulerSmoothBanachFlow.displacementCoefficient_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (t : ↑(Set.Icc 0 T)) (x : E) : ((displacementCoefficient T hT A B R hB hR hsmall hb).field t) x = (flowData T hT A).forward (↑t) x - x

theorem EulerSmoothBanachFlow.displacementCoefficient_jet_norm {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) : ‖(displacementCoefficient T hT A B R hB hR hsmall hb).jet n‖ ≤ B * T * (4 * R) ^ n * ↑n.factorial ^ 2

theorem EulerSmoothBanachFlow.accelerationFamily_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => (accelerationFamily T hT A A₁ y) t) x‖ ≤ (B₁ + 3 * B ^ 2 * R) * EulerSmoothFlowGevrey.flowRadius B R T (4 * R + R₁) ^ n * ↑n.factorial ^ 2

noncomputable def EulerSmoothBanachFlow.velocityCoefficient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) : SmoothTimeField (↑(Set.Icc 0 T)) E E

Velocity coefficient, constructed using SmoothTimeField.ofPathFamily.

Equations

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

@[simp]

theorem EulerSmoothBanachFlow.velocityCoefficient_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) (t : ↑(Set.Icc 0 T)) (x : E) : ((velocityCoefficient T hT A B R hB hR hsmall hb A₁ htime B₁ R₁ hB₁ hR₁ hb₁).field t) x = (A.field t) ((flowData T hT A).forward (↑t) x)

theorem EulerSmoothBanachFlow.velocityCoefficient_jet_norm {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) (B₁ R₁ : ℝ) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) (n : ℕ) : ‖(velocityCoefficient T hT A B R hB hR hsmall hb A₁ htime B₁ R₁ hB₁ hR₁ hb₁).jet n‖ ≤ B * EulerSmoothFlowGevrey.flowRadius B R T R ^ n * ↑n.factorial ^ 2