A constructed compactly supported Taylor–Borel extension

The input is an arbitrary sequence in a real Banach space. We choose increasing integer cutoff scales and sum actual cutoff monomials. All derivative bounds, convergence, smoothness, support, and prescribed derivatives at zero are proved.

noncomputable def NavierStokes.BorelExtension.monomial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) (s : ℝ) : E

Monomial, given by (s ^ j / (j.factorial : ℝ)) • v.

Equations

• NavierStokes.BorelExtension.monomial j v s = (s ^ j / ↑j.factorial) • v

theorem NavierStokes.BorelExtension.monomial_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) : ContDiff ℝ (↑⊤) (monomial j v)

theorem NavierStokes.BorelExtension.deriv_monomial_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) : deriv (monomial (j + 1) v) = monomial j v

theorem NavierStokes.BorelExtension.iteratedDeriv_monomial_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n j : ℕ) (v : E) : iteratedDeriv n (monomial j v) 0 = if n = j then v else 0

noncomputable def NavierStokes.BorelExtension.term {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : ℝ) (j : ℕ) (v : E) (s : ℝ) : E

The actual summand, with no smooth extension supplied as an input.

Equations

• NavierStokes.BorelExtension.term b j v s = NavierStokes.SmoothCutoffs.cutoff (b * s) • NavierStokes.BorelExtension.monomial j v s

noncomputable def NavierStokes.BorelExtension.template {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) (s : ℝ) : E

Template, given by SmoothCutoffs.cutoff s • monomial j v s.

Equations

• NavierStokes.BorelExtension.template j v s = NavierStokes.SmoothCutoffs.cutoff s • NavierStokes.BorelExtension.monomial j v s

theorem NavierStokes.BorelExtension.term_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : ℝ) (j : ℕ) (v : E) : ContDiff ℝ (↑⊤) (term b j v)

theorem NavierStokes.BorelExtension.template_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) : ContDiff ℝ (↑⊤) (template j v)

theorem NavierStokes.BorelExtension.template_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) : HasCompactSupport (template j v)

theorem NavierStokes.BorelExtension.template_iteratedDeriv_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j k : ℕ) (v : E) : HasCompactSupport (iteratedDeriv k (template j v))

theorem NavierStokes.BorelExtension.exists_template_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j k : ℕ) (v : E) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : ℝ), ‖iteratedDeriv k (template j v) s‖ ≤ C

noncomputable def NavierStokes.BorelExtension.templateBound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j k : ℕ) (v : E) : ℝ

Template bound, given by Classical.choose (exists_template_bound j k v).

Equations

• NavierStokes.BorelExtension.templateBound j k v = Classical.choose ⋯

theorem NavierStokes.BorelExtension.templateBound_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j k : ℕ) (v : E) : 0 ≤ templateBound j k v

theorem NavierStokes.BorelExtension.norm_template_iteratedDeriv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j k : ℕ) (v : E) (s : ℝ) : ‖iteratedDeriv k (template j v) s‖ ≤ templateBound j k v

theorem NavierStokes.BorelExtension.term_eq_scaled_template {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : ℝ} (hb : b ≠ 0) (j : ℕ) (v : E) : term b j v = fun (s : ℝ) => (b ^ j)⁻¹ • template j v (b * s)

theorem NavierStokes.BorelExtension.iteratedDeriv_term {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : ℝ} (hb : b ≠ 0) (j k : ℕ) (v : E) (s : ℝ) : iteratedDeriv k (term b j v) s = (b ^ k / b ^ j) • iteratedDeriv k (template j v) (b * s)

theorem NavierStokes.BorelExtension.iteratedDeriv_term_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (b : ℝ) (j k : ℕ) (v : E) : iteratedDeriv k (term b j v) 0 = if k = j then v else 0

theorem NavierStokes.BorelExtension.norm_iteratedDeriv_term_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : ℝ} (hb : 0 < b) (j k : ℕ) (v : E) (s : ℝ) : ‖iteratedDeriv k (term b j v) s‖ ≤ b ^ k / b ^ j * templateBound j k v

noncomputable def NavierStokes.BorelExtension.boundSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) : ℝ

A finite collection of bounds controls every derivative below the degree.

Equations

• NavierStokes.BorelExtension.boundSum j v = ∑ k ∈ Finset.range j, NavierStokes.BorelExtension.templateBound j k v

theorem NavierStokes.BorelExtension.boundSum_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) (v : E) : 0 ≤ boundSum j v

theorem NavierStokes.BorelExtension.templateBound_le_boundSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {j k : ℕ} (hkj : k < j) (v : E) : templateBound j k v ≤ boundSum j v

noncomputable def NavierStokes.BorelExtension.localScale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (j : ℕ) : ℕ

Local scale, given by Classical.choose (exists_nat_gt ((2 : ℝ) ^ j * boundSum j (a j))).

Equations

• NavierStokes.BorelExtension.localScale a j = Classical.choose ⋯

theorem NavierStokes.BorelExtension.localScale_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (j : ℕ) : 2 ^ j * boundSum j (a j) < ↑(localScale a j)

noncomputable def NavierStokes.BorelExtension.scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) : ℕ → ℕ

Increasing positive integer scales; they are selected from proved finite bounds.

Equations

• NavierStokes.BorelExtension.scale a = NavierStokes.DiagonalScale.doublingEnvelope (NavierStokes.BorelExtension.localScale a)

theorem NavierStokes.BorelExtension.scale_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (j : ℕ) : 0 < scale a j

theorem NavierStokes.BorelExtension.scale_strictMono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) : StrictMono (scale a)

theorem NavierStokes.BorelExtension.scale_doubling {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (j : ℕ) : 2 * scale a j ≤ scale a (j + 1)

theorem NavierStokes.BorelExtension.scale_ge_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (j : ℕ) : 1 ≤ ↑(scale a j)

theorem NavierStokes.BorelExtension.boundSum_le_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (j : ℕ) : boundSum j (a j) ≤ (1 / 2) ^ j * ↑(scale a j)

theorem NavierStokes.BorelExtension.term_derivative_tail_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) {j k : ℕ} (hkj : k < j) (s : ℝ) : ‖iteratedDeriv k (term (↑(scale a j)) j (a j)) s‖ ≤ (1 / 2) ^ j

The all-order diagonal estimate: for each fixed derivative order the tail is bounded uniformly on the whole real line by a geometric series.

noncomputable def NavierStokes.BorelExtension.majorant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (k j : ℕ) : ℝ

The finitely many early terms retain their actual derivative bounds.

Equations

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

theorem NavierStokes.BorelExtension.majorant_summable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (k : ℕ) : Summable (majorant a k)

theorem NavierStokes.BorelExtension.norm_iteratedDeriv_term_le_majorant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (k j : ℕ) (s : ℝ) : ‖iteratedDeriv k (term (↑(scale a j)) j (a j)) s‖ ≤ majorant a k j

noncomputable def NavierStokes.BorelExtension.extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (s : ℝ) : E

An actual series of compactly supported cutoff monomials.

Equations

• NavierStokes.BorelExtension.extension a s = ∑' (j : ℕ), NavierStokes.BorelExtension.term (↑(NavierStokes.BorelExtension.scale a j)) j (a j) s

theorem NavierStokes.BorelExtension.extension_eq_series {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) (s : ℝ) : extension a s = ∑' (j : ℕ), (SmoothCutoffs.cutoff (↑(scale a j) * s) * (s ^ j / ↑j.factorial)) • a j

theorem NavierStokes.BorelExtension.summable_iteratedDeriv_terms {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : ℕ → E) (k : ℕ) (s : ℝ) : Summable fun (j : ℕ) => iteratedDeriv k (term (↑(scale a j)) j (a j)) s

theorem NavierStokes.BorelExtension.extension_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : ℕ → E) : ContDiff ℝ (↑⊤) (extension a)

theorem NavierStokes.BorelExtension.iteratedDeriv_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : ℕ → E) (k : ℕ) (s : ℝ) : iteratedDeriv k (extension a) s = ∑' (j : ℕ), iteratedDeriv k (term (↑(scale a j)) j (a j)) s

theorem NavierStokes.BorelExtension.extension_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : ℕ → E) (k : ℕ) : iteratedDeriv k (extension a) 0 = a k

Every prescribed jet is attained, including the zeroth jet.

theorem NavierStokes.BorelExtension.extension_zero_of_one_le_abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) {s : ℝ} (hs : 1 ≤ |s|) : extension a s = 0

theorem NavierStokes.BorelExtension.extension_support {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) : Function.support (extension a) ⊆ Set.Ioo (-1) 1

theorem NavierStokes.BorelExtension.extension_tsupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) : tsupport (extension a) ⊆ Set.Icc (-1) 1

theorem NavierStokes.BorelExtension.extension_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : ℕ → E) : HasCompactSupport (extension a)

theorem NavierStokes.BorelExtension.extension_right_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : ℕ → E) (k : ℕ) : iteratedDerivWithin k (extension a) (Set.Ici 0) 0 = a k

The right endpoint jets used by the one-sided gluing theorem are the same prescribed jets as the ordinary derivatives.

noncomputable def NavierStokes.BorelExtension.rightExtension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (a : ℕ → E) (t : ℝ) : E

Translate the constructed extension to any joining time.

Equations

• NavierStokes.BorelExtension.rightExtension T a t = NavierStokes.BorelExtension.extension a (t - T)

theorem NavierStokes.BorelExtension.rightExtension_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (a : ℕ → E) : ContDiff ℝ (↑⊤) (rightExtension T a)

theorem NavierStokes.BorelExtension.rightExtension_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (a : ℕ → E) (k : ℕ) : iteratedDeriv k (rightExtension T a) T = a k

theorem NavierStokes.BorelExtension.rightExtension_right_jets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (a : ℕ → E) (k : ℕ) : iteratedDerivWithin k (rightExtension T a) (Set.Ici T) T = a k

theorem NavierStokes.BorelExtension.rightExtension_zero_from {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (a : ℕ → E) {t : ℝ} (ht : T + 1 ≤ t) : rightExtension T a t = 0

theorem NavierStokes.BorelExtension.exists_smooth_compact_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a : ℕ → E) : ∃ (f : ℝ → E), ContDiff ℝ (↑⊤) f ∧ tsupport f ⊆ Set.Icc (-1) 1 ∧ ∀ (k : ℕ), iteratedDeriv k f 0 = a k

Borel's jet realization theorem with a fixed compact support, constructed from the cutoff series rather than assumed as an extension principle.

theorem NavierStokes.BorelExtension.exists_smooth_right_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (a : ℕ → E) : ∃ (f : ℝ → E), ContDiffOn ℝ (↑⊤) f (Set.Ici T) ∧ (∀ (k : ℕ), iteratedDerivWithin k f (Set.Ici T) T = a k) ∧ ∀ (t : ℝ), T + 1 ≤ t → f t = 0

The interface for gluing to left endpoint limits at an arbitrary time.