Joint smooth gluing from matching normal time jets

Normal derivatives below are actual directional derivatives of joint fields. The final interface uses the actual one-sided iteratedDerivWithin of time slices. Equality of full mixed derivative tensors is not an input assumption.

@[reducible, inline]

abbrev NavierStokes.SpacetimeGluing.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.SpacetimeGluing.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.SpacetimeGluing.SpaceTime : Type

Space time: an abbreviation for ProblemStatement.SpaceTime.

Equations

• NavierStokes.SpacetimeGluing.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

noncomputable def NavierStokes.SpacetimeGluing.timeVector : SpaceTime

Time vector, given by (1, 0).

Equations

• NavierStokes.SpacetimeGluing.timeVector = (1, 0)

noncomputable def NavierStokes.SpacetimeGluing.directional {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set SpaceTime) (f : SpaceTime → V) (v z : SpaceTime) : V

Directional, given by fderivWithin ℝ f s z v.

Equations

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

noncomputable def NavierStokes.SpacetimeGluing.normalIter {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : Set SpaceTime) (f : SpaceTime → V) : ℕ → SpaceTime → V

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

Equations

• NavierStokes.SpacetimeGluing.normalIter s f 0 = f
• NavierStokes.SpacetimeGluing.normalIter s f n.succ = NavierStokes.SpacetimeGluing.directional s (NavierStokes.SpacetimeGluing.normalIter s f n) NavierStokes.SpacetimeGluing.timeVector

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

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

theorem NavierStokes.SpacetimeGluing.directional_commute {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set SpaceTime} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f s) (hs : UniqueDiffOn ℝ s) (hregular : s ⊆ closure (interior s)) {z : SpaceTime} (hz : z ∈ s) (v w : SpaceTime) : 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.SpacetimeGluing.normalIter_directional {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set SpaceTime} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f s) (hs : UniqueDiffOn ℝ s) (hregular : s ⊆ closure (interior s)) (v : SpaceTime) (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.SpacetimeGluing.time_slice_iteratedDerivWithin {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {I : Set ℝ} {f : SpaceTime → V} (hI : UniqueDiffOn ℝ I) (hf : ContDiffOn ℝ (↑⊤) f (I ×ˢ Set.univ)) (x : Space) (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.SpacetimeGluing.boundary_fderiv_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s t : Set SpaceTime} {f g : SpaceTime → V} {T : ℝ} (hf : ContDiffOn ℝ (↑⊤) f s) (hg : ContDiffOn ℝ (↑⊤) g t) (hBs : ∀ (x : Space), (T, x) ∈ s) (hBt : ∀ (x : Space), (T, x) ∈ t) (hvalue : ∀ (x : Space), f (T, x) = g (T, x)) (hnormal : ∀ (x : Space), directional s f timeVector (T, x) = directional t g timeVector (T, x)) (x : Space) : 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.SpacetimeGluing.normal_match_directional {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s t : Set SpaceTime} {f g : SpaceTime → 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 : Space), (T, x) ∈ s) (hBt : ∀ (x : Space), (T, x) ∈ t) (hmatch : ∀ (n : ℕ) (x : Space), normalIter s f n (T, x) = normalIter t g n (T, x)) (v : SpaceTime) (n : ℕ) (x : Space) : 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.

@[reducible, inline]

abbrev NavierStokes.SpacetimeGluing.past (T : ℝ) : Set SpaceTime

Past: an abbreviation for SpacetimeEndpoint.closedPast T.

Equations

• NavierStokes.SpacetimeGluing.past T = NavierStokes.SpacetimeEndpoint.closedPast T

def NavierStokes.SpacetimeGluing.future (T : ℝ) : Set SpaceTime

Future, given by Ici T ×ˢ univ.

Equations

• NavierStokes.SpacetimeGluing.future T = Set.Ici T ×ˢ Set.univ

theorem NavierStokes.SpacetimeGluing.past_uniqueDiff (T : ℝ) : UniqueDiffOn ℝ (past T)

theorem NavierStokes.SpacetimeGluing.future_uniqueDiff (T : ℝ) : UniqueDiffOn ℝ (future T)

theorem NavierStokes.SpacetimeGluing.past_regular (T : ℝ) : past T ⊆ closure (interior (past T))

theorem NavierStokes.SpacetimeGluing.future_regular (T : ℝ) : future T ⊆ closure (interior (future T))

theorem NavierStokes.SpacetimeGluing.past_union_future (T : ℝ) : past T ∪ future T = Set.univ

noncomputable def NavierStokes.SpacetimeGluing.glue {W : Type u_2} (T : ℝ) (f g : SpaceTime → W) (z : SpaceTime) : W

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

Equations

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

theorem NavierStokes.SpacetimeGluing.glue_eqOn_past {W : Type u_2} (T : ℝ) (f g : SpaceTime → W) : Set.EqOn (glue T f g) f (past T)

theorem NavierStokes.SpacetimeGluing.glue_eqOn_future {W : Type u_2} {T : ℝ} {f g : SpaceTime → W} (hvalue : ∀ (x : Space), f (T, x) = g (T, x)) : Set.EqOn (glue T f g) g (future T)

theorem NavierStokes.SpacetimeGluing.hasFDerivAt_glue {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : SpaceTime → V} {df dg : SpaceTime → SpaceTime →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 : Space), f (T, x) = g (T, x)) (hderiv : ∀ (x : Space), df (T, x) = dg (T, x)) (z : SpaceTime) : HasFDerivAt (glue T f g) (glue T df dg z) z

Actual full Frechet derivatives glue when their boundary values match.

theorem NavierStokes.SpacetimeGluing.hasFDerivAt_glue_of_normal {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (hg : ContDiffOn ℝ (↑⊤) g (future T)) (hvalue : ∀ (x : Space), f (T, x) = g (T, x)) (hnormal : ∀ (x : Space), directional (past T) f timeVector (T, x) = directional (future T) g timeVector (T, x)) (z : SpaceTime) : 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.SpacetimeGluing.contDiff_glue_finite {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (hg : ContDiffOn ℝ (↑⊤) g (future T)) (hmatch : ∀ (n : ℕ) (x : Space), 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.SpacetimeGluing.contDiff_glue {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f g : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (hg : ContDiffOn ℝ (↑⊤) g (future T)) (hmatch : ∀ (n : ℕ) (x : Space), 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.SpacetimeGluing.normalTrace {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (f : SpaceTime → V) (n : ℕ) (x : Space) : V

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

Equations

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

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

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

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

noncomputable def NavierStokes.SpacetimeGluing.smoothExtension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (f : SpaceTime → V) (hf : ContDiffOn ℝ (↑⊤) f (past T)) : SpaceTime → 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.SpacetimeGluing.smoothExtension_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {T : ℝ} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) : ContDiff ℝ (↑⊤) (smoothExtension T f hf)

theorem NavierStokes.SpacetimeGluing.smoothExtension_eqOn_past {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) : Set.EqOn (smoothExtension T f hf) f (past T)

theorem NavierStokes.SpacetimeGluing.smoothExtension_zero_from {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) {t : ℝ} (ht : T + 1 ≤ t) (x : Space) : smoothExtension T f hf (t, x) = 0

theorem NavierStokes.SpacetimeGluing.smoothExtension_iteratedFDeriv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {T : ℝ} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (n : ℕ) {z : SpaceTime} (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.SpacetimeGluing.smoothExtension_add_period {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (p : Space) (hperiod : ∀ t ≤ T, ∀ (x : Space), f (t, x + p) = f (t, x)) (t : ℝ) (x : Space) : smoothExtension T f hf (t, x + p) = smoothExtension T f hf (t, x)

theorem NavierStokes.SpacetimeGluing.smoothExtension_unit_periods {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (past T)) (hperiod : ProblemStatement.UnitSpatialPeriodsOn (Set.Iic T) f) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (smoothExtension T f hf)

theorem NavierStokes.SpacetimeGluing.exists_smooth_periodic_extension_of_limits {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace 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))) (hperiod : ProblemStatement.UnitSpatialPeriodsOn (Set.Iio T) f) : ∃ (F : SpaceTime → V), ContDiff ℝ (↑⊤) F ∧ Set.EqOn F f (SpacetimeEndpoint.openPast T) ∧ ProblemStatement.UnitSpatialPeriodsOn Set.univ F ∧ (∀ (t : ℝ), T + 1 ≤ t → ∀ (x : Space), F (t, x) = 0) ∧ ∀ (n : ℕ) (x : Space), iteratedFDeriv ℝ n F (T, x) = L x n

A complete constructive endpoint theorem for periodic spacetime fields. The inputs are derivative recurrence and locally uniform left limits, not closed-side or global smoothness. The resulting extension is jointly smooth, retains every mixed boundary jet, and vanishes after T + 1.