Bounds for actual Fréchet jets

Finite jet bounds on open domains, using iteratedFDeriv itself. The product estimates follow from Mathlib's higher-order Leibniz inequality. No PDE, construction, or prescribed derivative values are assumed here.

def NavierStokes.JetBounds.FiniteJetBound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (m : ℕ) (f : D → E) (s : Set D) (C : ℝ) : Prop

A common bound for the actual derivatives of orders 0, ..., m on s. Smoothness is a separate hypothesis of the closure theorems.

Equations

• NavierStokes.JetBounds.FiniteJetBound m f s C = ∀ n ≤ m, ∀ x ∈ s, ‖iteratedFDeriv ℝ n f x‖ ≤ C

def NavierStokes.JetBounds.AllJetBound {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : D → E) (s : Set D) (C : ℕ → ℝ) : Prop

An order-dependent bound for all actual derivatives on s.

Equations

• NavierStokes.JetBounds.AllJetBound f s C = ∀ (n : ℕ), ∀ x ∈ s, ‖iteratedFDeriv ℝ n f x‖ ≤ C n

theorem NavierStokes.JetBounds.FiniteJetBound.mono {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : D → E} {s : Set D} {A B : ℝ} (hf : FiniteJetBound m f s A) (hAB : A ≤ B) : FiniteJetBound m f s B

theorem NavierStokes.JetBounds.FiniteJetBound.of_le {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m n : ℕ} {f : D → E} {s : Set D} {C : ℝ} (hf : FiniteJetBound m f s C) (hn : n ≤ m) : FiniteJetBound n f s C

theorem NavierStokes.JetBounds.FiniteJetBound.nonneg {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : D → E} {s : Set D} {C : ℝ} (hf : FiniteJetBound m f s C) {x : D} (hx : x ∈ s) : 0 ≤ C

theorem NavierStokes.JetBounds.FiniteJetBound.norm_le {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : D → E} {s : Set D} {C : ℝ} (hf : FiniteJetBound m f s C) {x : D} (hx : x ∈ s) : ‖f x‖ ≤ C

theorem NavierStokes.JetBounds.FiniteJetBound.fderiv {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : D → E} {s : Set D} {C : ℝ} (hf : FiniteJetBound (m + 1) f s C) : FiniteJetBound m (_root_.fderiv ℝ f) s C

Taking a genuine Fréchet derivative consumes one derivative of the bound.

theorem NavierStokes.JetBounds.AllJetBound.fderiv {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} {s : Set D} {C : ℕ → ℝ} (hf : AllJetBound f s C) : AllJetBound (_root_.fderiv ℝ f) s fun (n : ℕ) => C (n + 1)

theorem NavierStokes.JetBounds.FiniteJetBound.add {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f g : D → E} {s : Set D} {A B : ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑m) f s) (hg : ContDiffOn ℝ (↑m) g s) (hA : FiniteJetBound m f s A) (hB : FiniteJetBound m g s B) : FiniteJetBound m (fun (x : D) => f x + g x) s (A + B)

Addition in a finite C^m bound, on an arbitrary open domain.

theorem NavierStokes.JetBounds.norm_iteratedFDeriv_bilinear_le_on {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) {f : D → E} {g : D → F} {s : Set D} {N : WithTop ℕ∞} (hs : IsOpen s) (hf : ContDiffOn ℝ N f s) (hg : ContDiffOn ℝ N g s) {x : D} (hx : x ∈ s) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDeriv ℝ n (fun (y : D) => (B (f y)) (g y)) x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖

Mathlib's Leibniz inequality stated with ambient derivatives on an open set.

theorem NavierStokes.JetBounds.norm_iteratedFDeriv_mul_le_on {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {f g : D → ℝ} {s : Set D} {N : WithTop ℕ∞} (hs : IsOpen s) (hf : ContDiffOn ℝ N f s) (hg : ContDiffOn ℝ N g s) {x : D} (hx : x ∈ s) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDeriv ℝ n (fun (y : D) => f y * g y) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖

The scalar Leibniz inequality on an open set, with ambient derivatives.

theorem NavierStokes.JetBounds.FiniteJetBound.bilinear {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {m : ℕ} (B : E →L[ℝ] F →L[ℝ] G) {f : D → E} {g : D → F} {s : Set D} {A C : ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑m) f s) (hg : ContDiffOn ℝ (↑m) g s) (hA : FiniteJetBound m f s A) (hC : FiniteJetBound m g s C) : FiniteJetBound m (fun (x : D) => (B (f x)) (g x)) s (‖B‖ * 2 ^ m * A * C)

A bounded bilinear map obeys the explicit finite-order Leibniz bound.

theorem NavierStokes.JetBounds.FiniteJetBound.mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {m : ℕ} {f g : D → ℝ} {s : Set D} {A B : ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑m) f s) (hg : ContDiffOn ℝ (↑m) g s) (hA : FiniteJetBound m f s A) (hB : FiniteJetBound m g s B) : FiniteJetBound m (fun (x : D) => f x * g x) s (2 ^ m * A * B)

Scalar multiplication has bilinear norm at most one, giving constant 2^m.

theorem NavierStokes.JetBounds.FiniteJetBound.clm_apply {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : ℕ} {f : D → E →L[ℝ] F} {g : D → E} {s : Set D} {A B : ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑m) f s) (hg : ContDiffOn ℝ (↑m) g s) (hA : FiniteJetBound m f s A) (hB : FiniteJetBound m g s B) : FiniteJetBound m (fun (x : D) => (f x) (g x)) s (2 ^ m * A * B)

Evaluation of an operator-valued field has the same 2^m product bound.

theorem NavierStokes.JetBounds.FiniteJetBound.transport {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : D → D} {g : D → E} {s : Set D} {A B : ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑m) f s) (hg : ContDiffOn ℝ (↑m + 1) g s) (hA : FiniteJetBound m f s A) (hB : FiniteJetBound (m + 1) g s B) : FiniteJetBound m (fun (x : D) => (_root_.fderiv ℝ g x) (f x)) s (2 ^ m * B * A)

The transport expression (Dg) f uses one extra derivative of g.

theorem NavierStokes.JetBounds.FiniteJetBound.secondFDeriv {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} {f : D → E} {s : Set D} {C : ℝ} (hf : FiniteJetBound (m + 2) f s C) : FiniteJetBound m (_root_.fderiv ℝ (_root_.fderiv ℝ f)) s C

The actual second Fréchet derivative consumes two orders of a finite bound.

def NavierStokes.JetBounds.leibnizProfile (A B : ℕ → ℝ) (n : ℕ) : ℝ

The order profile produced by the binomial Leibniz sum.

Equations

• NavierStokes.JetBounds.leibnizProfile A B n = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * A i * B (n - i)

theorem NavierStokes.JetBounds.AllJetBound.add {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : D → E} {s : Set D} {A B : ℕ → ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g s) (hA : AllJetBound f s A) (hB : AllJetBound g s B) : AllJetBound (fun (x : D) => f x + g x) s fun (n : ℕ) => A n + B n

theorem NavierStokes.JetBounds.AllJetBound.bilinear {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : E →L[ℝ] F →L[ℝ] G) {f : D → E} {g : D → F} {s : Set D} {A B : ℕ → ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g s) (hA : AllJetBound f s A) (hB : AllJetBound g s B) : AllJetBound (fun (x : D) => (L (f x)) (g x)) s fun (n : ℕ) => ‖L‖ * leibnizProfile A B n

All-order bilinear closure with the full binomial profile, rather than a constant uniform in derivative order.

theorem NavierStokes.JetBounds.AllJetBound.mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {f g : D → ℝ} {s : Set D} {A B : ℕ → ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g s) (hA : AllJetBound f s A) (hB : AllJetBound g s B) : AllJetBound (fun (x : D) => f x * g x) s (leibnizProfile A B)

theorem NavierStokes.JetBounds.leibnizProfile_scale (A B : ℕ → ℝ) (a b : ℝ) (n : ℕ) : leibnizProfile (fun (i : ℕ) => A i * a) (fun (i : ℕ) => B i * b) n = leibnizProfile A B n * (a * b)

theorem NavierStokes.JetBounds.FiniteJetBound.mul_rpow {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {m : ℕ} {f g : D → ℝ} {s : Set D} {A B ε α β : ℝ} (hε : 0 < ε) (hs : IsOpen s) (hf : ContDiffOn ℝ (↑m) f s) (hg : ContDiffOn ℝ (↑m) g s) (hA : FiniteJetBound m f s (A * ε ^ α)) (hB : FiniteJetBound m g s (B * ε ^ β)) : FiniteJetBound m (fun (x : D) => f x * g x) s (2 ^ m * A * B * ε ^ (α + β))

Exact exponent addition in the finite product bound.

theorem NavierStokes.JetBounds.AllJetBound.mul_rpow {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {f g : D → ℝ} {s : Set D} {A B : ℕ → ℝ} {ε α β : ℝ} (hε : 0 < ε) (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g s) (hA : AllJetBound f s fun (n : ℕ) => A n * ε ^ α) (hB : AllJetBound g s fun (n : ℕ) => B n * ε ^ β) : AllJetBound (fun (x : D) => f x * g x) s fun (n : ℕ) => leibnizProfile A B n * ε ^ (α + β)

The all-order product estimate preserves the sum of real decay exponents; the output constants are explicitly the binomial convolution of input constants.

theorem NavierStokes.JetBounds.FiniteJetBound.bilinear_perturbation {D : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {m : ℕ} (L : E →L[ℝ] F →L[ℝ] G) {f u : D → E} {g v : D → F} {s : Set D} {A U B V : ℝ} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑m) f s) (hu : ContDiffOn ℝ (↑m) u s) (hg : ContDiffOn ℝ (↑m) g s) (hv : ContDiffOn ℝ (↑m) v s) (hA : FiniteJetBound m f s A) (hU : FiniteJetBound m u s U) (hB : FiniteJetBound m g s B) (hV : FiniteJetBound m v s V) : FiniteJetBound m (fun (x : D) => (L (f x + u x)) (g x + v x) - (L (f x)) (g x)) s (‖L‖ * 2 ^ m * (A * V + U * B + U * V))

Quantitative change of a general bounded bilinear nonlinearity. The three terms are the two cross interactions and the quadratic perturbation.