Joint parameter derivatives of the normalized flat kernel

The estimates use actual total Fréchet derivatives and finite profile-jet bounds. The parameter space need not be finite-dimensional for these bounds.

theorem NavierStokes.ParametricKernelBounds.finite_polynomial_majorant {X : Type u_1} [NormedAddCommGroup X] (f : ℕ → X → ℝ → ℝ) (R : ℝ) (n : ℕ) : (∀ k ≤ n, ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (y : X) (t : ℝ), ‖y‖ ≤ R → 0 ≤ t → f k y t ≤ C * (1 + t) ^ N) → ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ k ≤ n, ∀ (y : X) (t : ℝ), ‖y‖ ≤ R → 0 ≤ t → f k y t ≤ C * (1 + t) ^ N

Combine finitely many polynomial bounds, allowing distinct initial constants and degrees.

theorem NavierStokes.ParametricKernelBounds.norm_iteratedFDeriv_pair_le {X : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : X → F} {g : X → G} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (x : X) : ‖iteratedFDeriv ℝ n (fun (y : X) => (f y, g y)) x‖ ≤ ‖iteratedFDeriv ℝ n f x‖ + ‖iteratedFDeriv ℝ n g x‖

theorem NavierStokes.ParametricKernelBounds.norm_iteratedFDeriv_linear_le {X : Type u_1} {F : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : X →L[ℝ] F) (n : ℕ) (hn : 1 ≤ n) (x : X) : ‖iteratedFDeriv ℝ n (⇑L) x‖ ≤ ‖L‖

theorem NavierStokes.ParametricKernelBounds.norm_iteratedFDeriv_mul_le_of_bounds {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {f g : X → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (x : X) {C D : ℝ} (hC : 0 ≤ C) (_hD : 0 ≤ D) (hfb : ∀ i ≤ n, ‖iteratedFDeriv ℝ i f x‖ ≤ C) (hgb : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g x‖ ≤ D) : ‖iteratedFDeriv ℝ n (fun (y : X) => f y * g y) x‖ ≤ (∑ i ∈ Finset.range (n + 1), ↑(n.choose i)) * C * D

theorem NavierStokes.ParametricKernelBounds.norm_iteratedFDeriv_scalar_snd_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (y : E × ℝ) : ‖iteratedFDeriv ℝ n (fun (z : E × ℝ) => f z.2) y‖ ≤ |iteratedDeriv n f y.2|

def NavierStokes.ParametricKernelBounds.coordinateExpr : FlatKernelBounds.Expr

Coordinate expr, given by .mul .x .invRoot.

Equations

• NavierStokes.ParametricKernelBounds.coordinateExpr = NavierStokes.FlatKernelBounds.Expr.x.mul NavierStokes.FlatKernelBounds.Expr.invRoot

theorem NavierStokes.ParametricKernelBounds.coordinate_eq_expr (x t : ℝ) : FlatKernelBounds.coordinate x t = coordinateExpr.eval (fun (x : ℝ) => 0) x t

theorem NavierStokes.ParametricKernelBounds.coordinate_contDiff {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : ℝ) => FlatKernelBounds.coordinate x t

theorem NavierStokes.ParametricKernelBounds.coordinate_derivative_bound (n : ℕ) {R : ℝ} (hR : 0 ≤ R) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (x t : ℝ), |x| ≤ R → 0 ≤ t → |iteratedDeriv n (fun (y : ℝ) => FlatKernelBounds.coordinate y t) x| ≤ C * (1 + t) ^ N

noncomputable def NavierStokes.ParametricKernelBounds.transform {E : Type u_1} (t : ℝ) (y : E × ℝ) : E × ℝ

Transform, given by (y.1, coordinate y.2 t).

Equations

• NavierStokes.ParametricKernelBounds.transform t y = (y.1, NavierStokes.FlatKernelBounds.coordinate y.2 t)

theorem NavierStokes.ParametricKernelBounds.transform_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (transform t)

theorem NavierStokes.ParametricKernelBounds.norm_transform_le {E : Type u_1} [NormedAddCommGroup E] {t : ℝ} (ht : 0 ≤ t) (y : E × ℝ) : ‖transform t y‖ ≤ ‖y‖

theorem NavierStokes.ParametricKernelBounds.norm_iteratedFDeriv_transform_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (hn : 1 ≤ n) {t : ℝ} (ht : 0 ≤ t) (y : E × ℝ) : ‖iteratedFDeriv ℝ n (transform t) y‖ ≤ 1 + |iteratedDeriv n (fun (x : ℝ) => FlatKernelBounds.coordinate x t) y.2|

theorem NavierStokes.ParametricKernelBounds.transform_derivative_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) {R : ℝ} (hR : 0 ≤ R) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (y : E × ℝ) (t : ℝ), ‖y‖ ≤ R → 0 ≤ t → ‖iteratedFDeriv ℝ n (transform t) y‖ ≤ C * (1 + t) ^ N

noncomputable def NavierStokes.ParametricKernelBounds.amplitude (j : ℕ) (x t : ℝ) : ℝ

Amplitude, given by denominator x t ^ j / denominator x t ^ 3.

Equations

• NavierStokes.ParametricKernelBounds.amplitude j x t = NavierStokes.FlatKernelBounds.denominator x t ^ j / NavierStokes.FlatKernelBounds.denominator x t ^ 3

theorem NavierStokes.ParametricKernelBounds.amplitude_contDiff (j : ℕ) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : ℝ) => amplitude j x t

theorem NavierStokes.ParametricKernelBounds.amplitude_derivative_bound (j n : ℕ) {R : ℝ} (hR : 0 ≤ R) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (x t : ℝ), |x| ≤ R → 0 ≤ t → |iteratedDeriv n (fun (y : ℝ) => amplitude j y t) x| ≤ C * (1 + t) ^ N

theorem NavierStokes.ParametricKernelBounds.amplitude_joint_derivative_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j n : ℕ) {R : ℝ} (hR : 0 ≤ R) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (y : E × ℝ) (t : ℝ), ‖y‖ ≤ R → 0 ≤ t → ‖iteratedFDeriv ℝ n (fun (z : E × ℝ) => amplitude j z.2 t) y‖ ≤ C * (1 + t) ^ N

noncomputable def NavierStokes.ParametricKernelBounds.rawKernel {E : Type u_1} (j : ℕ) (b : E × ℝ → ℝ) (y : E × ℝ) (t : ℝ) : ℝ

Raw kernel, given by amplitude j y.2 t * b (transform t y).

Equations

• NavierStokes.ParametricKernelBounds.rawKernel j b y t = NavierStokes.ParametricKernelBounds.amplitude j y.2 t * b (NavierStokes.ParametricKernelBounds.transform t y)

noncomputable def NavierStokes.ParametricKernelBounds.kernel {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (y : E × ℝ) (t : ℝ) : ℝ

Kernel, given by (1 / 2 : ℝ) * Real.exp (-c * t) * (denominator y.2 t ^ j / denominator y.2 t ^ 3) * b (y.1, coordinate y.2 t).

Equations

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

theorem NavierStokes.ParametricKernelBounds.rawKernel_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (y : E × ℝ) => rawKernel j b y t

theorem NavierStokes.ParametricKernelBounds.profile_comp_derivative_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (n : ℕ) {R : ℝ} (hR : 0 ≤ R) {B : ℝ} (hB : 0 ≤ B) (hjets : ∀ k ≤ n, ∀ (z : E × ℝ), ‖z‖ ≤ R → ‖iteratedFDeriv ℝ k b z‖ ≤ B) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (y : E × ℝ) (t : ℝ), ‖y‖ ≤ R → 0 ≤ t → ‖iteratedFDeriv ℝ n (b ∘ transform t) y‖ ≤ C * (1 + t) ^ N

The profile composed with the coordinate transform has polynomially bounded total derivatives, using only profile jets through the requested order.

theorem NavierStokes.ParametricKernelBounds.rawKernel_iteratedFDeriv_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (j n : ℕ) {R : ℝ} (hR : 0 ≤ R) {B : ℝ} (hB : 0 ≤ B) (hjets : ∀ k ≤ n, ∀ (z : E × ℝ), ‖z‖ ≤ R → ‖iteratedFDeriv ℝ k b z‖ ≤ B) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (y : E × ℝ) (t : ℝ), ‖y‖ ≤ R → 0 ≤ t → ‖iteratedFDeriv ℝ n (fun (z : E × ℝ) => rawKernel j b z t) y‖ ≤ C * (1 + t) ^ N

theorem NavierStokes.ParametricKernelBounds.kernel_eq_raw {E : Type u_1} (c : ℝ) (j : ℕ) (b : E × ℝ → ℝ) (y : E × ℝ) (t : ℝ) : kernel c j b y t = 1 / 2 * Real.exp (-c * t) * rawKernel j b y t

theorem NavierStokes.ParametricKernelBounds.kernel_iteratedFDeriv_bound_of_jetBounds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : E × ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (c : ℝ) (j n : ℕ) {R : ℝ} (hR : 0 ≤ R) {B : ℝ} (hB : 0 ≤ B) (hjets : ∀ k ≤ n, ∀ (z : E × ℝ), ‖z‖ ≤ R → ‖iteratedFDeriv ℝ k b z‖ ≤ B) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (y : E × ℝ) (t : ℝ), ‖y‖ ≤ R → 0 ≤ t → ‖iteratedFDeriv ℝ n (fun (z : E × ℝ) => kernel c j b z t) y‖ ≤ C * (1 + t) ^ N * Real.exp (-c * t)

Total parameter derivatives of the concrete kernel have an exponential times polynomial majorant. No bound for kernel derivatives is assumed.