Off-plane endpoint extensions from actual raw jets

A compact spacetime localization converts bounds on every actual derivative in a past half-ball into a genuine smooth extension. The physical scale is then localized away from zero, so raw power-logarithmic jet bounds supply the required estimates without a recursive continuation assumption.

A dimension-independent smooth extension of a bounded-jet open strip

The endpoint values below are derived from bounds on the actual joint Frechet derivatives, using completeness and the mean-value theorem. The normal-jet gluing argument is generalized from SpacetimeGluing; no existing project source is altered and no extension or closed-side regularity is assumed.

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.timeVector {X : Type u_1} [NormedAddCommGroup X] : ℝ × X

Time vector, given by (1, 0).

Equations

• NavierStokes.GenericEndpointExtension.Gluing.timeVector = (1, 0)

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.directional {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set (ℝ × X)) (f : ℝ × X → V) (v z : ℝ × X) : V

Directional, given by fderivWithin ℝ f s z v.

Equations

• NavierStokes.GenericEndpointExtension.Gluing.directional s f v z = (fderivWithin ℝ f s z) v

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.normalIter {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set (ℝ × X)) (f : ℝ × X → V) : ℕ → ℝ × X → V

Normal iter as an element of ℕ → (ℝ × X) → V | 0 => f | n + 1 => directional s (normalIter s f n) timeVector.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.GenericEndpointExtension.Gluing.normalIter s f 0 = f

theorem NavierStokes.GenericEndpointExtension.Gluing.directional_contDiffOn {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set (ℝ × X)} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f s) (hs : UniqueDiffOn ℝ s) (v : ℝ × X) : ContDiffOn ℝ (↑⊤) (directional s f v) s

theorem NavierStokes.GenericEndpointExtension.Gluing.normalIter_contDiffOn {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set (ℝ × X)} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f s) (hs : UniqueDiffOn ℝ s) (n : ℕ) : ContDiffOn ℝ (↑⊤) (normalIter s f n) s

theorem NavierStokes.GenericEndpointExtension.Gluing.directional_commute {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set (ℝ × X)} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f s) (hs : UniqueDiffOn ℝ s) (hregular : s ⊆ closure (interior s)) {z : ℝ × X} (hz : z ∈ s) (v w : ℝ × X) : directional s (directional s f v) w z = directional s (directional s f w) v z

Schwarz's theorem commutes two fixed directional derivatives on a regular closed domain; no symmetry of full higher tensors is assumed.

theorem NavierStokes.GenericEndpointExtension.Gluing.normalIter_directional {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set (ℝ × X)} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f s) (hs : UniqueDiffOn ℝ s) (hregular : s ⊆ closure (interior s)) (v : ℝ × X) (n : ℕ) : Set.EqOn (normalIter s (directional s f v) n) (directional s (normalIter s f n) v) s

Any fixed directional derivative commutes with every normal iterate.

theorem NavierStokes.GenericEndpointExtension.Gluing.time_slice_iteratedDerivWithin {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {I : Set ℝ} {f : ℝ × X → V} (hI : UniqueDiffOn ℝ I) (hf : ContDiffOn ℝ (↑⊤) f (I ×ˢ Set.univ)) (x : X) (n : ℕ) : Set.EqOn (iteratedDerivWithin n (fun (t : ℝ) => f (t, x)) I) (fun (t : ℝ) => normalIter (I ×ˢ Set.univ) f n (t, x)) I

The joint normal iterates equal the genuine one-dimensional derivatives of the time slice, including at a one-sided boundary.

theorem NavierStokes.GenericEndpointExtension.Gluing.boundary_fderiv_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {s t : Set (ℝ × X)} {f g : ℝ × X → V} {T : ℝ} (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g t) (hBs : ∀ (x : X), (T, x) ∈ s) (hBt : ∀ (x : X), (T, x) ∈ t) (hvalue : ∀ (x : X), f (T, x) = g (T, x)) (hnormal : ∀ (x : X), directional s f timeVector (T, x) = directional t g timeVector (T, x)) (x : X) : fderivWithin ℝ f s (T, x) = fderivWithin ℝ g t (T, x)

Matching boundary values gives matching tangential derivatives; together with the first normal derivative this determines the full Frechet derivative.

theorem NavierStokes.GenericEndpointExtension.Gluing.normal_match_directional {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {s t : Set (ℝ × X)} {f g : ℝ × X → V} {T : ℝ} (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g t) (hs : UniqueDiffOn ℝ s) (ht : UniqueDiffOn ℝ t) (hregularS : s ⊆ closure (interior s)) (hregularT : t ⊆ closure (interior t)) (hBs : ∀ (x : X), (T, x) ∈ s) (hBt : ∀ (x : X), (T, x) ∈ t) (hmatch : ∀ (n : ℕ) (x : X), normalIter s f n (T, x) = normalIter t g n (T, x)) (v : ℝ × X) (n : ℕ) (x : X) : normalIter s (directional s f v) n (T, x) = normalIter t (directional t g v) n (T, x)

Matching normal trace functions implies matching normal traces after any directional derivative. The proof derives, rather than assumes, the necessary tangential and mixed derivative equalities.

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.past {X : Type u_1} (T : ℝ) : Set (ℝ × X)

Past, given by Iic T ×ˢ univ.

Equations

• NavierStokes.GenericEndpointExtension.Gluing.past T = Set.Iic T ×ˢ Set.univ

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.future {X : Type u_1} (T : ℝ) : Set (ℝ × X)

Future, given by Ici T ×ˢ univ.

Equations

• NavierStokes.GenericEndpointExtension.Gluing.future T = Set.Ici T ×ˢ Set.univ

theorem NavierStokes.GenericEndpointExtension.Gluing.past_uniqueDiff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (T : ℝ) : UniqueDiffOn ℝ (past T)

theorem NavierStokes.GenericEndpointExtension.Gluing.future_uniqueDiff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (T : ℝ) : UniqueDiffOn ℝ (future T)

theorem NavierStokes.GenericEndpointExtension.Gluing.past_regular {X : Type u_1} [NormedAddCommGroup X] (T : ℝ) : past T ⊆ closure (interior (past T))

theorem NavierStokes.GenericEndpointExtension.Gluing.future_regular {X : Type u_1} [NormedAddCommGroup X] (T : ℝ) : future T ⊆ closure (interior (future T))

theorem NavierStokes.GenericEndpointExtension.Gluing.past_union_future {X : Type u_1} (T : ℝ) : past T ∪ future T = Set.univ

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.glue {X : Type u_1} {W : Type u_3} (T : ℝ) (f g : ℝ × X → W) (z : ℝ × X) : W

Glue along the time hyperplane, using the past branch at the join.

Equations

• NavierStokes.GenericEndpointExtension.Gluing.glue T f g z = if z.1 ≤ T then f z else g z

theorem NavierStokes.GenericEndpointExtension.Gluing.glue_eqOn_past {X : Type u_1} {W : Type u_3} (T : ℝ) (f g : ℝ × X → W) : Set.EqOn (glue T f g) f (past T)

theorem NavierStokes.GenericEndpointExtension.Gluing.glue_eqOn_future {X : Type u_1} {W : Type u_3} {T : ℝ} {f g : ℝ × X → W} (hvalue : ∀ (x : X), f (T, x) = g (T, x)) : Set.EqOn (glue T f g) g (future T)

theorem NavierStokes.GenericEndpointExtension.Gluing.hasFDerivAt_glue {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : ℝ × X → V} {df dg : ℝ × X → ℝ × X →L[ℝ] V} (hf : ∀ z ∈ past T, HasFDerivWithinAt f (df z) (past T) z) (hg : ∀ z ∈ future T, HasFDerivWithinAt g (dg z) (future T) z) (hvalue : ∀ (x : X), f (T, x) = g (T, x)) (hderiv : ∀ (x : X), df (T, x) = dg (T, x)) (z : ℝ × X) : HasFDerivAt (glue T f g) (glue T df dg z) z

Actual full Frechet derivatives glue when their boundary values match.

theorem NavierStokes.GenericEndpointExtension.Gluing.hasFDerivAt_glue_of_normal {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (hg : ContDiffOn ℝ (↑⊤) g (future T)) (hvalue : ∀ (x : X), f (T, x) = g (T, x)) (hnormal : ∀ (x : X), directional (past T) f timeVector (T, x) = directional (future T) g timeVector (T, x)) (z : ℝ × X) : HasFDerivAt (glue T f g) (glue T (fderivWithin ℝ f (past T)) (fderivWithin ℝ g (future T)) z) z

First-order joint gluing needs only value and first normal-derivative matching; spatial derivative matching is a consequence.

theorem NavierStokes.GenericEndpointExtension.Gluing.contDiff_glue_finite {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (hg : ContDiffOn ℝ (↑⊤) g (future T)) (hmatch : ∀ (n : ℕ) (x : X), normalIter (past T) f n (T, x) = normalIter (future T) g n (T, x)) (m : ℕ) : ContDiff ℝ (↑m) (glue T f g)

Finite-order induction from all matching normal jets. The induction keeps the codomain fixed and differentiates in each spacetime direction.

theorem NavierStokes.GenericEndpointExtension.Gluing.contDiff_glue {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (hg : ContDiffOn ℝ (↑⊤) g (future T)) (hmatch : ∀ (n : ℕ) (x : X), iteratedDerivWithin n (fun (t : ℝ) => f (t, x)) (Set.Iic T) T = iteratedDerivWithin n (fun (t : ℝ) => g (t, x)) (Set.Ici T) T) : ContDiff ℝ (↑⊤) (glue T f g)

Joint C∞ gluing, expressed in actual one-sided time-slice jets. No matching of mixed Frechet tensors is assumed: it is derived from the normal trace functions and Schwarz's theorem.

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.normalTrace {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (f : ℝ × X → V) (n : ℕ) (x : X) : V

The actual normal jet of a closed-past field, viewed as a spatial coefficient for the Taylor--Borel construction.

Equations

• NavierStokes.GenericEndpointExtension.Gluing.normalTrace T f n x = NavierStokes.GenericEndpointExtension.Gluing.normalIter (NavierStokes.GenericEndpointExtension.Gluing.past T) f n (T, x)

theorem NavierStokes.GenericEndpointExtension.Gluing.normalTrace_contDiff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (n : ℕ) : ContDiff ℝ (↑⊤) (normalTrace T f n)

theorem NavierStokes.GenericEndpointExtension.Gluing.normalTrace_eq_time_jet {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (n : ℕ) (x : X) : normalTrace T f n x = iteratedDerivWithin n (fun (t : ℝ) => f (t, x)) (Set.Iic T) T

theorem NavierStokes.GenericEndpointExtension.Gluing.normalTrace_add_period {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (p : X) (hperiod : ∀ t ≤ T, ∀ (x : X), f (t, x + p) = f (t, x)) (n : ℕ) (x : X) : normalTrace T f n (x + p) = normalTrace T f n x

noncomputable def NavierStokes.GenericEndpointExtension.Gluing.smoothExtension {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (f : ℝ × X → V) (hf : ContDiffOn ℝ (↑⊤) f (past T)) : ℝ × X → V

A constructed global extension: join the closed-past field to the Taylor--Borel realization of its actual normal jets.

Equations

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

theorem NavierStokes.GenericEndpointExtension.Gluing.smoothExtension_contDiff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) : ContDiff ℝ (↑⊤) (smoothExtension T f hf)

theorem NavierStokes.GenericEndpointExtension.Gluing.smoothExtension_eqOn_past {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) : Set.EqOn (smoothExtension T f hf) f (past T)

theorem NavierStokes.GenericEndpointExtension.Gluing.smoothExtension_zero_from {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) {t : ℝ} (ht : T + 1 ≤ t) (x : X) : smoothExtension T f hf (t, x) = 0

theorem NavierStokes.GenericEndpointExtension.Gluing.smoothExtension_iteratedFDeriv {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (n : ℕ) {z : ℝ × X} (hz : z ∈ past T) : iteratedFDeriv ℝ n (smoothExtension T f hf) z = iteratedFDerivWithin ℝ n f (past T) z

Every full mixed jet on the past, including the boundary, is preserved.

theorem NavierStokes.GenericEndpointExtension.Gluing.smoothExtension_add_period {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (p : X) (hperiod : ∀ t ≤ T, ∀ (x : X), f (t, x + p) = f (t, x)) (t : ℝ) (x : X) : smoothExtension T f hf (t, x + p) = smoothExtension T f hf (t, x)

theorem NavierStokes.GenericEndpointExtension.exists_limit_of_uniformContinuousOn {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedAddCommGroup V] [CompleteSpace V] {s : Set Y} {f : Y → V} (hf : UniformContinuousOn f s) {x : Y} (hx : x ∈ closure s) : ∃ (v : V), Filter.Tendsto f (nhdsWithin x s) (nhds v)

Uniform continuity makes the actual values Cauchy at every point of the closure. Completeness supplies a limit; it is not an input assumption.

theorem NavierStokes.GenericEndpointExtension.actualJet_hasFDerivAt {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (n : ℕ) {x : Y} (hx : x ∈ s) : HasFDerivAt (iteratedFDeriv ℝ n f) (iteratedFDeriv ℝ (n + 1) f x).curryLeft x

The genuine joint derivatives are differentiable inside the open set.

theorem NavierStokes.GenericEndpointExtension.actualJet_uniformContinuousOn {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hc : Convex ℝ s) (hf : ContDiffOn ℝ (↑⊤) f s) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ x ∈ s, ‖iteratedFDeriv ℝ n f x‖ ≤ C) (n : ℕ) : UniformContinuousOn (iteratedFDeriv ℝ n f) s

A bound for derivative n+1 controls differences of the actual n-th joint derivative on the convex set.

noncomputable def NavierStokes.GenericEndpointExtension.closureJet {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set Y) (f : Y → V) (n : ℕ) : Y → Y [×n]→L[ℝ] V

The continuous completion of an actual joint derivative tensor.

Equations

• NavierStokes.GenericEndpointExtension.closureJet s f n = extendFrom s (iteratedFDeriv ℝ n f)

theorem NavierStokes.GenericEndpointExtension.closureJet_limit {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hc : Convex ℝ s) (hf : ContDiffOn ℝ (↑⊤) f s) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ x ∈ s, ‖iteratedFDeriv ℝ n f x‖ ≤ C) (n : ℕ) {x : Y} (hx : x ∈ closure s) : Filter.Tendsto (iteratedFDeriv ℝ n f) (nhdsWithin x s) (nhds (closureJet s f n x))

theorem NavierStokes.GenericEndpointExtension.closureJet_continuousOn {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hc : Convex ℝ s) (hf : ContDiffOn ℝ (↑⊤) f s) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ x ∈ s, ‖iteratedFDeriv ℝ n f x‖ ≤ C) (n : ℕ) : ContinuousOn (closureJet s f n) (closure s)

theorem NavierStokes.GenericEndpointExtension.closureJet_eq {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (n : ℕ) {x : Y} (hx : x ∈ s) : closureJet s f n x = iteratedFDeriv ℝ n f x

theorem NavierStokes.GenericEndpointExtension.closureJet_eventuallyEq {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) (n : ℕ) {x : Y} (hx : x ∈ s) : closureJet s f n =ᶠ[nhds x] iteratedFDeriv ℝ n f

theorem NavierStokes.GenericEndpointExtension.closureJet_hasFDerivWithinAt {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hc : Convex ℝ s) (hf : ContDiffOn ℝ (↑⊤) f s) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ x ∈ s, ‖iteratedFDeriv ℝ n f x‖ ≤ C) (n : ℕ) {x : Y} (hx : x ∈ closure s) : HasFDerivWithinAt (closureJet s f n) (closureJet s f (n + 1) x).curryLeft (closure s) x

The mean-value theorem identifies the derivatives of the completed tensors on the boundary, including all mixed derivative directions.

noncomputable def NavierStokes.GenericEndpointExtension.closedField {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set Y) (f : Y → V) (x : Y) : V

Complete the values using the zeroth tensor.

Equations

• NavierStokes.GenericEndpointExtension.closedField s f x = (NavierStokes.GenericEndpointExtension.closureJet s f 0 x).curry0

theorem NavierStokes.GenericEndpointExtension.closedField_eq {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hf : ContDiffOn ℝ (↑⊤) f s) {x : Y} (hx : x ∈ s) : closedField s f x = f x

theorem NavierStokes.GenericEndpointExtension.closedField_contDiffOn {Y : Type u_1} {V : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {s : Set Y} {f : Y → V} (hs : IsOpen s) (hc : Convex ℝ s) (hf : ContDiffOn ℝ (↑⊤) f s) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ x ∈ s, ‖iteratedFDeriv ℝ n f x‖ ≤ C) : ContDiffOn ℝ (↑⊤) (closedField s f) (closure s)

Actual uniform joint derivative bounds give joint smoothness on the closure. In particular no one-sided trace regularity is assumed.

def NavierStokes.GenericEndpointExtension.openStrip {X : Type u_1} : Set (ℝ × X)

Open strip, given by Ioo (-1 : ℝ) 1 ×ˢ univ.

Equations

• NavierStokes.GenericEndpointExtension.openStrip = Set.Ioo (-1) 1 ×ˢ Set.univ

def NavierStokes.GenericEndpointExtension.closedStrip {X : Type u_1} : Set (ℝ × X)

Closed strip, given by Icc (-1 : ℝ) 1 ×ˢ univ.

Equations

• NavierStokes.GenericEndpointExtension.closedStrip = Set.Icc (-1) 1 ×ˢ Set.univ

theorem NavierStokes.GenericEndpointExtension.openStrip_isOpen {X : Type u_1} [NormedAddCommGroup X] : IsOpen openStrip

theorem NavierStokes.GenericEndpointExtension.openStrip_convex {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : Convex ℝ openStrip

theorem NavierStokes.GenericEndpointExtension.closure_openStrip {X : Type u_1} [NormedAddCommGroup X] : closure openStrip = closedStrip

theorem NavierStokes.GenericEndpointExtension.stripClosedField_contDiffOn {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) : ContDiffOn ℝ (↑⊤) (closedField openStrip f) closedStrip

theorem NavierStokes.GenericEndpointExtension.stripClosedField_zero {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) {x : X} (hz : ∀ t ∈ Set.Ioo (-1) 1, f (t, x) = 0) {t : ℝ} (ht : t ∈ Set.Icc (-1) 1) : closedField openStrip f (t, x) = 0

A fiber that vanishes on the open strip also vanishes at its two completed endpoints. This follows from continuity, not a support enlargement.

theorem NavierStokes.GenericEndpointExtension.stripClosedField_add_period {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) (p : X) (hp : ∀ t ∈ Set.Ioo (-1) 1, ∀ (x : X), f (t, x + p) = f (t, x)) {t : ℝ} (ht : t ∈ Set.Icc (-1) 1) (x : X) : closedField openStrip f (t, x + p) = closedField openStrip f (t, x)

Every spatial additive period passes to both completed boundary values.

noncomputable def NavierStokes.GenericEndpointExtension.lowerClamp (t : ℝ) : ℝ

A fixed smooth retraction of the past into the closed strip, equal to the identity for t ≥ -1/2.

Equations

• NavierStokes.GenericEndpointExtension.lowerClamp t = t * (2 * t + 2).smoothTransition

theorem NavierStokes.GenericEndpointExtension.lowerClamp_contDiff : ContDiff ℝ (↑⊤) lowerClamp

theorem NavierStokes.GenericEndpointExtension.lowerClamp_eq {t : ℝ} (ht : -1 / 2 ≤ t) : lowerClamp t = t

theorem NavierStokes.GenericEndpointExtension.lowerClamp_mem {t : ℝ} (ht : t ≤ 1) : lowerClamp t ∈ Set.Icc (-1) 1

noncomputable def NavierStokes.GenericEndpointExtension.clamped {X : Type u_1} {V : Type u_2} (f : ℝ × X → V) (z : ℝ × X) : V

Clamped, given by f (lowerClamp z.1, z.2).

Equations

• NavierStokes.GenericEndpointExtension.clamped f z = f (NavierStokes.GenericEndpointExtension.lowerClamp z.1, z.2)

theorem NavierStokes.GenericEndpointExtension.clamped_contDiffOn {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) : ContDiffOn ℝ (↑⊤) (clamped f) (Gluing.past 1)

theorem NavierStokes.GenericEndpointExtension.Gluing.smoothExtension_zero_fiber {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) {x : X} (hz : ∀ t ≤ T, f (t, x) = 0) (t : ℝ) : smoothExtension T f hf (t, x) = 0

Zero normal coefficients stay zero in the actual Borel series.

noncomputable def NavierStokes.GenericEndpointExtension.upperClosed {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (f : ℝ × X → V) (hf : ContDiffOn ℝ (↑⊤) f closedStrip) : ℝ × X → V

Upper closed, given by Gluing.smoothExtension 1 (clamped f) (clamped_contDiffOn hf).

Equations

• NavierStokes.GenericEndpointExtension.upperClosed f hf = NavierStokes.GenericEndpointExtension.Gluing.smoothExtension 1 (NavierStokes.GenericEndpointExtension.clamped f) ⋯

theorem NavierStokes.GenericEndpointExtension.upperClosed_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) : ContDiff ℝ (↑⊤) (upperClosed f hf)

theorem NavierStokes.GenericEndpointExtension.upperClosed_eq {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) {t : ℝ} (hlo : -1 / 2 ≤ t) (hhi : t ≤ 1) (x : X) : upperClosed f hf (t, x) = f (t, x)

theorem NavierStokes.GenericEndpointExtension.upperClosed_zero {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) {x : X} (hz : ∀ t ∈ Set.Icc (-1) 1, f (t, x) = 0) (t : ℝ) : upperClosed f hf (t, x) = 0

theorem NavierStokes.GenericEndpointExtension.upperClosed_add_period {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) (p : X) (hp : ∀ t ∈ Set.Icc (-1) 1, ∀ (x : X), f (t, x + p) = f (t, x)) (t : ℝ) (x : X) : upperClosed f hf (t, x + p) = upperClosed f hf (t, x)

noncomputable def NavierStokes.GenericEndpointExtension.reflect {X : Type u_1} {V : Type u_2} (f : ℝ × X → V) (z : ℝ × X) : V

Reflect, given by f (-z.1, z.2).

Equations

• NavierStokes.GenericEndpointExtension.reflect f z = f (-z.1, z.2)

theorem NavierStokes.GenericEndpointExtension.reflect_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (reflect f)

theorem NavierStokes.GenericEndpointExtension.reflect_contDiffOn {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) : ContDiffOn ℝ (↑⊤) (reflect f) closedStrip

noncomputable def NavierStokes.GenericEndpointExtension.lowerClosed {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (f : ℝ × X → V) (hf : ContDiffOn ℝ (↑⊤) f closedStrip) : ℝ × X → V

Lower closed, given by reflect (upperClosed (reflect f) (reflect_contDiffOn hf)).

Equations

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

theorem NavierStokes.GenericEndpointExtension.lowerClosed_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) : ContDiff ℝ (↑⊤) (lowerClosed f hf)

theorem NavierStokes.GenericEndpointExtension.lowerClosed_eq {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) {t : ℝ} (hlo : -1 ≤ t) (hhi : t ≤ 1 / 2) (x : X) : lowerClosed f hf (t, x) = f (t, x)

theorem NavierStokes.GenericEndpointExtension.lowerClosed_zero {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) {x : X} (hz : ∀ t ∈ Set.Icc (-1) 1, f (t, x) = 0) (t : ℝ) : lowerClosed f hf (t, x) = 0

theorem NavierStokes.GenericEndpointExtension.lowerClosed_add_period {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) (p : X) (hp : ∀ t ∈ Set.Icc (-1) 1, ∀ (x : X), f (t, x + p) = f (t, x)) (t : ℝ) (x : X) : lowerClosed f hf (t, x + p) = lowerClosed f hf (t, x)

noncomputable def NavierStokes.GenericEndpointExtension.closedStripExtension {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (f : ℝ × X → V) (hf : ContDiffOn ℝ (↑⊤) f closedStrip) (z : ℝ × X) : V

Use the lower continuation for negative parameters and the upper continuation for positive ones. They agree on a whole central strip.

Equations

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

theorem NavierStokes.GenericEndpointExtension.closedStripExtension_eq {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) {z : ℝ × X} (hz : z ∈ closedStrip) : closedStripExtension f hf z = f z

theorem NavierStokes.GenericEndpointExtension.closedStripExtension_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) : ContDiff ℝ (↑⊤) (closedStripExtension f hf)

theorem NavierStokes.GenericEndpointExtension.closedStripExtension_zero {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) {x : X} (hz : ∀ t ∈ Set.Icc (-1) 1, f (t, x) = 0) (t : ℝ) : closedStripExtension f hf (t, x) = 0

theorem NavierStokes.GenericEndpointExtension.closedStripExtension_add_period {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) (p : X) (hp : ∀ t ∈ Set.Icc (-1) 1, ∀ (x : X), f (t, x + p) = f (t, x)) (t : ℝ) (x : X) : closedStripExtension f hf (t, x + p) = closedStripExtension f hf (t, x)

theorem NavierStokes.GenericEndpointExtension.closedStripExtension_zero_parameter {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f closedStrip) {t : ℝ} (ht : 2 ≤ |t|) (x : X) : closedStripExtension f hf (t, x) = 0

noncomputable def NavierStokes.GenericEndpointExtension.extension {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (f : ℝ × X → V) (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) : ℝ × X → V

The constructed extension takes only interior smoothness and bounds on the actual joint derivatives as inputs.

Equations

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

theorem NavierStokes.GenericEndpointExtension.extension_contDiff {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) : ContDiff ℝ (↑⊤) (extension f hf hb)

theorem NavierStokes.GenericEndpointExtension.extension_eq {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) {z : ℝ × X} (hz : z ∈ openStrip) : extension f hf hb z = f z

theorem NavierStokes.GenericEndpointExtension.extension_zero_of_fiber {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) {x : X} (hz : ∀ t ∈ Set.Ioo (-1) 1, f (t, x) = 0) (t : ℝ) : extension f hf hb (t, x) = 0

theorem NavierStokes.GenericEndpointExtension.extension_add_period {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) (p : X) (hp : ∀ t ∈ Set.Ioo (-1) 1, ∀ (x : X), f (t, x + p) = f (t, x)) (t : ℝ) (x : X) : extension f hf hb (t, x + p) = extension f hf hb (t, x)

theorem NavierStokes.GenericEndpointExtension.extension_zero_parameter {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) {t : ℝ} (ht : 2 ≤ |t|) (x : X) : extension f hf hb (t, x) = 0

theorem NavierStokes.GenericEndpointExtension.extension_iteratedFDeriv {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ℝ × X → V} (hf : ContDiffOn ℝ (↑⊤) f openStrip) (hb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ z ∈ openStrip, ‖iteratedFDeriv ℝ n f z‖ ≤ C) (n : ℕ) {z : ℝ × X} (hz : z ∈ openStrip) : iteratedFDeriv ℝ n (extension f hf hb) z = iteratedFDeriv ℝ n f z

noncomputable def NavierStokes.OffplaneJetExtensions.pastBall (x : ProblemStatement.Space) (r : ℝ) : Set ProblemStatement.SpaceTime

Past ball, given by Metric.ball (1, x) r ∩ SpacetimeEndpoint.openPast 1.

Equations

• NavierStokes.OffplaneJetExtensions.pastBall x r = Metric.ball (1, x) r ∩ NavierStokes.SpacetimeEndpoint.openPast 1

theorem NavierStokes.OffplaneJetExtensions.pastBall_open (x : ProblemStatement.Space) (r : ℝ) : IsOpen (pastBall x r)

noncomputable def NavierStokes.OffplaneJetExtensions.localBump (x : ProblemStatement.Space) {r : ℝ} (hr : 0 < r) : ContDiffBump (1, x)

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

Equations

• NavierStokes.OffplaneJetExtensions.localBump x hr = { rIn := r / 4, rOut := r / 2, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem NavierStokes.OffplaneJetExtensions.localBump_support (x : ProblemStatement.Space) {r : ℝ} (hr : 0 < r) : tsupport ↑(localBump x hr) ⊆ Metric.ball (1, x) r

theorem NavierStokes.OffplaneJetExtensions.localBump_jet_bounded (x : ProblemStatement.Space) {r : ℝ} (hr : 0 < r) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (w : ProblemStatement.SpaceTime), ‖iteratedFDeriv ℝ m (↑(localBump x hr)) w‖ ≤ C

noncomputable def NavierStokes.OffplaneJetExtensions.localized {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : ProblemStatement.SpaceTime → V) (x : ProblemStatement.Space) {r : ℝ} (hr : 0 < r) (w : ProblemStatement.SpaceTime) : V

Localized, given by localBump x hr w • f w.

Equations

• NavierStokes.OffplaneJetExtensions.localized f x hr w = ↑(NavierStokes.OffplaneJetExtensions.localBump x hr) w • f w

theorem NavierStokes.OffplaneJetExtensions.localized_zero_germ {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : ProblemStatement.SpaceTime → V) (x : ProblemStatement.Space) {r : ℝ} (hr : 0 < r) {w : ProblemStatement.SpaceTime} (hw : w ∉ tsupport ↑(localBump x hr)) : localized f x hr =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.OffplaneJetExtensions.localized_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} {x : ProblemStatement.Space} {r : ℝ} (hr : 0 < r) (hf : ContDiffOn ℝ (↑⊤) f (pastBall x r)) : ContDiffOn ℝ (↑⊤) (localized f x hr) GenericEndpointExtension.openStrip

theorem NavierStokes.OffplaneJetExtensions.localized_jets_bounded {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} {x : ProblemStatement.Space} {r : ℝ} (hr : 0 < r) (hf : ContDiffOn ℝ (↑⊤) f (pastBall x r)) (hb : ∀ (m : ℕ), ∃ (C : ℝ), ∀ w ∈ pastBall x r, ‖iteratedFDeriv ℝ m f w‖ ≤ C) (m : ℕ) : ∃ (C : ℝ), ∀ w ∈ GenericEndpointExtension.openStrip, ‖iteratedFDeriv ℝ m (localized f x hr) w‖ ≤ C

theorem NavierStokes.OffplaneJetExtensions.extension_of_local_jets {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f : ProblemStatement.SpaceTime → V} {x : ProblemStatement.Space} {r : ℝ} (hr : 0 < r) (hf : ContDiffOn ℝ (↑⊤) f (pastBall x r)) (hb : ∀ (m : ℕ), ∃ (C : ℝ), ∀ w ∈ pastBall x r, ‖iteratedFDeriv ℝ m f w‖ ≤ C) : Nonempty (JointResidualLimits.OneSidedExtension f x)

A local bound for every actual joint derivative supplies an actual smooth extension. Endpoint derivative limits are constructed by the generic extension theorem; they are not additional inputs.

theorem NavierStokes.OffplaneJetExtensions.exists_scale_neighborhood {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hq : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : ∃ (r : ℝ), 0 < r ∧ ∀ w ∈ pastBall x r, w ∈ CutStageEstimates.physicalSublevel h qbig ∧ EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) / 2 < PhysicalWaveSum.physicalQ h w ∧ |w.1| ≤ 1

One neighborhood controls the physical scale for all derivative orders. Only the actual past coordinate is used in the conclusion.

theorem NavierStokes.OffplaneJetExtensions.powerLog_bounded {a : ℝ} (ha : 0 < a) (C p e : ℝ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ q ∈ Set.Icc a 1, C * (1 + |Real.log q|) ^ p * q ^ e ≤ K

Arbitrary real powers and logarithmic losses are uniformly bounded when the scale lies in a fixed compact subinterval of (0,∞).

theorem NavierStokes.OffplaneJetExtensions.extension_of_powerLog_jets {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) {f : ProblemStatement.SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (CutStageEstimates.physicalSublevel h qbig)) (hb : ∀ (m : ℕ), ∃ (C : ℝ) (p : ℝ) (e : ℝ), ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * (1 + |Real.log (PhysicalWaveSum.physicalQ h w)|) ^ p * PhysicalWaveSum.physicalQ h w ^ e) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension f x)

A single-field endpoint theorem, including the bounded finite pieces at stage zero. It assumes only their actual interior jet estimates.

theorem NavierStokes.OffplaneJetExtensions.extension_of_power_jets {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) {f : ProblemStatement.SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (CutStageEstimates.physicalSublevel h qbig)) (hb : ∀ (m : ℕ), ∃ (C : ℝ) (e : ℝ), ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m f w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ e) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension f x)

theorem NavierStokes.OffplaneJetExtensions.rawStage_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) {F : ℕ → ProblemStatement.SpaceTime → V} {g L : ℕ → ℝ} {C p : ℕ → ℕ → ℝ} (hb : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) F g L C p (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)) {j : ℕ} (hj : 1 ≤ j) (hf : ContDiffOn ℝ (↑⊤) (F j) (CutStageEstimates.physicalSublevel h qbig)) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension (F j) x)

Positive raw stages extend directly from RawStageBounds. The stage index hypothesis is retained exactly: no stage-zero estimate is inferred.

theorem NavierStokes.OffplaneJetExtensions.rawStages_extensions {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) {F : ℕ → ProblemStatement.SpaceTime → V} {g L : ℕ → ℝ} {C p : ℕ → ℕ → ℝ} (hb : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) F g L C p (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)) (hf : ∀ (j : ℕ), 1 ≤ j → ContDiffOn ℝ (↑⊤) (F j) (CutStageEstimates.physicalSublevel h qbig)) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) (j : ℕ) : 1 ≤ j → Nonempty (JointResidualLimits.OneSidedExtension (F j) x)

noncomputable def NavierStokes.OffplaneJetExtensions.addExtension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : ProblemStatement.SpaceTime → V} {x : ProblemStatement.Space} (ef : JointResidualLimits.OneSidedExtension f x) (eg : JointResidualLimits.OneSidedExtension g x) : JointResidualLimits.OneSidedExtension (fun (w : JointResidualLimits.SpaceTime) => f w + g w) x

Combine, for example, the existing base-gauge extension with the separately derived extension of the finite initial correction.

Equations

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

theorem NavierStokes.OffplaneJetExtensions.extension_add {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : ProblemStatement.SpaceTime → V} {x : ProblemStatement.Space} (hf : Nonempty (JointResidualLimits.OneSidedExtension f x)) (hg : Nonempty (JointResidualLimits.OneSidedExtension g x)) : Nonempty (JointResidualLimits.OneSidedExtension (fun (w : JointResidualLimits.SpaceTime) => f w + g w) x)

theorem NavierStokes.OffplaneJetExtensions.extension_of_eqOn_sublevel {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f g : ProblemStatement.SpaceTime → V} (he : Set.EqOn f g (CutStageEstimates.physicalSublevel h qbig)) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) (eg : Nonempty (JointResidualLimits.OneSidedExtension g x)) : Nonempty (JointResidualLimits.OneSidedExtension f x)

The constructed stage need only agree with the bounded model on its actual validity region. The positive scale margin supplies the required past neighborhood automatically.

theorem NavierStokes.OffplaneJetExtensions.mean_field_extension {h degree qbig : ℝ} (M : ActualPhysicalStageBounds.MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) (hq : qbig ≤ ChartScales.Q M.firstBand) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension M.family.field x)

theorem NavierStokes.OffplaneJetExtensions.mean_angular_extension {h degree qbig : ℝ} (M : ActualPhysicalStageBounds.MeanInput h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) (hq : qbig ≤ ChartScales.Q M.firstBand) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension M.family.angularField x)

theorem NavierStokes.OffplaneJetExtensions.initialIncrement_extension {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {h qbig : ℝ} (W : PhysicalStageBounds.WaveData h D I K (Fin 3)) (MT MR : ActualPhysicalStageBounds.MeanInput h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) (hqT : qbig ≤ ChartScales.Q MT.firstBand) (hqR : qbig ≤ ChartScales.Q MR.firstBand) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension (ActualPhysicalStageBounds.initialIncrement W MT MR) x)

The finite initialized potential correction has its own derived estimate. This theorem does not apply the positive-stage bound to index zero.

theorem NavierStokes.OffplaneJetExtensions.initialPressureIncrement_extension {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {h qbig : ℝ} (W : PhysicalStageBounds.WaveData h D I K Unit) (M : ActualPhysicalStageBounds.MeanInput h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : qbig ≤ 1) (hq : qbig ≤ ChartScales.Q M.firstBand) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (hqx : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < qbig) : Nonempty (JointResidualLimits.OneSidedExtension (ActualPhysicalStageBounds.initialPressureIncrement W M) x)