Jointly smooth Taylor–Borel extension of spatially smooth jets

There is one cutoff scale per Taylor degree. Its finite list of constraints includes all joint derivatives and all spatial localizations up to that degree. This gives joint smoothness without imposing global bounds on the input jets.

def NavierStokes.SpatialBorelExtension.spatialBump {X : Type u_1} [NormedAddCommGroup X] (m : ℕ) : ContDiffBump 0

Spatial bump, bundling rIn, rOut, rIn_pos, rIn_lt_rOut.

Equations

• NavierStokes.SpatialBorelExtension.spatialBump m = { rIn := ↑m + 1, rOut := ↑m + 2, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def NavierStokes.SpatialBorelExtension.spatialCutoff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] (m : ℕ) : X → ℝ

Spatial cutoff, given by (spatialBump (X := X) m : X → ℝ).

Equations

• NavierStokes.SpatialBorelExtension.spatialCutoff m = ↑(NavierStokes.SpatialBorelExtension.spatialBump m)

theorem NavierStokes.SpatialBorelExtension.spatialCutoff_contDiff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] (m : ℕ) : ContDiff ℝ (↑⊤) (spatialCutoff m)

theorem NavierStokes.SpatialBorelExtension.spatialCutoff_eventually_one {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] (m : ℕ) {x : X} (hx : ‖x‖ < ↑m + 1) : spatialCutoff m =ᶠ[nhds x] fun (x : X) => 1

theorem NavierStokes.SpatialBorelExtension.spatialCutoff_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] (m : ℕ) {x : X} (hx : ↑m + 2 ≤ ‖x‖) : spatialCutoff m x = 0

theorem NavierStokes.SpatialBorelExtension.exists_spatial_plateau {X : Type u_1} [NormedAddCommGroup X] (x : X) : ∃ (m : ℕ), ‖x‖ < ↑m + 1

theorem NavierStokes.SpatialBorelExtension.exists_compact_spatial_plateau {X : Type u_1} [NormedAddCommGroup X] {K : Set X} (hK : IsCompact K) : ∃ (m : ℕ), ∀ x ∈ K, ‖x‖ < ↑m + 1

noncomputable def NavierStokes.SpatialBorelExtension.term {X : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (j : ℕ) (a : X → V) (z : ℝ × X) : V

Term, given by BorelExtension.term b j (a z.2) z.1.

Equations

• NavierStokes.SpatialBorelExtension.term b j a z = NavierStokes.BorelExtension.term b j (a z.2) z.1

noncomputable def NavierStokes.SpatialBorelExtension.localizedTerm {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (m : ℕ) (b : ℝ) (j : ℕ) (a : X → V) (z : ℝ × X) : V

Localized term, given by spatialCutoff m z.2 • term b j a z.

Equations

• NavierStokes.SpatialBorelExtension.localizedTerm m b j a z = NavierStokes.SpatialBorelExtension.spatialCutoff m z.2 • NavierStokes.SpatialBorelExtension.term b j a z

noncomputable def NavierStokes.SpatialBorelExtension.template {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (m j : ℕ) (a : X → V) : ℝ × X → V

Template, given by localizedTerm m 1 j a.

Equations

• NavierStokes.SpatialBorelExtension.template m j a = NavierStokes.SpatialBorelExtension.localizedTerm m 1 j a

theorem NavierStokes.SpatialBorelExtension.term_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) (b : ℝ) (j : ℕ) : ContDiff ℝ (↑⊤) (term b j a)

theorem NavierStokes.SpatialBorelExtension.localizedTerm_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) (m : ℕ) (b : ℝ) (j : ℕ) : ContDiff ℝ (↑⊤) (localizedTerm m b j a)

theorem NavierStokes.SpatialBorelExtension.template_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) (m j : ℕ) : ContDiff ℝ (↑⊤) (template m j a)

theorem NavierStokes.SpatialBorelExtension.template_hasCompactSupport {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (m j : ℕ) (a : X → V) : HasCompactSupport (template m j a)

def NavierStokes.SpatialBorelExtension.timeScale {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (b : ℝ) : ℝ × X →L[ℝ] ℝ × X

Time scale, given by (b • ContinuousLinearMap.fst ℝ ℝ X).prod (ContinuousLinearMap.snd ℝ ℝ X).

Equations

• NavierStokes.SpatialBorelExtension.timeScale b = (b • ContinuousLinearMap.fst ℝ ℝ X).prod (ContinuousLinearMap.snd ℝ ℝ X)

@[simp]

theorem NavierStokes.SpatialBorelExtension.timeScale_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (b : ℝ) (z : ℝ × X) : (timeScale b) z = (b * z.1, z.2)

theorem NavierStokes.SpatialBorelExtension.norm_timeScale_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {b : ℝ} (hb : 1 ≤ b) : ‖timeScale b‖ ≤ b

theorem NavierStokes.SpatialBorelExtension.localizedTerm_eq_scaled {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {b : ℝ} (hb : b ≠ 0) (m j : ℕ) (a : X → V) : localizedTerm m b j a = (b ^ j)⁻¹ • template m j a ∘ ⇑(timeScale b)

theorem NavierStokes.SpatialBorelExtension.exists_template_bound {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) (m j k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : ℝ × X), ‖iteratedFDeriv ℝ k (template m j a) z‖ ≤ C

noncomputable def NavierStokes.SpatialBorelExtension.templateBound {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) (m j k : ℕ) : ℝ

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

Equations

• NavierStokes.SpatialBorelExtension.templateBound ha m j k = Classical.choose ⋯

theorem NavierStokes.SpatialBorelExtension.templateBound_nonneg {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) (m j k : ℕ) : 0 ≤ templateBound ha m j k

theorem NavierStokes.SpatialBorelExtension.template_deriv_le {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) (m j k : ℕ) (z : ℝ × X) : ‖iteratedFDeriv ℝ k (template m j a) z‖ ≤ templateBound ha m j k

theorem NavierStokes.SpatialBorelExtension.localizedTerm_deriv_bound {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : X → V} (ha : ContDiff ℝ (↑⊤) a) {b : ℝ} (hb : 1 ≤ b) (m j k : ℕ) (z : ℝ × X) : ‖iteratedFDeriv ℝ k (localizedTerm m b j a) z‖ ≤ b ^ k / b ^ j * templateBound ha m j k

noncomputable def NavierStokes.SpatialBorelExtension.boundSum {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : ℝ

Each degree controls finitely many spatial windows and derivative orders.

Equations

• NavierStokes.SpatialBorelExtension.boundSum a ha j = ∑ m ∈ Finset.range j, ∑ k ∈ Finset.range j, NavierStokes.SpatialBorelExtension.templateBound ⋯ m j k

theorem NavierStokes.SpatialBorelExtension.boundSum_nonneg {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : 0 ≤ boundSum a ha j

theorem NavierStokes.SpatialBorelExtension.templateBound_le_boundSum {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) {m j k : ℕ} (hm : m < j) (hk : k < j) : templateBound ⋯ m j k ≤ boundSum a ha j

noncomputable def NavierStokes.SpatialBorelExtension.localScale {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : ℕ

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

Equations

• NavierStokes.SpatialBorelExtension.localScale a ha j = Classical.choose ⋯

theorem NavierStokes.SpatialBorelExtension.localScale_bound {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : 2 ^ j * boundSum a ha j < ↑(localScale a ha j)

noncomputable def NavierStokes.SpatialBorelExtension.scale {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) : ℕ → ℕ

The scale depends on the degree and the whole input family, never on the evaluation point or on the derivative order subsequently requested.

Equations

• NavierStokes.SpatialBorelExtension.scale a ha = NavierStokes.DiagonalScale.doublingEnvelope (NavierStokes.SpatialBorelExtension.localScale a ha)

theorem NavierStokes.SpatialBorelExtension.scale_pos {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : 0 < scale a ha j

theorem NavierStokes.SpatialBorelExtension.scale_ge_one {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : 1 ≤ ↑(scale a ha j)

theorem NavierStokes.SpatialBorelExtension.scale_strictMono {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) : StrictMono (scale a ha)

theorem NavierStokes.SpatialBorelExtension.scale_doubling {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : 2 * scale a ha j ≤ scale a ha (j + 1)

theorem NavierStokes.SpatialBorelExtension.boundSum_le_scale {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (j : ℕ) : boundSum a ha j ≤ (1 / 2) ^ j * ↑(scale a ha j)

theorem NavierStokes.SpatialBorelExtension.localized_derivative_tail_bound {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) {m j k : ℕ} (hm : m < j) (hk : k < j) (z : ℝ × X) : ‖iteratedFDeriv ℝ k (localizedTerm m (↑(scale a ha j)) j (a j)) z‖ ≤ (1 / 2) ^ j

noncomputable def NavierStokes.SpatialBorelExtension.majorant {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (m k j : ℕ) : ℝ

Majorant, with branches according to m < j ∧ k < j.

Equations

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

theorem NavierStokes.SpatialBorelExtension.majorant_summable {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (m k : ℕ) : Summable (majorant a ha m k)

theorem NavierStokes.SpatialBorelExtension.localized_derivative_bound {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (m k j : ℕ) (z : ℝ × X) : ‖iteratedFDeriv ℝ k (localizedTerm m (↑(scale a ha j)) j (a j)) z‖ ≤ majorant a ha m k j

theorem NavierStokes.SpatialBorelExtension.term_eventuallyEq_localized {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (m : ℕ) {z : ℝ × X} (hz : ‖z.2‖ < ↑m + 1) (b : ℝ) (j : ℕ) (f : X → V) : term b j f =ᶠ[nhds z] localizedTerm m b j f

theorem NavierStokes.SpatialBorelExtension.derivative_tail_bound_on_compact {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) {K : Set X} (hK : IsCompact K) (k : ℕ) : ∀ᶠ (j : ℕ) in Filter.atTop, ∀ (z : ℝ × X), z.2 ∈ K → ‖iteratedFDeriv ℝ k (term (↑(scale a ha j)) j (a j)) z‖ ≤ (1 / 2) ^ j

On any fixed compact spatial set, every joint derivative has a uniform geometric tail bound. Time is unrestricted in this estimate.

noncomputable def NavierStokes.SpatialBorelExtension.extension {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (z : ℝ × X) : V

Extension, given by ∑' j : ℕ, term (scale a ha j) j (a j) z.

Equations

• NavierStokes.SpatialBorelExtension.extension a ha z = ∑' (j : ℕ), NavierStokes.SpatialBorelExtension.term (↑(NavierStokes.SpatialBorelExtension.scale a ha j)) j (a j) z

noncomputable def NavierStokes.SpatialBorelExtension.localizedExtension {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (m : ℕ) (z : ℝ × X) : V

Localized extension, given by ∑' j : ℕ, localizedTerm m (scale a ha j) j (a j) z.

Equations

• NavierStokes.SpatialBorelExtension.localizedExtension a ha m z = ∑' (j : ℕ), NavierStokes.SpatialBorelExtension.localizedTerm m (↑(NavierStokes.SpatialBorelExtension.scale a ha j)) j (a j) z

theorem NavierStokes.SpatialBorelExtension.terms_summable {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (z : ℝ × X) : Summable fun (j : ℕ) => term (↑(scale a ha j)) j (a j) z

The defining series converges at every point; its tsum is never being used merely as the default value of a divergent series.

theorem NavierStokes.SpatialBorelExtension.localized_derivatives_summable {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (m k : ℕ) (z : ℝ × X) : Summable fun (j : ℕ) => iteratedFDeriv ℝ k (localizedTerm m (↑(scale a ha j)) j (a j)) z

theorem NavierStokes.SpatialBorelExtension.localizedExtension_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (m : ℕ) : ContDiff ℝ (↑⊤) (localizedExtension a ha m)

theorem NavierStokes.SpatialBorelExtension.localizedExtension_iteratedFDeriv {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (m k : ℕ) (z : ℝ × X) : iteratedFDeriv ℝ k (localizedExtension a ha m) z = ∑' (j : ℕ), iteratedFDeriv ℝ k (localizedTerm m (↑(scale a ha j)) j (a j)) z

theorem NavierStokes.SpatialBorelExtension.extension_eq_localized {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (m : ℕ) (z : ℝ × X) (hz : spatialCutoff m z.2 = 1) : extension a ha z = localizedExtension a ha m z

theorem NavierStokes.SpatialBorelExtension.extension_eventuallyEq_localized {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (m : ℕ) {z : ℝ × X} (hz : ‖z.2‖ < ↑m + 1) : extension a ha =ᶠ[nhds z] localizedExtension a ha m

theorem NavierStokes.SpatialBorelExtension.extension_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] : ContDiff ℝ (↑⊤) (extension a ha)

Joint smoothness in time and space follows from local equality with an all-order uniformly convergent smooth series.

theorem NavierStokes.SpatialBorelExtension.derivatives_summable {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (k : ℕ) (z : ℝ × X) : Summable fun (j : ℕ) => iteratedFDeriv ℝ k (term (↑(scale a ha j)) j (a j)) z

theorem NavierStokes.SpatialBorelExtension.extension_iteratedFDeriv {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (k : ℕ) (z : ℝ × X) : iteratedFDeriv ℝ k (extension a ha) z = ∑' (j : ℕ), iteratedFDeriv ℝ k (term (↑(scale a ha j)) j (a j)) z

theorem NavierStokes.SpatialBorelExtension.derivatives_tendstoUniformlyOn_compact {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] {K : Set X} (hK : IsCompact K) (k : ℕ) : TendstoUniformlyOn (fun (N : ℕ) (z : ℝ × X) => ∑ j ∈ Finset.range N, iteratedFDeriv ℝ k (term (↑(scale a ha j)) j (a j)) z) (iteratedFDeriv ℝ k (extension a ha)) Filter.atTop (Set.univ ×ˢ K)

Uniform convergence of every full derivative series on compact spatial sets, uniformly over all real times.

theorem NavierStokes.SpatialBorelExtension.time_iteratedDeriv {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiff ℝ (↑⊤) f) (k : ℕ) (t : ℝ) (x : X) : iteratedDeriv k (fun (s : ℝ) => f (s, x)) t = (iteratedFDeriv ℝ k f (t, x)) fun (x : Fin k) => (1, 0)

theorem NavierStokes.SpatialBorelExtension.extension_time_jets {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (k : ℕ) (x : X) : iteratedDeriv k (fun (t : ℝ) => extension a ha (t, x)) 0 = a k x

All prescribed time jets hold as equalities of smooth spatial functions.

theorem NavierStokes.SpatialBorelExtension.extension_mixed_boundary_jets {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (k l : ℕ) (x : X) : iteratedFDeriv ℝ l (fun (y : X) => iteratedDeriv k (fun (t : ℝ) => extension a ha (t, y)) 0) x = iteratedFDeriv ℝ l (a k) x

Taking any number of spatial derivatives of the boundary time-jet function gives the corresponding derivative of the prescribed coefficient.

theorem NavierStokes.SpatialBorelExtension.extension_eq_series {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (z : ℝ × X) : extension a ha z = ∑' (j : ℕ), (SmoothCutoffs.cutoff (↑(scale a ha j) * z.1) * (z.1 ^ j / ↑j.factorial)) • a j z.2

theorem NavierStokes.SpatialBorelExtension.extension_zero_of_one_le_abs {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) {z : ℝ × X} (hz : 1 ≤ |z.1|) : extension a ha z = 0

theorem NavierStokes.SpatialBorelExtension.extension_time_support {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) : tsupport (extension a ha) ⊆ Set.Icc (-1) 1 ×ˢ Set.univ

theorem NavierStokes.SpatialBorelExtension.extension_add_period {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (p : X) (hp : ∀ (j : ℕ) (x : X), a j (x + p) = a j x) (t : ℝ) (x : X) : extension a ha (t, x + p) = extension a ha (t, x)

Spatial periods of every coefficient pass to the same actual series.

theorem NavierStokes.SpatialBorelExtension.extension_zero_of_coefficients_zero {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) {x : X} (hx : ∀ (j : ℕ), a j x = 0) (t : ℝ) : extension a ha (t, x) = 0

A zero spatial slice of every coefficient stays identically zero.

noncomputable def NavierStokes.SpatialBorelExtension.rightExtension {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (T : ℝ) (z : ℝ × X) : V

Right extension, given by extension a ha (z.1 - T, z.2).

Equations

• NavierStokes.SpatialBorelExtension.rightExtension a ha T z = NavierStokes.SpatialBorelExtension.extension a ha (z.1 - T, z.2)

theorem NavierStokes.SpatialBorelExtension.rightExtension_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (T : ℝ) : ContDiff ℝ (↑⊤) (rightExtension a ha T)

theorem NavierStokes.SpatialBorelExtension.rightExtension_time_jets {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (T : ℝ) (k : ℕ) (x : X) : iteratedDeriv k (fun (t : ℝ) => rightExtension a ha T (t, x)) T = a k x

theorem NavierStokes.SpatialBorelExtension.rightExtension_right_jets {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] (T : ℝ) (k : ℕ) (x : X) : iteratedDerivWithin k (fun (t : ℝ) => rightExtension a ha T (t, x)) (Set.Ici T) T = a k x

theorem NavierStokes.SpatialBorelExtension.rightExtension_add_period {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (T : ℝ) (p : X) (hp : ∀ (j : ℕ) (x : X), a j (x + p) = a j x) (t : ℝ) (x : X) : rightExtension a ha T (t, x + p) = rightExtension a ha T (t, x)

theorem NavierStokes.SpatialBorelExtension.rightExtension_zero_from {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) (T : ℝ) {t : ℝ} (ht : T + 1 ≤ t) (x : X) : rightExtension a ha T (t, x) = 0

theorem NavierStokes.SpatialBorelExtension.exists_smooth_extension {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → X → V) (ha : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (a j)) [CompleteSpace V] : ∃ (F : ℝ × X → V), ContDiff ℝ (↑⊤) F ∧ tsupport F ⊆ Set.Icc (-1) 1 ×ˢ Set.univ ∧ ∀ (k : ℕ) (x : X), iteratedDeriv k (fun (t : ℝ) => F (t, x)) 0 = a k x

Jointly smooth realization for arbitrary smooth spatial coefficients in a finite-dimensional space, with no global growth restriction.