Smooth dependence of finite-interval linear ODE solutions

The coefficient and forcing are elements of spaces of continuous paths with the supremum norm. The actual integral equation is solved by an invertible Volterra operator. Smooth inversion then gives parameter dependence without assuming smoothness of a pre-existing family of solutions.

@[reducible, inline]

abbrev NavierStokes.ParametricODE.Curve (a b : ℝ) (E : Type u_2) [TopologicalSpace E] : Type u_2

Curve: an abbreviation for C(Icc a b, E).

Equations

• NavierStokes.ParametricODE.Curve a b E = C(↑(Set.Icc a b), E)

@[reducible, inline]

abbrev NavierStokes.ParametricODE.Coefficient (a b : ℝ) (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_2

Coefficient: an abbreviation for Curve a b (E →L[ℝ] E).

Equations

• NavierStokes.ParametricODE.Coefficient a b E = NavierStokes.ParametricODE.Curve a b (E →L[ℝ] E)

noncomputable def NavierStokes.ParametricODE.extend {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (f : Curve a b E) (t : ℝ) : E

Extend, given by f (projIcc a b hab t).

Equations

• NavierStokes.ParametricODE.extend hab f t = f (Set.projIcc a b hab t)

theorem NavierStokes.ParametricODE.continuous_extend {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (f : Curve a b E) : Continuous (extend hab f)

theorem NavierStokes.ParametricODE.extend_coe {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (f : Curve a b E) (t : ↑(Set.Icc a b)) : extend hab f ↑t = f t

noncomputable def NavierStokes.ParametricODE.integralPath {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (f : Curve a b E) : Curve a b E

Integral path as an element of Curve a b E.

Equations

• NavierStokes.ParametricODE.integralPath hab f = { toFun := fun (t : ↑(Set.Icc a b)) => ∫ (s : ℝ) in a..↑t, NavierStokes.ParametricODE.extend hab f s, continuous_toFun := ⋯ }

theorem NavierStokes.ParametricODE.norm_integralPath_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (f : Curve a b E) : ‖integralPath hab f‖ ≤ (b - a) * ‖f‖

noncomputable def NavierStokes.ParametricODE.integrator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) : Curve a b E →L[ℝ] Curve a b E

Integrator, constructed using LinearMap.mkContinuous.

Equations

• NavierStokes.ParametricODE.integrator hab = { toFun := NavierStokes.ParametricODE.integralPath hab, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (b - a) ⋯

theorem NavierStokes.ParametricODE.integrator_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (f : Curve a b E) (t : ↑(Set.Icc a b)) : ((integrator hab) f) t = ∫ (s : ℝ) in a..↑t, extend hab f s

noncomputable def NavierStokes.ParametricODE.applyCoefficient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : Coefficient a b E) (u : Curve a b E) : Curve a b E

Apply coefficient, given by ⟨fun t => A t (u t), A.continuous.clm_apply u.continuous⟩.

Equations

• NavierStokes.ParametricODE.applyCoefficient A u = { toFun := fun (t : ↑(Set.Icc a b)) => (A t) (u t), continuous_toFun := ⋯ }

theorem NavierStokes.ParametricODE.norm_applyCoefficient_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : Coefficient a b E) (u : Curve a b E) : ‖applyCoefficient A u‖ ≤ ‖A‖ * ‖u‖

noncomputable def NavierStokes.ParametricODE.coefficientLinear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} : Coefficient a b E →ₗ[ℝ] Curve a b E →ₗ[ℝ] Curve a b E

Coefficient 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.

noncomputable def NavierStokes.ParametricODE.coefficientAction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} : Coefficient a b E →L[ℝ] Curve a b E →L[ℝ] Curve a b E

Coefficient action as an element of Coefficient a b E →L[ℝ] Curve a b E →L[ℝ] Curve a b E.

Equations

• NavierStokes.ParametricODE.coefficientAction = NavierStokes.ParametricODE.coefficientLinear.mkContinuous₂ 1 ⋯

theorem NavierStokes.ParametricODE.coefficientAction_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : Coefficient a b E) (u : Curve a b E) (t : ↑(Set.Icc a b)) : ((coefficientAction A) u) t = (A t) (u t)

noncomputable def NavierStokes.ParametricODE.volterra {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) : Coefficient a b E →L[ℝ] Curve a b E →L[ℝ] Curve a b E

Volterra, given by ((ContinuousLinearMap.compL ℝ (Curve a b E) (Curve a b E) (Curve a b E)) (integrator hab)).comp (coefficientAction (E := E)).

Equations

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

theorem NavierStokes.ParametricODE.volterra_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (u : Curve a b E) (t : ↑(Set.Icc a b)) : (((volterra hab) A) u) t = ∫ (s : ℝ) in a..↑t, (extend hab A s) (extend hab u s)

theorem NavierStokes.ParametricODE.norm_volterra_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (u : Curve a b E) : ‖((volterra hab) A) u‖ ≤ (b - a) * ‖A‖ * ‖u‖

noncomputable def NavierStokes.ParametricODE.homogeneousSystem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) : TangentODE.IntervalSystem E

Homogeneous system as an element of TangentODE.IntervalSystem E.

Equations

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

theorem NavierStokes.ParametricODE.volterra_eq_next {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) : ⇑((volterra hab) A) = (homogeneousSystem hab A).next

theorem NavierStokes.ParametricODE.volterra_contracting_iterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) : ∃ (N : ℕ) (K : NNReal), ContractingWith K (⇑((volterra hab) A))^[N]

theorem NavierStokes.ParametricODE.affine_iterate_sub {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (L : X →L[ℝ] X) (g : X) (n : ℕ) (u w : X) : (fun (x : X) => g + L x)^[n] u - (fun (x : X) => g + L x)^[n] w = (⇑L)^[n] u - (⇑L)^[n] w

theorem NavierStokes.ParametricODE.id_sub_isInvertible {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (L : X →L[ℝ] X) (hL : ∃ (N : ℕ) (K : NNReal), ContractingWith K (⇑L)^[N]) : (ContinuousLinearMap.id ℝ X - L).IsInvertible

theorem NavierStokes.ParametricODE.contDiff_inverse_family {X : Type u_2} {Q : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (L : Q → X →L[ℝ] X) (hL : ContDiff ℝ (↑⊤) L) (hInv : ∀ (q : Q), (L q).IsInvertible) : ContDiff ℝ ↑⊤ fun (q : Q) => (L q).inverse

noncomputable def NavierStokes.ParametricODE.equationOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) : Curve a b E →L[ℝ] Curve a b E

Equation operator, given by ContinuousLinearMap.id ℝ (Curve a b E) - volterra (E := E) hab A.

Equations

• NavierStokes.ParametricODE.equationOperator hab A = ContinuousLinearMap.id ℝ (NavierStokes.ParametricODE.Curve a b E) - (NavierStokes.ParametricODE.volterra hab) A

theorem NavierStokes.ParametricODE.equationOperator_isInvertible {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) : (equationOperator hab A).IsInvertible

noncomputable def NavierStokes.ParametricODE.resolvent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) : Curve a b E →L[ℝ] Curve a b E

Resolvent of the actual Volterra integral equation on the full finite interval.

Equations

• NavierStokes.ParametricODE.resolvent hab A = (NavierStokes.ParametricODE.equationOperator hab A).inverse

theorem NavierStokes.ParametricODE.contDiff_resolvent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) : ContDiff ℝ (↑⊤) (resolvent hab)

noncomputable def NavierStokes.ParametricODE.constantCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} : E →L[ℝ] Curve a b E

Constant curve, constructed using LinearMap.mkContinuous.

Equations

• NavierStokes.ParametricODE.constantCurve = { toFun := ContinuousMap.const ↑(Set.Icc a b), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

noncomputable def NavierStokes.ParametricODE.source {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (x₀ : E) (f : Curve a b E) : Curve a b E

Source, given by constantCurve x₀ + integrator hab f.

Equations

• NavierStokes.ParametricODE.source hab x₀ f = NavierStokes.ParametricODE.constantCurve x₀ + (NavierStokes.ParametricODE.integrator hab) f

noncomputable def NavierStokes.ParametricODE.solution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) : Curve a b E

The constructed solution as a continuous path, not an assumed solution family.

Equations

• NavierStokes.ParametricODE.solution hab A x₀ f = (NavierStokes.ParametricODE.resolvent hab A) (NavierStokes.ParametricODE.source hab x₀ f)

theorem NavierStokes.ParametricODE.resolvent_equation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (g : Curve a b E) : (equationOperator hab A) ((resolvent hab A) g) = g

theorem NavierStokes.ParametricODE.solution_integralEquation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) : solution hab A x₀ f = constantCurve x₀ + (integrator hab) (applyCoefficient A (solution hab A x₀ f) + f)

theorem NavierStokes.ParametricODE.solution_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) : (solution hab A x₀ f) ⟨a, ⋯⟩ = x₀

noncomputable def NavierStokes.ParametricODE.solutionExtension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) (t : ℝ) : E

Solution extension, given by x₀ + ∫ s in a..t, extend hab (applyCoefficient A (solution hab A x₀ f) + f) s.

Equations

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

theorem NavierStokes.ParametricODE.solutionExtension_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) (t : ↑(Set.Icc a b)) : solutionExtension hab A x₀ f ↑t = (solution hab A x₀ f) t

theorem NavierStokes.ParametricODE.solutionExtension_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) (t : ↑(Set.Icc a b)) : HasDerivAt (solutionExtension hab A x₀ f) ((A t) (solutionExtension hab A x₀ f ↑t) + f t) ↑t

The constructed path has a differentiable extension satisfying the actual ODE at every point of the prescribed interval.

theorem NavierStokes.ParametricODE.solution_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) (t : ↑(Set.Icc a b)) : HasDerivWithinAt (extend hab (solution hab A x₀ f)) ((A t) ((solution hab A x₀ f) t) + f t) (Set.Icc a b) ↑t

theorem NavierStokes.ParametricODE.fderiv_resolvent_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → Coefficient a b E) (g : P → Curve a b E) {p : P} {A' : P →L[ℝ] Coefficient a b E} {g' : P →L[ℝ] Curve a b E} (hA : HasFDerivAt A A' p) (hg : HasFDerivAt g g' p) (v : P) : (fderiv ℝ (fun (q : P) => (resolvent hab (A q)) (g q)) p) v = (resolvent hab (A p)) (g' v + ((volterra hab) (A' v)) ((resolvent hab (A p)) (g p)))

Differentiating the actual inverse equation gives the first variation in every direction of an arbitrary normed parameter space.

theorem NavierStokes.ParametricODE.parameter_derivative_eq_solution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → Coefficient a b E) (x₀ : P → E) (f : P → Curve a b E) {p : P} {A' : P →L[ℝ] Coefficient a b E} {x₀' : P →L[ℝ] E} {f' : P →L[ℝ] Curve a b E} (hA : HasFDerivAt A A' p) (hx₀ : HasFDerivAt x₀ x₀' p) (hf : HasFDerivAt f f' p) (v : P) : (fderiv ℝ (fun (q : P) => solution hab (A q) (x₀ q) (f q)) p) v = solution hab (A p) (x₀' v) (applyCoefficient (A' v) (solution hab (A p) (x₀ p) (f p)) + f' v)

The actual parameter derivative is the solution of the variational equation, with source (∂A)u + ∂f and initial value ∂x₀.

theorem NavierStokes.ParametricODE.parameter_derivative_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → Coefficient a b E) (x₀ : P → E) (f : P → Curve a b E) {p : P} {A' : P →L[ℝ] Coefficient a b E} {x₀' : P →L[ℝ] E} {f' : P →L[ℝ] Curve a b E} (hA : HasFDerivAt A A' p) (hx₀ : HasFDerivAt x₀ x₀' p) (hf : HasFDerivAt f f' p) (v : P) (t : ↑(Set.Icc a b)) : HasDerivWithinAt (extend hab ((fderiv ℝ (fun (q : P) => solution hab (A q) (x₀ q) (f q)) p) v)) (((A p) t) (((fderiv ℝ (fun (q : P) => solution hab (A q) (x₀ q) (f q)) p) v) t) + ((A' v) t) ((solution hab (A p) (x₀ p) (f p)) t) + (f' v) t) (Set.Icc a b) ↑t

theorem NavierStokes.ParametricODE.norm_constantCurve_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (x : E) : ‖constantCurve x‖ ≤ ‖x‖

theorem NavierStokes.ParametricODE.norm_source_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (x₀ : E) (f : Curve a b E) : ‖source hab x₀ f‖ ≤ ‖x₀‖ + (b - a) * ‖f‖

theorem NavierStokes.ParametricODE.norm_solution_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : Coefficient a b E) (x₀ : E) (f : Curve a b E) : ‖solution hab A x₀ f‖ ≤ ‖resolvent hab A‖ * (‖x₀‖ + (b - a) * ‖f‖)

A finite stability bound in terms of the norm of the actual inverse operator.

theorem NavierStokes.ParametricODE.norm_parameter_derivative_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → Coefficient a b E) (x₀ : P → E) (f : P → Curve a b E) {p : P} {A' : P →L[ℝ] Coefficient a b E} {x₀' : P →L[ℝ] E} {f' : P →L[ℝ] Curve a b E} (hA : HasFDerivAt A A' p) (hx₀ : HasFDerivAt x₀ x₀' p) (hf : HasFDerivAt f f' p) (v : P) : ‖(fderiv ℝ (fun (q : P) => solution hab (A q) (x₀ q) (f q)) p) v‖ ≤ ‖resolvent hab (A p)‖ * (‖x₀' v‖ + (b - a) * (‖A' v‖ * ‖solution hab (A p) (x₀ p) (f p)‖ + ‖f' v‖))

theorem NavierStokes.ParametricODE.contDiff_solution_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → Coefficient a b E) (x₀ : P → E) (f : P → Curve a b E) (hA : ContDiff ℝ (↑⊤) A) (hx₀ : ContDiff ℝ (↑⊤) x₀) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ ↑⊤ fun (p : P) => solution hab (A p) (x₀ p) (f p)

Full smooth dependence in the supremum-norm spaces of coefficient and forcing paths. Smoothness of the solution map is a conclusion.

theorem NavierStokes.ParametricODE.contDiffOn_solution_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : Set P} (A : P → Coefficient a b E) (x₀ : P → E) (f : P → Curve a b E) (hA : ContDiffOn ℝ (↑⊤) A s) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ s) (hf : ContDiffOn ℝ (↑⊤) f s) : ContDiffOn ℝ (↑⊤) (fun (p : P) => solution hab (A p) (x₀ p) (f p)) s

theorem NavierStokes.ParametricODE.parameter_derivatives_bounded_on_compact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → Coefficient a b E) (x₀ : P → E) (f : P → Curve a b E) (hA : ContDiff ℝ (↑⊤) A) (hx₀ : ContDiff ℝ (↑⊤) x₀) (hf : ContDiff ℝ (↑⊤) f) {s : Set P} (hs : IsCompact s) (m : ℕ) : ∃ (C : ℝ), ∀ p ∈ s, ‖iteratedFDeriv ℝ m (fun (q : P) => solution hab (A q) (x₀ q) (f q)) p‖ ≤ C

Every parameter derivative has a finite uniform bound on a compact parameter set. This does not assert polynomial dependence of those bounds on a band index.