Jointly smooth functions as smooth families of continuous paths

The first derivative is proved with a uniform mean-value remainder estimate. Continuity into the supremum-norm path space follows from compact-open currying. All path derivatives are constructed from genuine parameter derivatives.

noncomputable def NavierStokes.SmoothPathFamily.pathFamily {P E : Type u} [NormedAddCommGroup E] {a b : ℝ} (F : P × ℝ → E) (p : P) : C(↑(Set.Icc a b), E)

Canonical continuous path where the slice is continuous, zero elsewhere. Only values in the stated open parameter domain enter any theorem.

Equations

• NavierStokes.SmoothPathFamily.pathFamily F p = if h : Continuous fun (t : ↑(Set.Icc a b)) => F (p, ↑t) then { toFun := fun (t : ↑(Set.Icc a b)) => F (p, ↑t), continuous_toFun := h } else 0

theorem NavierStokes.SmoothPathFamily.pathFamily_apply {P E : Type u} [NormedAddCommGroup E] {a b : ℝ} (F : P × ℝ → E) (p : P) (hp : Continuous fun (t : ↑(Set.Icc a b)) => F (p, ↑t)) (t : ↑(Set.Icc a b)) : (pathFamily F p) t = F (p, ↑t)

theorem NavierStokes.SmoothPathFamily.slice_continuous {P E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup E] {a b : ℝ} {U : Set P} {F : P × ℝ → E} (hF : ContinuousOn F (U ×ˢ Set.Icc a b)) {p : P} (hp : p ∈ U) : Continuous fun (t : ↑(Set.Icc a b)) => F (p, ↑t)

theorem NavierStokes.SmoothPathFamily.continuousOn_pathFamily {P E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup E] {a b : ℝ} {U : Set P} {F : P × ℝ → E} (hF : ContinuousOn F (U ×ˢ Set.Icc a b)) : ContinuousOn (pathFamily F) U

Compact-open continuity becomes norm continuity because the time interval is compact. No smoothness of a path map is assumed here.

noncomputable def NavierStokes.SmoothPathFamily.flipLinear {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} : C(↑(Set.Icc a b), P →L[ℝ] E) →ₗ[ℝ] P →ₗ[ℝ] C(↑(Set.Icc a b), E)

Flip linear, bundling toFun, toFun, map_add, map_smul and the required compatibility proofs.

Equations

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

theorem NavierStokes.SmoothPathFamily.norm_flipLinear_le {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (g : C(↑(Set.Icc a b), P →L[ℝ] E)) (v : P) : ‖(flipLinear g) v‖ ≤ ‖g‖ * ‖v‖

noncomputable def NavierStokes.SmoothPathFamily.flipPath {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} : C(↑(Set.Icc a b), P →L[ℝ] E) →L[ℝ] P →L[ℝ] C(↑(Set.Icc a b), E)

Reorder the continuous time variable and the bounded linear parameter variable. This is a proved bounded linear operation.

Equations

• NavierStokes.SmoothPathFamily.flipPath = NavierStokes.SmoothPathFamily.flipLinear.mkContinuous₂ 1 ⋯

theorem NavierStokes.SmoothPathFamily.flipPath_apply {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (g : C(↑(Set.Icc a b), P →L[ℝ] E)) (v : P) (t : ↑(Set.Icc a b)) : ((flipPath g) v) t = (g t) v

theorem NavierStokes.SmoothPathFamily.hasFDerivAt_pathFamily {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {U : Set P} (hU : IsOpen U) (F : P × ℝ → E) (G : P × ℝ → P →L[ℝ] E) (hF : ContinuousOn F (U ×ˢ Set.Icc a b)) (hG : ContinuousOn G (U ×ˢ Set.Icc a b)) (hderiv : ∀ p ∈ U, ∀ (t : ↑(Set.Icc a b)), HasFDerivAt (fun (q : P) => F (q, ↑t)) (G (p, ↑t)) p) {p : P} (hp : p ∈ U) : HasFDerivAt (pathFamily F) (flipPath (pathFamily G p)) p

The key uniform differentiability theorem. Joint continuity of the actual slice derivative supplies a common remainder estimate for every time point.

noncomputable def NavierStokes.SmoothPathFamily.parameterDerivative {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (F : P × ℝ → E) (z : P × ℝ) : P →L[ℝ] E

The actual parameter derivative, obtained by restricting the joint derivative to the parameter direction.

Equations

• NavierStokes.SmoothPathFamily.parameterDerivative F z = fderiv ℝ F z ∘SL ContinuousLinearMap.inl ℝ P ℝ

theorem NavierStokes.SmoothPathFamily.contDiffOn_pathFamily_nat {P : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (U : Set P) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (n : ℕ) {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] (F : P × ℝ → W) : ContDiffOn ℝ (↑n) F (U ×ˢ V) → ContDiffOn ℝ (↑n) (pathFamily F) U

Every finite joint differentiability order lifts to the path Banach space. The induction changes the target to the space of parameter derivatives.

theorem NavierStokes.SmoothPathFamily.contDiffOn_pathFamily_of_joint {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (U : Set P) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (F : P × ℝ → E) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ V)) : ContDiffOn ℝ (↑⊤) (pathFamily F) U

Joint C∞ regularity on an open product containing the compact time interval implies C∞ dependence as a path in the supremum norm.

theorem NavierStokes.SmoothPathFamily.iteratedFDeriv_pathFamily_apply {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (U : Set P) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (F : P × ℝ → E) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ V)) {p : P} (hp : p ∈ U) (k : ℕ) (v : Fin k → P) (t : ↑(Set.Icc a b)) : ((iteratedFDeriv ℝ k (pathFamily F) p) v) t = (iteratedFDeriv ℝ k (fun (q : P) => F (q, ↑t)) p) v

Every actual path jet evaluates to the genuine iterated parameter derivative of the original scalar-time slice.

noncomputable def NavierStokes.SmoothPathFamily.odeFamily {P E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (p : P) : C(↑(Set.Icc a b), E)

The actual finite-interval ODE solution for the supplied joint coefficient and forcing families.

Equations

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

theorem NavierStokes.SmoothPathFamily.contDiffOn_odeFamily_of_joint {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) (U : Set P) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (hA : ContDiffOn ℝ (↑⊤) A (U ×ˢ V)) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) : ContDiffOn ℝ (↑⊤) (odeFamily hab A x₀ f) U

Directly closes the joint-smoothness interface of ParametricODE.

theorem NavierStokes.SmoothPathFamily.odeFamily_initial {P E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (p : P) : (odeFamily hab A x₀ f p) ⟨a, ⋯⟩ = x₀ p

theorem NavierStokes.SmoothPathFamily.odeFamily_hasDerivWithinAt {P E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) (U : Set P) (V : Set ℝ) (hI : Set.Icc a b ⊆ V) (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (hA : ContinuousOn A (U ×ˢ V)) (hf : ContinuousOn f (U ×ˢ V)) {p : P} (hp : p ∈ U) (t : ↑(Set.Icc a b)) : HasDerivWithinAt (ParametricODE.extend hab (odeFamily hab A x₀ f p)) ((A (p, ↑t)) ((odeFamily hab A x₀ f p) t) + f (p, ↑t)) (Set.Icc a b) ↑t

The smooth path family satisfies the ODE with the originally supplied coefficient values at every time in the closed interval.