Weighted estimates for actual parameter derivatives of linear ODE solutions

Parameter derivatives are genuine iterated Fréchet derivatives in prescribed directions. The differentiated Volterra equation gives a triangular system; the energy estimate, rather than an uncontrolled inverse norm, estimates it.

noncomputable def NavierStokes.WeightedODEJets.directional {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : P → E) (v : P) : P → E

One actual parameter derivative in a fixed direction.

Equations

• NavierStokes.WeightedODEJets.directional f v p = (fderiv ℝ f p) v

noncomputable def NavierStokes.WeightedODEJets.jet {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : P → E) (l : List P) : P → E

Successive actual directional Fréchet derivatives. Directions are applied from the head of the word to its tail; the empty word means order zero.

Equations

• NavierStokes.WeightedODEJets.jet f l = List.foldl (fun (g : P → E) (v : P) => NavierStokes.WeightedODEJets.directional g v) f l

@[simp]

theorem NavierStokes.WeightedODEJets.jet_nil {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : P → E) : jet f [] = f

@[simp]

theorem NavierStokes.WeightedODEJets.jet_cons {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : P → E) (v : P) (l : List P) : jet f (v :: l) = jet (directional f v) l

def NavierStokes.WeightedODEJets.UnitWord {P : Type u_1} [NormedAddCommGroup P] (l : List P) : Prop

Restricting all directions to the unit ball converts the estimates to uniform bounds for all mixed parameter derivatives of a given order.

Equations

• NavierStokes.WeightedODEJets.UnitWord l = ∀ v ∈ l, ‖v‖ ≤ 1

@[simp]

theorem NavierStokes.WeightedODEJets.unitWord_nil {P : Type u_1} [NormedAddCommGroup P] : UnitWord []

@[simp]

theorem NavierStokes.WeightedODEJets.unitWord_cons {P : Type u_1} [NormedAddCommGroup P] (v : P) (l : List P) : UnitWord (v :: l) ↔ ‖v‖ ≤ 1 ∧ UnitWord l

theorem NavierStokes.WeightedODEJets.contDiffOn_directional {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (v : P) : ContDiffOn ℝ (↑⊤) (directional f v) U

theorem NavierStokes.WeightedODEJets.contDiffOn_jet {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (l : List P) : ContDiffOn ℝ (↑⊤) (jet f l) U

theorem NavierStokes.WeightedODEJets.directional_congr {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f g : P → E} (heq : Set.EqOn f g U) (v : P) : Set.EqOn (directional f v) (directional g v) U

theorem NavierStokes.WeightedODEJets.jet_congr {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f g : P → E} (heq : Set.EqOn f g U) (l : List P) : Set.EqOn (jet f l) (jet g l) U

theorem NavierStokes.WeightedODEJets.directional_add {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f g : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) (v : P) : Set.EqOn (directional (fun (p : P) => f p + g p) v) (fun (p : P) => directional f v p + directional g v p) U

theorem NavierStokes.WeightedODEJets.jet_add {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f g : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) (l : List P) : Set.EqOn (jet (fun (p : P) => f p + g p) l) (fun (p : P) => jet f l p + jet g l p) U

theorem NavierStokes.WeightedODEJets.directional_clm {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set P} (hU : IsOpen U) {f : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] F) (v : P) : Set.EqOn (directional (fun (p : P) => L (f p)) v) (fun (p : P) => L (directional f v p)) U

theorem NavierStokes.WeightedODEJets.jet_clm {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set P} (hU : IsOpen U) {f : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] F) (l : List P) : Set.EqOn (jet (fun (p : P) => L (f p)) l) (fun (p : P) => L (jet f l p)) U

theorem NavierStokes.WeightedODEJets.jet_ofFn_reverse {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (n : ℕ) (v : Fin n → P) {p : P} (hp : p ∈ U) : jet f (List.ofFn v).reverse p = (iteratedFDeriv ℝ n f p) v

The word formulation is exactly Mathlib's iterated Fréchet derivative, with the reversal dictated by its convention for the order of arguments.

theorem NavierStokes.WeightedODEJets.norm_jet_le_iteratedFDeriv {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set P} (hU : IsOpen U) {f : P → E} (hf : ContDiffOn ℝ (↑⊤) f U) (l : List P) {p : P} (hp : p ∈ U) (hl : UnitWord l) : ‖jet f l p‖ ≤ ‖iteratedFDeriv ℝ l.length f p‖

A bound for the ordinary multilinear derivative controls every word of unit directions, including the empty word.

theorem NavierStokes.WeightedODEJets.multilinear_norm_le_of_unit {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (T : P [×n]→L[ℝ] E) {B : ℝ} (hB : 0 ≤ B) (hT : ∀ (v : Fin n → P), (∀ (i : Fin n), ‖v i‖ ≤ 1) → ‖T v‖ ≤ B) : ‖T‖ ≤ B

Unit-direction bounds control the full multilinear norm, also at order zero.

noncomputable def NavierStokes.WeightedODEJets.productJet {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : P → ParametricODE.Coefficient a b E) (u : P → ParametricODE.Curve a b E) (l : List P) : P → ParametricODE.Curve a b E

The full Leibniz expansion, retaining ordered differentiation and therefore automatically retaining every mixed-term multiplicity.

Equations

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

noncomputable def NavierStokes.WeightedODEJets.crossJet {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : P → ParametricODE.Coefficient a b E) (u : P → ParametricODE.Curve a b E) (l : List P) : P → ParametricODE.Curve a b E

The proper Leibniz terms: at least one derivative hits the coefficient, so every solution derivative in this expression has strictly lower order.

Equations

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

theorem NavierStokes.WeightedODEJets.productJet_split {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : P → ParametricODE.Coefficient a b E) (u : P → ParametricODE.Curve a b E) (l : List P) (p : P) : productJet A u l p = ParametricODE.applyCoefficient (A p) (jet u l p) + crossJet A u l p

theorem NavierStokes.WeightedODEJets.directional_product {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {U : Set P} (hU : IsOpen U) {A : P → ParametricODE.Coefficient a b E} {u : P → ParametricODE.Curve a b E} (hA : ContDiffOn ℝ (↑⊤) A U) (hu : ContDiffOn ℝ (↑⊤) u U) (v : P) : Set.EqOn (directional (fun (p : P) => ParametricODE.applyCoefficient (A p) (u p)) v) (fun (p : P) => ParametricODE.applyCoefficient (directional A v p) (u p) + ParametricODE.applyCoefficient (A p) (directional u v p)) U

theorem NavierStokes.WeightedODEJets.jet_product {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {U : Set P} (hU : IsOpen U) {A : P → ParametricODE.Coefficient a b E} {u : P → ParametricODE.Curve a b E} (hA : ContDiffOn ℝ (↑⊤) A U) (hu : ContDiffOn ℝ (↑⊤) u U) (l : List P) : Set.EqOn (jet (fun (p : P) => ParametricODE.applyCoefficient (A p) (u p)) l) (productJet A u l) U

theorem NavierStokes.WeightedODEJets.norm_productJet_le {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : P → ParametricODE.Coefficient a b E) (u : P → ParametricODE.Curve a b E) (l : List P) (p : P) (t : ↑(Set.Icc a b)) {M B : ℝ} (hM : 0 ≤ M) (_hB : 0 ≤ B) (hA : ∀ (k : List P), k.length ≤ l.length → UnitWord k → ‖(jet A k p) t‖ ≤ M) (hu : ∀ (k : List P), k.length ≤ l.length → UnitWord k → ‖(jet u k p) t‖ ≤ B) (hl : UnitWord l) : ‖(productJet A u l p) t‖ ≤ 2 ^ l.length * M * B

Every term in the full Leibniz expansion has the product estimate. There are 2^length ordered choices of which factor receives each derivative.

theorem NavierStokes.WeightedODEJets.norm_crossJet_le {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : P → ParametricODE.Coefficient a b E) (u : P → ParametricODE.Curve a b E) (l : List P) (p : P) (t : ↑(Set.Icc a b)) {M B : ℝ} (hM : 0 ≤ M) (hB : 0 ≤ B) (hA : ∀ (k : List P), k.length ≤ l.length → UnitWord k → ‖(jet A k p) t‖ ≤ M) (hu : ∀ (k : List P), k.length < l.length → UnitWord k → ‖(jet u k p) t‖ ≤ B) (hl : UnitWord l) : ‖(crossJet A u l p) t‖ ≤ 2 ^ l.length * M * B

The proper Leibniz expansion only requires solution jets of strictly lower order. This is the triangular property used by the weighted induction.

noncomputable def NavierStokes.WeightedODEJets.jetSource {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (A : P → ParametricODE.Coefficient a b E) (f u : P → ParametricODE.Curve a b E) (l : List P) (p : P) : ParametricODE.Curve a b E

The actual inhomogeneity of the differentiated equation.

Equations

• NavierStokes.WeightedODEJets.jetSource A f u l p = NavierStokes.WeightedODEJets.jet f l p + NavierStokes.WeightedODEJets.crossJet A u l p

theorem NavierStokes.WeightedODEJets.jet_solution_eq_solution {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (A : P → ParametricODE.Coefficient a b E) (x₀ : P → E) (f : P → ParametricODE.Curve a b E) (hA : ContDiffOn ℝ (↑⊤) A U) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f U) (l : List P) {p : P} (hp : p ∈ U) : jet (fun (q : P) => ParametricODE.solution hab (A q) (x₀ q) (f q)) l p = ParametricODE.solution hab (A p) (jet x₀ l p) (jetSource A f (fun (q : P) => ParametricODE.solution hab (A q) (x₀ q) (f q)) l p)

Every actual parameter jet of the constructed solution is itself the constructed solution of the corresponding triangular variational equation. No existence or smoothness of solution jets is assumed.

theorem NavierStokes.WeightedODEJets.jet_solution_hasDerivWithinAt {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (A : P → ParametricODE.Coefficient a b E) (x₀ : P → E) (f : P → ParametricODE.Curve a b E) (hA : ContDiffOn ℝ (↑⊤) A U) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f U) (l : List P) {p : P} (hp : p ∈ U) (t : ↑(Set.Icc a b)) : have u := fun (q : P) => ParametricODE.solution hab (A q) (x₀ q) (f q); HasDerivWithinAt (ParametricODE.extend hab (jet u l p)) (((A p) t) ((jet u l p) t) + (jetSource A f u l p) t) (Set.Icc a b) ↑t

The time derivative of each actual parameter jet is its triangular variational equation on the original closed interval.

theorem NavierStokes.WeightedODEJets.norm_solution_le_envelope {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (hab : a ≤ b) (A : ParametricODE.Coefficient a b H) (x₀ : H) (f : ParametricODE.Curve a b H) (rate W : ℝ → ℝ) {μ C X F₀ : ℝ} (hμ : 0 ≤ μ) (hW : ∀ (t : ℝ), 0 < W t) (hdW : ∀ (t : ℝ), HasDerivAt W (rate t * W t) t) (henergy : ∀ (t : ↑(Set.Icc a b)) (x : H), inner ℝ x ((A t) x) ≤ (rate ↑t + μ) * ‖x‖ ^ 2) (hC : Real.exp (μ * (b - a)) ≤ C) (hX : 0 ≤ X) (hF : 0 ≤ F₀) (hx₀ : ‖x₀‖ ≤ X * W a) (hf : ∀ (t : ↑(Set.Icc a b)), ‖f t‖ ≤ F₀ * W ↑t) (t : ↑(Set.Icc a b)) : ‖(ParametricODE.solution hab A x₀ f) t‖ ≤ C * (X + (b - a) * F₀) * W ↑t

The constructed solution retains a positive reference envelope. A uniform bound for the error exponential gives a factor linear in the slot length. The estimate follows from the proved energy inequality for the actual ODE.

theorem NavierStokes.WeightedODEJets.norm_jet_solution_le {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (A : P → ParametricODE.Coefficient a b H) (x₀ : P → H) (f : P → ParametricODE.Curve a b H) (hA : ContDiffOn ℝ (↑⊤) A U) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f U) {p : P} (hp : p ∈ U) (rate W : ℝ → ℝ) {μ C M X F₀ : ℝ} (hμ : 0 ≤ μ) (hW : ∀ (t : ℝ), 0 < W t) (hdW : ∀ (t : ℝ), HasDerivAt W (rate t * W t) t) (henergy : ∀ (t : ↑(Set.Icc a b)) (x : H), inner ℝ x (((A p) t) x) ≤ (rate ↑t + μ) * ‖x‖ ^ 2) (hC : Real.exp (μ * (b - a)) ≤ C) (hM : 0 ≤ M) (hX : 0 ≤ X) (hF : 0 ≤ F₀) (N : ℕ) (hAj : ∀ (l : List P), l.length ≤ N → UnitWord l → ∀ (t : ↑(Set.Icc a b)), ‖(jet A l p) t‖ ≤ M) (hxj : ∀ (l : List P), l.length ≤ N → UnitWord l → ‖jet x₀ l p‖ ≤ X * W a) (hfj : ∀ (l : List P), l.length ≤ N → UnitWord l → ∀ (t : ↑(Set.Icc a b)), ‖(jet f l p) t‖ ≤ F₀ * W ↑t) (l : List P) (hlN : l.length ≤ N) (hl : UnitWord l) (t : ↑(Set.Icc a b)) : ‖(jet (fun (q : P) => ParametricODE.solution hab (A q) (x₀ q) (f q)) l p) t‖ ≤ C * (X + (b - a) * F₀) * (1 + C * (b - a) * (2 ^ N * M)) ^ l.length * W ↑t

A finite-order weighted estimate for every actual mixed parameter jet. Only input jets are bounded in the hypotheses. The factor multiplying each successive derivative is polynomial in the slot length and coefficient bound.

theorem NavierStokes.WeightedODEJets.amplitude_le_polynomial {S K w L : ℝ} (hS : 1 ≤ S) (hK : 1 ≤ K) (hw : 0 ≤ w) (hL : 0 ≤ L) (hLS : L ≤ K * S) (m N n : ℕ) : K * (w * K * S ^ m + L * (w * K * S ^ m)) * (1 + K * L * (2 ^ N * (K * S ^ m))) ^ n ≤ w * (2 ^ (N + 1) * K ^ 3) ^ (n + 1) * S ^ ((m + 1) * (n + 1))

Explicit polynomial bookkeeping. The nonnegative factor w appears only once and is therefore preserved by every fixed differentiation order.

theorem NavierStokes.WeightedODEJets.exp_error_le_of_inv_scale {μ S L c d : ℝ} (hS : 0 < S) (hc : 0 ≤ c) (hμ : μ ≤ c / S) (hL : 0 ≤ L) (hslot : L ≤ d * S) : Real.exp (μ * L) ≤ Real.exp (c * d)

An error of order 1/S on a slot of length at most d*S has a uniform exponential factor, independent of S.

theorem NavierStokes.WeightedODEJets.norm_jet_solution_le_polynomial {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (A : P → ParametricODE.Coefficient a b H) (x₀ : P → H) (f : P → ParametricODE.Curve a b H) (hA : ContDiffOn ℝ (↑⊤) A U) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f U) {p : P} (hp : p ∈ U) (rate W : ℝ → ℝ) {μ S K w : ℝ} (hμ : 0 ≤ μ) (hW : ∀ (t : ℝ), 0 < W t) (hdW : ∀ (t : ℝ), HasDerivAt W (rate t * W t) t) (henergy : ∀ (t : ↑(Set.Icc a b)) (x : H), inner ℝ x (((A p) t) x) ≤ (rate ↑t + μ) * ‖x‖ ^ 2) (hC : Real.exp (μ * (b - a)) ≤ K) (hS : 1 ≤ S) (hK : 1 ≤ K) (hw : 0 ≤ w) (hslot : b - a ≤ K * S) (m N : ℕ) (hAj : ∀ (l : List P), l.length ≤ N → UnitWord l → ∀ (t : ↑(Set.Icc a b)), ‖(jet A l p) t‖ ≤ K * S ^ m) (hxj : ∀ (l : List P), l.length ≤ N → UnitWord l → ‖jet x₀ l p‖ ≤ w * K * S ^ m * W a) (hfj : ∀ (l : List P), l.length ≤ N → UnitWord l → ∀ (t : ↑(Set.Icc a b)), ‖(jet f l p) t‖ ≤ w * K * S ^ m * W ↑t) (l : List P) (hlN : l.length ≤ N) (hl : UnitWord l) (t : ↑(Set.Icc a b)) : ‖(jet (fun (q : P) => ParametricODE.solution hab (A q) (x₀ q) (f q)) l p) t‖ ≤ w * (2 ^ (N + 1) * K ^ 3) ^ (l.length + 1) * S ^ ((m + 1) * (l.length + 1)) * W ↑t

A concrete slot-polynomial estimate. w may be a small-scale power times a slow-variable weight; no loss of its power occurs in the induction.

theorem NavierStokes.WeightedODEJets.jet_pathFamily_apply {Q G : Type u} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (F : Q × ℝ → G) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ V)) {p : Q} (hp : p ∈ U) (l : List Q) (t : ↑(Set.Icc a b)) : (jet (SmoothPathFamily.pathFamily F) l p) t = jet (fun (q : Q) => F (q, ↑t)) l p

Actual directional path jets evaluate to the corresponding jets of the jointly supplied coefficient or source at each time.

theorem NavierStokes.WeightedODEJets.norm_jet_pathFamily_le {Q G : Type u} [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup G] [NormedSpace ℝ G] {a b : ℝ} (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (F : Q × ℝ → G) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ V)) {p : Q} (hp : p ∈ U) (l : List Q) (hl : UnitWord l) (t : ↑(Set.Icc a b)) : ‖(jet (SmoothPathFamily.pathFamily F) l p) t‖ ≤ ‖iteratedFDeriv ℝ l.length (fun (q : Q) => F (q, ↑t)) p‖

theorem NavierStokes.WeightedODEJets.norm_iteratedFDeriv_odeFamily_le_polynomial {Q : Type u} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {a b : ℝ} {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (hab : a ≤ b) (U : Set Q) (V : Set ℝ) (hU : IsOpen U) (hV : IsOpen V) (hI : Set.Icc a b ⊆ V) (A : Q × ℝ → H →L[ℝ] H) (x₀ : Q → H) (f : Q × ℝ → H) (hA : ContDiffOn ℝ (↑⊤) A (U ×ˢ V)) (hx₀ : ContDiffOn ℝ (↑⊤) x₀ U) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ V)) {p : Q} (hp : p ∈ U) (rate W : ℝ → ℝ) {μ S K w : ℝ} (hμ : 0 ≤ μ) (hW : ∀ (t : ℝ), 0 < W t) (hdW : ∀ (t : ℝ), HasDerivAt W (rate t * W t) t) (henergy : ∀ (t : ↑(Set.Icc a b)) (x : H), inner ℝ x ((A (p, ↑t)) x) ≤ (rate ↑t + μ) * ‖x‖ ^ 2) (hC : Real.exp (μ * (b - a)) ≤ K) (hS : 1 ≤ S) (hK : 1 ≤ K) (hw : 0 ≤ w) (hslot : b - a ≤ K * S) (m N : ℕ) (hAj : ∀ j ≤ N, ∀ (t : ↑(Set.Icc a b)), ‖iteratedFDeriv ℝ j (fun (q : Q) => A (q, ↑t)) p‖ ≤ K * S ^ m) (hxj : ∀ j ≤ N, ‖iteratedFDeriv ℝ j x₀ p‖ ≤ w * K * S ^ m * W a) (hfj : ∀ j ≤ N, ∀ (t : ↑(Set.Icc a b)), ‖iteratedFDeriv ℝ j (fun (q : Q) => f (q, ↑t)) p‖ ≤ w * K * S ^ m * W ↑t) (n : ℕ) (hn : n ≤ N) (t : ↑(Set.Icc a b)) : ‖iteratedFDeriv ℝ n (fun (q : Q) => (SmoothPathFamily.odeFamily hab A x₀ f q) t) p‖ ≤ w * (2 ^ (N + 1) * K ^ 3) ^ (n + 1) * S ^ ((m + 1) * (n + 1)) * W ↑t

Jointly smooth physical inputs with polynomial bounds on their actual Fréchet jets give polynomially bounded jets of the actual ODE solution. The bound is for the full multilinear norm at each time, retaining the envelope.