Joint spacetime endpoint regularity from locally uniform derivative limits

The domain is the concrete four-dimensional spacetime ℝ × ℝ³. All derivative data below are full Frechet derivative tensors, and convergence is locally uniform in the spatial variable in the tensor norm. Closed-side smoothness is proved from these data, rather than included as a hypothesis.

@[reducible, inline]

abbrev NavierStokes.SpacetimeEndpoint.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.SpacetimeEndpoint.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.SpacetimeEndpoint.SpaceTime : Type

Space time: an abbreviation for ProblemStatement.SpaceTime.

Equations

• NavierStokes.SpacetimeEndpoint.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

def NavierStokes.SpacetimeEndpoint.openPast (T : ℝ) : Set SpaceTime

Open past, given by Iio T ×ˢ univ.

Equations

• NavierStokes.SpacetimeEndpoint.openPast T = Set.Iio T ×ˢ Set.univ

def NavierStokes.SpacetimeEndpoint.closedPast (T : ℝ) : Set SpaceTime

Closed past, given by Iic T ×ˢ univ.

Equations

• NavierStokes.SpacetimeEndpoint.closedPast T = Set.Iic T ×ˢ Set.univ

theorem NavierStokes.SpacetimeEndpoint.openPast_isOpen (T : ℝ) : IsOpen (openPast T)

theorem NavierStokes.SpacetimeEndpoint.openPast_convex (T : ℝ) : Convex ℝ (openPast T)

theorem NavierStokes.SpacetimeEndpoint.closure_openPast (T : ℝ) : closure (openPast T) = closedPast T

theorem NavierStokes.SpacetimeEndpoint.closedPast_uniqueDiff (T : ℝ) : UniqueDiffOn ℝ (closedPast T)

noncomputable def NavierStokes.SpacetimeEndpoint.extendTrace {V : Type u_1} (T : ℝ) (f : SpaceTime → V) (L : Space → V) (z : SpaceTime) : V

Extend by the boundary trace. Only closed-past smoothness is claimed.

Equations

• NavierStokes.SpacetimeEndpoint.extendTrace T f L z = if z.1 < T then f z else L z.2

theorem NavierStokes.SpacetimeEndpoint.extendTrace_of_lt {V : Type u_1} {T : ℝ} {f : SpaceTime → V} {L : Space → V} {z : SpaceTime} (hz : z.1 < T) : extendTrace T f L z = f z

@[simp]

theorem NavierStokes.SpacetimeEndpoint.extendTrace_at {V : Type u_1} (T : ℝ) (f : SpaceTime → V) (L : Space → V) (x : Space) : extendTrace T f L (T, x) = L x

theorem NavierStokes.SpacetimeEndpoint.hasFDerivAt_extendTrace {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {L : Space → V} {z : SpaceTime} {f' : SpaceTime →L[ℝ] V} (hz : z.1 < T) (hf : HasFDerivAt f f' z) : HasFDerivAt (extendTrace T f L) f' z

theorem NavierStokes.SpacetimeEndpoint.trace_continuous {V : Type u_1} [NormedAddCommGroup V] {T : ℝ} {f : SpaceTime → V} {L : Space → V} (hcont : ∀ t < T, Continuous fun (x : Space) => f (t, x)) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) L (nhdsWithin T (Set.Iio T))) : Continuous L

Local-uniform limits of continuous spatial slices are continuous traces.

theorem NavierStokes.SpacetimeEndpoint.joint_tendsto_at_boundary {V : Type u_1} [NormedAddCommGroup V] {T : ℝ} {f : SpaceTime → V} {L : Space → V} (hL : Continuous L) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) L (nhdsWithin T (Set.Iio T))) (x : Space) : Filter.Tendsto f (nhdsWithin (T, x) (openPast T)) (nhds (L x))

The local-uniform hypothesis controls simultaneous motion in time and space; this is stronger than convergence at each fixed spatial point.

theorem NavierStokes.SpacetimeEndpoint.extendTrace_continuousWithinAt_boundary {V : Type u_1} [NormedAddCommGroup V] {T : ℝ} {f : SpaceTime → V} {L : Space → V} (hL : Continuous L) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) L (nhdsWithin T (Set.Iio T))) (x : Space) : ContinuousWithinAt (extendTrace T f L) (openPast T) (T, x)

theorem NavierStokes.SpacetimeEndpoint.trace_periodic {V : Type u_1} [NormedAddCommGroup V] {T : ℝ} {f : SpaceTime → V} {L : Space → V} (v : Space) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) L (nhdsWithin T (Set.Iio T))) (hperiod : ∀ t < T, ∀ (x : Space), f (t, x + v) = f (t, x)) (x : Space) : L (x + v) = L x

Every spatial period of the slices passes to the boundary trace.

theorem NavierStokes.SpacetimeEndpoint.extendTrace_periodic {V : Type u_1} [NormedAddCommGroup V] {T : ℝ} {f : SpaceTime → V} {L : Space → V} (v : Space) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) L (nhdsWithin T (Set.Iio T))) (hperiod : ∀ t < T, ∀ (x : Space), f (t, x + v) = f (t, x)) (t : ℝ) (x : Space) : extendTrace T f L (t, x + v) = extendTrace T f L (t, x)

theorem NavierStokes.SpacetimeEndpoint.locallyUniform_linearMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {T : ℝ} {f : SpaceTime → V} {L : Space → V} (A : V →L[ℝ] W) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) L (nhdsWithin T (Set.Iio T))) : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => A (f (t, x))) (fun (x : ProblemStatement.Space) => A (L x)) (nhdsWithin T (Set.Iio T))

A fixed continuous linear map preserves the locally uniform limit.

theorem NavierStokes.SpacetimeEndpoint.hasFDerivWithinAt_extendTrace {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {f' : SpaceTime → SpaceTime →L[ℝ] V} {L : Space → V} {L' : Space → SpaceTime →L[ℝ] V} (hderiv : ∀ (z : SpaceTime), z.1 < T → HasFDerivAt f (f' z) z) (hL : Continuous L) (hL' : Continuous L') (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) L (nhdsWithin T (Set.Iio T))) (hlim' : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f' (t, x)) L' (nhdsWithin T (Set.Iio T))) (z : SpaceTime) (hz : z ∈ closedPast T) : HasFDerivWithinAt (extendTrace T f L) (extendTrace T f' L' z) (closedPast T) z

The full Frechet derivative extends to the boundary. The proof uses the mean-value theorem on the convex open past halfspace.

noncomputable def NavierStokes.SpacetimeEndpoint.extendJets {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V) (L : Space → FormalMultilinearSeries ℝ SpaceTime V) (z : SpaceTime) : FormalMultilinearSeries ℝ SpaceTime V

Extend every actual mixed derivative tensor by its spatial boundary trace.

Equations

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

theorem NavierStokes.SpacetimeEndpoint.derivative_trace_continuous {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) (n : ℕ) : Continuous fun (x : Space) => L x n

theorem NavierStokes.SpacetimeEndpoint.extendedJets_hasFDerivWithinAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) (n : ℕ) (z : SpaceTime) (hz : z ∈ closedPast T) : HasFDerivWithinAt (fun (y : SpaceTime) => extendJets T J L y n) (extendJets T J L z (n + 1)).curryLeft (closedPast T) z

All tensor derivatives remain compatible after taking boundary limits. This is an actual HasFDerivWithinAt statement on the closed halfspace.

theorem NavierStokes.SpacetimeEndpoint.hasFTaylorSeriesUpToOn_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hzero : ∀ (z : SpaceTime), z.1 < T → (J z 0).curry0 = f z) (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) : HasFTaylorSeriesUpToOn (↑⊤) (extendTrace T f fun (x : Space) => (L x 0).curry0) (extendJets T J L) (closedPast T)

The limiting derivative tensors form the actual smooth Taylor family of the extended field. All fields of this predicate are proved.

theorem NavierStokes.SpacetimeEndpoint.contDiffOn_joint_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hzero : ∀ (z : SpaceTime), z.1 < T → (J z 0).curry0 = f z) (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) : ContDiffOn ℝ (↑⊤) (extendTrace T f fun (x : Space) => (L x 0).curry0) (closedPast T)

Main joint endpoint theorem: local-uniform limits of every compatible full Frechet derivative imply joint C∞ regularity on the closed past.

theorem NavierStokes.SpacetimeEndpoint.iteratedFDerivWithin_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hzero : ∀ (z : SpaceTime), z.1 < T → (J z 0).curry0 = f z) (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) (n : ℕ) (z : SpaceTime) (hz : z ∈ closedPast T) : iteratedFDerivWithin ℝ n (extendTrace T f fun (x : Space) => (L x 0).curry0) (closedPast T) z = extendJets T J L z n

The limit tensors are the genuine mixed derivative jets of the extension.

theorem NavierStokes.SpacetimeEndpoint.boundary_jets_eq_limits {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hzero : ∀ (z : SpaceTime), z.1 < T → (J z 0).curry0 = f z) (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) (n : ℕ) (x : Space) : iteratedFDerivWithin ℝ n (extendTrace T f fun (y : Space) => (L y 0).curry0) (closedPast T) (T, x) = L x n

theorem NavierStokes.SpacetimeEndpoint.extendedJets_contDiffOn {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : SpaceTime) => extendJets T J L z n) (closedPast T)

Every extended mixed-derivative tensor is itself jointly smooth.

theorem NavierStokes.SpacetimeEndpoint.boundary_tensors_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) (n : ℕ) : ContDiff ℝ ↑⊤ fun (x : Space) => L x n

The boundary limits are smooth spatial coefficient functions, as required for a spatial Taylor--Borel construction. This regularity is derived.

theorem NavierStokes.SpacetimeEndpoint.field_locallyUniform_limit {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hzero : ∀ (z : SpaceTime), z.1 < T → (J z 0).curry0 = f z) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) 0) (fun (x : ProblemStatement.Space) => L x 0) (nhdsWithin T (Set.Iio T))) : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => f (t, x)) (fun (x : ProblemStatement.Space) => (L x 0).curry0) (nhdsWithin T (Set.Iio T))

theorem NavierStokes.SpacetimeEndpoint.unit_periods_joint_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hzero : ∀ (z : SpaceTime), z.1 < T → (J z 0).curry0 = f z) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) 0) (fun (x : ProblemStatement.Space) => L x 0) (nhdsWithin T (Set.Iio T))) (hperiod : ProblemStatement.UnitSpatialPeriodsOn (Set.Iio T) f) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (extendTrace T f fun (x : Space) => (L x 0).curry0)

Unit spatial periods are retained by the constructed endpoint extension.

theorem NavierStokes.SpacetimeEndpoint.exists_joint_endpoint_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} {J : SpaceTime → FormalMultilinearSeries ℝ SpaceTime V} {L : Space → FormalMultilinearSeries ℝ SpaceTime V} (hzero : ∀ (z : SpaceTime), z.1 < T → (J z 0).curry0 = f z) (hderiv : ∀ (n : ℕ) (z : SpaceTime), z.1 < T → HasFDerivAt (fun (y : SpaceTime) => J y n) (J z (n + 1)).curryLeft z) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => J (t, x) n) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin T (Set.Iio T))) : ∃ (g : SpaceTime → V), Set.EqOn g f (openPast T) ∧ ContDiffOn ℝ (↑⊤) g (closedPast T) ∧ ∀ (n : ℕ) (x : Space), iteratedFDerivWithin ℝ n g (closedPast T) (T, x) = L x n

A constructive endpoint extension theorem with exact full boundary jets.