Joint parameter and current-time smoothness for linear ODE solutions

A fixed-interval solution is reparametrized from [a,t] onto [0,1], with (p,t) as its parameter. Evaluation at the fixed endpoint 1 is bounded linear on the path space. A compact tube argument supplies genuinely open coefficient neighborhoods, including when t is an original endpoint.

The reparametrized solution is a locally smooth extension of the original solution on the prescribed closed interval. We do not assert smoothness of the original clamped extension outside that interval.

noncomputable def NavierStokes.JointODE.actualSolution {P E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (z : P × ℝ) : E

The actual extension constructed by the Volterra inverse, jointly indexed.

Equations

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

noncomputable def NavierStokes.JointODE.affineTime (a t s : ℝ) : ℝ

The affine time change from the unit interval to [a,t].

Equations

• NavierStokes.JointODE.affineTime a t s = a + s * (t - a)

@[simp]

theorem NavierStokes.JointODE.affineTime_zero (a t : ℝ) : affineTime a t 0 = a

@[simp]

theorem NavierStokes.JointODE.affineTime_one (a t : ℝ) : affineTime a t 1 = t

theorem NavierStokes.JointODE.affineTime_mem {a b t s : ℝ} (ht : t ∈ Set.Icc a b) (hs : s ∈ Set.Icc 0 1) : affineTime a t s ∈ Set.Icc a b

theorem NavierStokes.JointODE.hasDerivAt_affineTime (a t s : ℝ) : HasDerivAt (affineTime a t) (t - a) s

noncomputable def NavierStokes.JointODE.timeMap {P : Type u} (a : ℝ) (w : (P × ℝ) × ℝ) : P × ℝ

(p,t,s) is sent to the original coefficient argument (p,a+s(t-a)).

Equations

• NavierStokes.JointODE.timeMap a w = (w.1.1, NavierStokes.JointODE.affineTime a w.1.2 w.2)

theorem NavierStokes.JointODE.contDiff_timeMap {P : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] (a : ℝ) : ContDiff ℝ (↑⊤) (timeMap a)

noncomputable def NavierStokes.JointODE.rescale {P W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : ℝ) (F : P × ℝ → W) (w : (P × ℝ) × ℝ) : W

Both the linear coefficient and the source acquire the time-change factor.

Equations

• NavierStokes.JointODE.rescale a F w = (w.1.2 - a) • F (NavierStokes.JointODE.timeMap a w)

theorem NavierStokes.JointODE.rescale_contDiffOn {P : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] {a : ℝ} {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] {U : Set P} {V : Set ℝ} {Q : Set (P × ℝ)} {S : Set ℝ} (F : P × ℝ → W) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ V)) (hmap : Set.MapsTo (timeMap a) (Q ×ˢ S) (U ×ˢ V)) : ContDiffOn ℝ (↑⊤) (rescale a F) (Q ×ˢ S)

theorem NavierStokes.JointODE.rescale_slice_continuousOn {P : Type u} [NormedAddCommGroup P] {a b : ℝ} {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] {U : Set P} (F : P × ℝ → W) (hF : ContinuousOn F (U ×ˢ Set.Icc a b)) {z : P × ℝ} (hz : z ∈ U ×ˢ Set.Icc a b) : ContinuousOn (fun (s : ℝ) => rescale a F (z, s)) (Set.Icc 0 1)

noncomputable def NavierStokes.JointODE.reparamSolution {P E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : ℝ) (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (z : P × ℝ) : E

A new solution on the fixed unit interval, evaluated at its fixed right endpoint.

Equations

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

theorem NavierStokes.JointODE.reparamSolution_contDiffAt {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {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)) {z : P × ℝ} (hz : z ∈ U ×ˢ Set.Icc a b) : ContDiffAt ℝ (↑⊤) (reparamSolution a A x₀ f) z

This representative is smooth on a genuine open neighborhood of every point of the original closed parameter/time domain.

theorem NavierStokes.JointODE.actualSolution_initial {P E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (p : P) : actualSolution hab A x₀ f (p, a) = x₀ p

theorem NavierStokes.JointODE.actualSolution_hasDerivAt {P E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {U : Set P} (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (hA : ContinuousOn A (U ×ˢ Set.Icc a b)) (hf : ContinuousOn f (U ×ˢ Set.Icc a b)) {p : P} (hp : p ∈ U) {t : ℝ} (ht : t ∈ Set.Icc a b) : HasDerivAt (fun (s : ℝ) => actualSolution hab A x₀ f (p, s)) ((A (p, t)) (actualSolution hab A x₀ f (p, t)) + f (p, t)) t

The actual extension solves the original ODE at every point of the closed interval.

theorem NavierStokes.JointODE.reparamSolution_eq_actualSolution {P E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {U : Set P} (A : P × ℝ → E →L[ℝ] E) (x₀ : P → E) (f : P × ℝ → E) (hA : ContinuousOn A (U ×ˢ Set.Icc a b)) (hf : ContinuousOn f (U ×ˢ Set.Icc a b)) {z : P × ℝ} (hz : z ∈ U ×ˢ Set.Icc a b) : reparamSolution a A x₀ f z = actualSolution hab A x₀ f z

Uniqueness identifies the fixed-unit-interval construction with the actual Volterra solution at every parameter and every time in the closed interval.

theorem NavierStokes.JointODE.contDiffOn_solutionExtension_joint {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (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 ℝ (↑⊤) (fun (z : P × ℝ) => ParametricODE.solutionExtension hab (SmoothPathFamily.pathFamily A z.1) (x₀ z.1) (SmoothPathFamily.pathFamily f z.1) z.2) (U ×ˢ Set.Icc a b)

Genuine joint parameter/current-time C∞ for the actual solution on the closed interval, including its endpoints in the relative smoothness sense.

theorem NavierStokes.JointODE.contDiffOn_solutionExtension_joint_interior {P E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (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 ℝ (↑⊤) (fun (z : P × ℝ) => ParametricODE.solutionExtension hab (SmoothPathFamily.pathFamily A z.1) (x₀ z.1) (SmoothPathFamily.pathFamily f z.1) z.2) (U ×ˢ Set.Ioo a b)

The interior form used when localizing a solution inside the slot.