Genuine derivative bounds for polynomially weighted Gaussian edges

The scalar derivative polynomials are the actual ones from FlatCutoff. Compactness bounds the derivatives of the smooth coefficient; the full Fréchet product rule then gives estimates for all joint derivative tensors.

theorem NavierStokes.EdgeWeightJets.nat_le_infty (n : ℕ) : ↑n ≤ ↑⊤

noncomputable def NavierStokes.EdgeWeightJets.coefficientMass (p : Polynomial ℝ) : ℝ

Coefficient mass, given by ∑ i ∈ Finset.range (p.natDegree + 1), |p.coeff i|.

Equations

• NavierStokes.EdgeWeightJets.coefficientMass p = ∑ i ∈ Finset.range (p.natDegree + 1), |p.coeff i|

theorem NavierStokes.EdgeWeightJets.coefficientMass_nonneg (p : Polynomial ℝ) : 0 ≤ coefficientMass p

theorem NavierStokes.EdgeWeightJets.polynomial_eval_bound (p : Polynomial ℝ) {x T : ℝ} (hT : 1 ≤ T) (hx : |x| ≤ T) : |Polynomial.eval x p| ≤ coefficientMass p * T ^ p.natDegree

noncomputable def NavierStokes.EdgeWeightJets.jetMass (c : ℝ) (p : Polynomial ℝ) (n : ℕ) : ℝ

Jet mass, given by 1 + ∑ i ∈ Finset.range (n + 1), coefficientMass (FlatCutoff.jetPolynomial c p i).

Equations

• NavierStokes.EdgeWeightJets.jetMass c p n = 1 + ∑ i ∈ Finset.range (n + 1), NavierStokes.EdgeWeightJets.coefficientMass (NavierStokes.FlatCutoff.jetPolynomial c p i)

noncomputable def NavierStokes.EdgeWeightJets.jetOrder (c : ℝ) (p : Polynomial ℝ) (n : ℕ) : ℕ

Jet order, given by ∑ i ∈ Finset.range (n + 1), (FlatCutoff.jetPolynomial c p i).natDegree.

Equations

• NavierStokes.EdgeWeightJets.jetOrder c p n = ∑ i ∈ Finset.range (n + 1), (NavierStokes.FlatCutoff.jetPolynomial c p i).natDegree

theorem NavierStokes.EdgeWeightJets.jetMass_pos (c : ℝ) (p : Polynomial ℝ) (n : ℕ) : 0 < jetMass c p n

theorem NavierStokes.EdgeWeightJets.jetMass_bound (c : ℝ) (p : Polynomial ℝ) {i n : ℕ} (hi : i ≤ n) : coefficientMass (FlatCutoff.jetPolynomial c p i) ≤ jetMass c p n

theorem NavierStokes.EdgeWeightJets.jetOrder_bound (c : ℝ) (p : Polynomial ℝ) {i n : ℕ} (hi : i ≤ n) : (FlatCutoff.jetPolynomial c p i).natDegree ≤ jetOrder c p n

theorem NavierStokes.EdgeWeightJets.polynomialEdge_jets_bound {c : ℝ} (hc : 0 < c) (p : Polynomial ℝ) (n : ℕ) {d : ℝ} (hd : 0 < d) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (FlatCutoff.polynomialEdge c p) x‖ ≤ C * FlatCutoff.edge c x / x ^ N

theorem NavierStokes.EdgeWeightJets.edge_div_pow_eq_polynomial (c : ℝ) (j : ℕ) : (fun (x : ℝ) => FlatCutoff.edge c x / x ^ j) = FlatCutoff.polynomialEdge c (Polynomial.X ^ j)

theorem NavierStokes.EdgeWeightJets.edge_div_pow_jets_bound {c : ℝ} (hc : 0 < c) (j n : ℕ) {d : ℝ} (hd : 0 < d) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (fun (x : ℝ) => FlatCutoff.edge c x / x ^ j) x‖ ≤ C * FlatCutoff.edge c x / x ^ N

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

theorem NavierStokes.EdgeWeightJets.compact_coefficient_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E × ℝ → F} (hB : ContDiff ℝ (↑⊤) B) {S : Set E} (hS : IsCompact S) (n : ℕ) (d : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ i ≤ n, ∀ p ∈ S, ∀ x ∈ Set.Icc 0 d, ‖iteratedFDeriv ℝ i B (p, x)‖ ≤ C

noncomputable def NavierStokes.EdgeWeightJets.weighted {E : Type u_1} (c : ℝ) (j : ℕ) (B : E × ℝ → ℝ) (y : E × ℝ) : ℝ

Weighted, given by (FlatCutoff.edge c y.2 / y.2 ^ j) * B y.

Equations

• NavierStokes.EdgeWeightJets.weighted c j B y = NavierStokes.FlatCutoff.edge c y.2 / y.2 ^ j * B y

theorem NavierStokes.EdgeWeightJets.weighted_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) : ContDiff ℝ (↑⊤) (weighted c j B)

theorem NavierStokes.EdgeWeightJets.edge_mul_iteratedFDeriv_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) {S : Set E} (hS : IsCompact S) (n : ℕ) {d : ℝ} (hd : 0 < d) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (weighted c j B) (p, x)‖ ≤ C * FlatCutoff.edge c x / x ^ N

A bound for every actual joint derivative tensor through a fixed order. Only smoothness of the coefficient and compactness of the parameter set are assumed; no weighted derivative estimates are inputs.

theorem NavierStokes.EdgeWeightJets.edge_mul_iteratedFDeriv_bound_unit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) {S : Set E} (hS : IsCompact S) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ p ∈ S, ∀ x ∈ Set.Ioo 0 1, ‖iteratedFDeriv ℝ n (fun (y : E × ℝ) => FlatCutoff.edge c y.2 / y.2 ^ j * B y) (p, x)‖ ≤ C * FlatCutoff.edge c x / x ^ N

theorem NavierStokes.EdgeWeightJets.weightedJets_of_isCompact_closure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) {U : Set E} (hU : IsCompact (closure U)) : WeightedQuotients.WeightedJets c U (fun (x : E × ℝ) => 1) (weighted c j B)

theorem NavierStokes.EdgeWeightJets.edge_div_pow_iteratedFDeriv_zero {c : ℝ} (hc : 0 < c) (j n : ℕ) : iteratedFDeriv ℝ n (fun (x : ℝ) => FlatCutoff.edge c x / x ^ j) 0 = 0

theorem NavierStokes.EdgeWeightJets.weighted_iteratedFDeriv_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) (n : ℕ) (p : E) : iteratedFDeriv ℝ n (weighted c j B) (p, 0) = 0

Every full derivative tensor vanishes on the joining hyperplane.

theorem NavierStokes.EdgeWeightJets.weighted_of_nonpos {E : Type u_1} (c : ℝ) (j : ℕ) (B : E × ℝ → ℝ) {y : E × ℝ} (hy : y.2 ≤ 0) : weighted c j B y = 0

theorem NavierStokes.EdgeWeightJets.norm_iteratedFDeriv_comp_linear_le {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : F → ℝ} (hf : ContDiff ℝ (↑⊤) f) (L : G →L[ℝ] F) (hL : ‖L‖ ≤ 1) (n : ℕ) (x : G) : ‖iteratedFDeriv ℝ n (f ∘ ⇑L) x‖ ≤ ‖iteratedFDeriv ℝ n f (L x)‖

theorem NavierStokes.EdgeWeightJets.norm_iteratedFDeriv_parameter_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (p : E) (x : ℝ) : ‖iteratedFDeriv ℝ n (fun (p : E) => f (p, x)) p‖ ≤ ‖iteratedFDeriv ℝ n f (p, x)‖

noncomputable def NavierStokes.EdgeWeightJets.radialIterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E × ℝ → ℝ) : ℕ → E × ℝ → ℝ

Radial iterate as an element of ℕ → E × ℝ → ℝ | 0 => f | n + 1 => fun y => fderiv ℝ (radialIterate f n) y (0, 1).

Equations

• NavierStokes.EdgeWeightJets.radialIterate f 0 = f
• NavierStokes.EdgeWeightJets.radialIterate f n.succ = fun (y : E × ℝ) => (fderiv ℝ (NavierStokes.EdgeWeightJets.radialIterate f n) y) (0, 1)

theorem NavierStokes.EdgeWeightJets.radialIterate_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (radialIterate f n)

theorem NavierStokes.EdgeWeightJets.deriv_slice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (p : E) (x : ℝ) : deriv (fun (t : ℝ) => f (p, t)) x = (fderiv ℝ f (p, x)) (0, 1)

theorem NavierStokes.EdgeWeightJets.radialIterate_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (p : E) (x : ℝ) : radialIterate f n (p, x) = iteratedDeriv n (fun (t : ℝ) => f (p, t)) x

theorem NavierStokes.EdgeWeightJets.norm_radialIterate_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n m : ℕ) (y : E × ℝ) : ‖iteratedFDeriv ℝ m (radialIterate f n) y‖ ≤ ‖iteratedFDeriv ℝ (m + n) f y‖

theorem NavierStokes.EdgeWeightJets.norm_mixed_derivatives_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (m n : ℕ) (p : E) (x : ℝ) : ‖iteratedFDeriv ℝ m (fun (q : E) => iteratedDeriv n (fun (t : ℝ) => f (q, t)) x) p‖ ≤ ‖iteratedFDeriv ℝ (m + n) f (p, x)‖

The left side contains the actual nested radial and parameter derivatives, and is controlled by the full joint tensor of total order.

theorem NavierStokes.EdgeWeightJets.edge_mul_mixed_derivatives_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) {S : Set E} (hS : IsCompact S) (k : ℕ) {d : ℝ} (hd : 0 < d) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ (m n : ℕ), m + n ≤ k → ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ m (fun (q : E) => iteratedDeriv n (fun (t : ℝ) => weighted c j B (q, t)) x) p‖ ≤ C * FlatCutoff.edge c x / x ^ N

theorem NavierStokes.EdgeWeightJets.compact_coefficient_jets_on {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E × ℝ → F} {V : Set (E × ℝ)} (hV : IsOpen V) (hB : ContDiffOn ℝ (↑⊤) B V) {S : Set E} (hS : IsCompact S) (n : ℕ) (d : ℝ) (hSV : S ×ˢ Set.Icc 0 d ⊆ V) : ∃ (C : ℝ), 0 < C ∧ ∀ i ≤ n, ∀ p ∈ S, ∀ x ∈ Set.Icc 0 d, ‖iteratedFDeriv ℝ i B (p, x)‖ ≤ C

theorem NavierStokes.EdgeWeightJets.edge_smul_iteratedFDeriv_bound_on {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → F} {V : Set (E × ℝ)} (hV : IsOpen V) (hB : ContDiffOn ℝ (↑⊤) B V) {S : Set E} (hS : IsCompact S) (n : ℕ) {d : ℝ} (hd : 0 < d) (hSV : S ×ˢ Set.Icc 0 d ⊆ V) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (fun (y : E × ℝ) => (FlatCutoff.edge c y.2 / y.2 ^ j) • B y) (p, x)‖ ≤ C * FlatCutoff.edge c x / x ^ N

The vector-valued local version needs only genuine smoothness on an open neighborhood of the compact parameter-coordinate region.

theorem NavierStokes.EdgeWeightJets.edge_smul_iteratedFDeriv_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → F} (hB : ContDiff ℝ (↑⊤) B) {S : Set E} (hS : IsCompact S) (n : ℕ) {d : ℝ} (hd : 0 < d) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (fun (y : E × ℝ) => (FlatCutoff.edge c y.2 / y.2 ^ j) • B y) (p, x)‖ ≤ C * FlatCutoff.edge c x / x ^ N

theorem NavierStokes.EdgeWeightJets.edge_mul_iteratedFDeriv_bound_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} {V : Set (E × ℝ)} (hV : IsOpen V) (hB : ContDiffOn ℝ (↑⊤) B V) {S : Set E} (hS : IsCompact S) (n : ℕ) {d : ℝ} (hd : 0 < d) (hSV : S ×ˢ Set.Icc 0 d ⊆ V) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (weighted c j B) (p, x)‖ ≤ C * FlatCutoff.edge c x / x ^ N

theorem NavierStokes.EdgeWeightJets.edge_mul_edge (c d x : ℝ) : FlatCutoff.edge c x * FlatCutoff.edge d x = FlatCutoff.edge (c + d) x

theorem NavierStokes.EdgeWeightJets.weighted_mul {E : Type u_1} (c d : ℝ) (j k : ℕ) (B D : E × ℝ → ℝ) : (fun (y : E × ℝ) => weighted c j B y * weighted d k D y) = weighted (c + d) (j + k) fun (y : E × ℝ) => B y * D y

theorem NavierStokes.EdgeWeightJets.weighted_mul_iteratedFDeriv_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c d : ℝ} (hc : 0 < c) (hd : 0 < d) (j k : ℕ) {B D : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) (hD : ContDiff ℝ (↑⊤) D) {S : Set E} (hS : IsCompact S) (n : ℕ) {a : ℝ} (ha : 0 < a) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ a → ‖iteratedFDeriv ℝ i (fun (y : E × ℝ) => weighted c j B y * weighted d k D y) (p, x)‖ ≤ C * FlatCutoff.edge (c + d) x / x ^ N

theorem NavierStokes.EdgeWeightJets.radial_power_iteratedFDeriv_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j k : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) {S : Set E} (hS : IsCompact S) (n : ℕ) {d : ℝ} (hd : 0 < d) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (fun (y : E × ℝ) => FlatCutoff.edge c y.2 / y.2 ^ j * (y.2 ^ k * B y)) (p, x)‖ ≤ C * FlatCutoff.edge c x / x ^ N

Any fixed nonnegative power of the radial coordinate can be retained inside the actual smooth coefficient. Inverse powers are already arbitrary.

theorem NavierStokes.EdgeWeightJets.edge_pow (c x : ℝ) {k : ℕ} (hk : 0 < k) : FlatCutoff.edge c x ^ k = FlatCutoff.edge (↑k * c) x

theorem NavierStokes.EdgeWeightJets.weighted_pow {E : Type u_1} (c : ℝ) (j : ℕ) (B : E × ℝ → ℝ) {k : ℕ} (hk : 0 < k) : (fun (y : E × ℝ) => weighted c j B y ^ k) = weighted (↑k * c) (j * k) fun (y : E × ℝ) => B y ^ k

theorem NavierStokes.EdgeWeightJets.weighted_pow_iteratedFDeriv_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 0 < c) (j : ℕ) {B : E × ℝ → ℝ} (hB : ContDiff ℝ (↑⊤) B) {S : Set E} (hS : IsCompact S) {k : ℕ} (hk : 0 < k) (n : ℕ) {d : ℝ} (hd : 0 < d) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ d → ‖iteratedFDeriv ℝ i (fun (y : E × ℝ) => weighted c j B y ^ k) (p, x)‖ ≤ C * FlatCutoff.edge (↑k * c) x / x ^ N