Endpoint limits from actual joint jets and local one-sided extensions

The input is an actual function, smooth on t < 1. Its full Frechet jets vanish jointly at (1,0), and it has an actual smooth local extension near each other point of the terminal slice. The boundary tensor family and its local uniform convergence are constructed below.

@[reducible, inline]

abbrev NavierStokes.JointResidualLimits.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.JointResidualLimits.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.JointResidualLimits.SpaceTime : Type

Space time: an abbreviation for ProblemStatement.SpaceTime.

Equations

• NavierStokes.JointResidualLimits.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

theorem NavierStokes.JointResidualLimits.continuous_of_joint_limits {ι : Type u_1} {X : Type u_2} {V : Type u_3} [TopologicalSpace X] [PseudoMetricSpace V] {p : Filter ι} [p.NeBot] {F : ι × X → V} {L : X → V} (hlim : ∀ (x : X), Filter.Tendsto F (p ×ˢ nhds x) (nhds (L x))) : Continuous L

Joint convergence to boundary values forces continuity of those values. No continuity or local-uniform convergence of the boundary map is assumed.

theorem NavierStokes.JointResidualLimits.locallyUniform_of_joint_limits {ι : Type u_1} {X : Type u_2} {V : Type u_3} [TopologicalSpace X] [PseudoMetricSpace V] {p : Filter ι} [p.NeBot] {F : ι × X → V} {L : X → V} (hlim : ∀ (x : X), Filter.Tendsto F (p ×ˢ nhds x) (nhds (L x))) : TendstoLocallyUniformly (fun (i : ι) (x : X) => F (i, x)) L p

Reverse joint-to-local-uniform implication, using the uniform-space characterization of local uniform convergence.

structure NavierStokes.JointResidualLimits.OneSidedExtension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) (x : Space) : Type u_1

A genuine smooth extension on a neighborhood, agreeing with the original function on the portion of that neighborhood with t < 1.

• value : SpaceTime → V

  Value of OneSidedExtension, of type SpaceTime → V.

• domain : Set SpaceTime

  Domain of OneSidedExtension, of type Set SpaceTime.

• isOpen : IsOpen self.domain
• mem : (1, x) ∈ self.domain
• smooth : ContDiffOn ℝ (↑⊤) self.value self.domain
• agrees : Set.EqOn self.value f (self.domain ∩ SpacetimeEndpoint.openPast 1)

def NavierStokes.JointResidualLimits.AwayExtensions {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) : Prop

Away extensions, given by ∀ x : Space, x ≠ 0 → Nonempty (OneSidedExtension f x).

Equations

• NavierStokes.JointResidualLimits.AwayExtensions f = ∀ (x : NavierStokes.JointResidualLimits.Space), x ≠ 0 → Nonempty (NavierStokes.JointResidualLimits.OneSidedExtension f x)

def NavierStokes.JointResidualLimits.VanishingJointJets {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) : Prop

Vanishing joint jets, given by ∀ n : ℕ, Tendsto (iteratedFDeriv ℝ n f) (𝓝[SpacetimeEndpoint.openPast 1] ((1 : ℝ), (0 : Space))) (𝓝 0).

Equations

• NavierStokes.JointResidualLimits.VanishingJointJets f = ∀ (n : ℕ), Filter.Tendsto (iteratedFDeriv ℝ n f) (nhdsWithin (1, 0) (NavierStokes.SpacetimeEndpoint.openPast 1)) (nhds 0)

theorem NavierStokes.JointResidualLimits.past_filter (x : Space) : nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1) = nhdsWithin 1 (Set.Iio 1) ×ˢ nhds x

theorem NavierStokes.JointResidualLimits.OneSidedExtension.eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} {x : Space} (e : OneSidedExtension f x) : f =ᶠ[nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)] e.value

theorem NavierStokes.JointResidualLimits.OneSidedExtension.jets_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} {x : Space} (e : OneSidedExtension f x) (n : ℕ) : iteratedFDeriv ℝ n f =ᶠ[nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)] iteratedFDeriv ℝ n e.value

Local agreement on the open past gives agreement of every actual jet.

theorem NavierStokes.JointResidualLimits.OneSidedExtension.jet_tendsto {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} {x : Space} (e : OneSidedExtension f x) (n : ℕ) : Filter.Tendsto (iteratedFDeriv ℝ n f) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds (iteratedFDeriv ℝ n e.value (1, x)))

noncomputable def NavierStokes.JointResidualLimits.boundaryLimits {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) (hext : AwayExtensions f) (x : Space) : FormalMultilinearSeries ℝ SpaceTime V

One family of tensors, selected from actual extensions away from zero. At the origin each tensor is explicitly zero.

Equations

• NavierStokes.JointResidualLimits.boundaryLimits f hext x = if hx : x = 0 then 0 else ftaylorSeries ℝ (Classical.choice ⋯).value (1, x)

@[simp]

theorem NavierStokes.JointResidualLimits.boundaryLimits_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) (hext : AwayExtensions f) (n : ℕ) : boundaryLimits f hext 0 n = 0

theorem NavierStokes.JointResidualLimits.boundaryLimits_joint {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) (x : Space) : Filter.Tendsto (iteratedFDeriv ℝ n f) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds (boundaryLimits f hext x n))

theorem NavierStokes.JointResidualLimits.boundaryLimits_continuous {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) : Continuous fun (x : Space) => boundaryLimits f hext x n

theorem NavierStokes.JointResidualLimits.boundaryLimits_locallyUniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n f (t, x)) (fun (x : ProblemStatement.Space) => boundaryLimits f hext x n) (nhdsWithin 1 (Set.Iio 1))

theorem NavierStokes.JointResidualLimits.boundaryLimits_uniformOn_compact {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) {K : Set Space} (hK : IsCompact K) : TendstoUniformlyOn (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n f (t, x)) (fun (x : ProblemStatement.Space) => boundaryLimits f hext x n) (nhdsWithin 1 (Set.Iio 1)) K

theorem NavierStokes.JointResidualLimits.past_filter_neBot (x : Space) : (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)).NeBot

theorem NavierStokes.JointResidualLimits.boundaryLimits_eq_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (hext : AwayExtensions f) {x : Space} (e : OneSidedExtension f x) (n : ℕ) : boundaryLimits f hext x n = iteratedFDeriv ℝ n e.value (1, x)

The chosen tensors agree with every actual local extension, so they do not depend on the choice used to construct the family.

theorem NavierStokes.JointResidualLimits.boundaryLimits_independent {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (h₁ h₂ : AwayExtensions f) : boundaryLimits f h₁ = boundaryLimits f h₂

theorem NavierStokes.JointResidualLimits.iteratedFDeriv_eqOn_past {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : SpaceTime → V} (h : Set.EqOn f g (SpacetimeEndpoint.openPast 1)) (n : ℕ) : Set.EqOn (iteratedFDeriv ℝ n f) (iteratedFDeriv ℝ n g) (SpacetimeEndpoint.openPast 1)

theorem NavierStokes.JointResidualLimits.boundaryLimits_eq_of_eqOn_past {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : SpaceTime → V} (hf : VanishingJointJets f) (hg : VanishingJointJets g) (ef : AwayExtensions f) (eg : AwayExtensions g) (h : Set.EqOn f g (SpacetimeEndpoint.openPast 1)) : boundaryLimits f ef = boundaryLimits g eg

Values at and after time one, including an arbitrary zero extension, do not change the boundary family when the past functions agree.

theorem NavierStokes.JointResidualLimits.actual_derivative_recurrence {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (n : ℕ) (z : SpaceTime) (hz : z.1 < 1) : HasFDerivAt (iteratedFDeriv ℝ n f) (iteratedFDeriv ℝ (n + 1) f z).curryLeft z

Actual derivative recurrence on the open past; the jet family is not independent input data.

theorem NavierStokes.JointResidualLimits.boundaryLimits_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) : ContDiff ℝ ↑⊤ fun (x : Space) => boundaryLimits f hext x n

theorem NavierStokes.JointResidualLimits.extendedJets_compatible {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) (z : SpaceTime) (hz : z ∈ SpacetimeEndpoint.closedPast 1) : HasFDerivWithinAt (fun (y : SpacetimeEndpoint.SpaceTime) => SpacetimeEndpoint.extendJets 1 (ftaylorSeries ℝ f) (boundaryLimits f hext) y n) (SpacetimeEndpoint.extendJets 1 (ftaylorSeries ℝ f) (boundaryLimits f hext) z (n + 1)).curryLeft (SpacetimeEndpoint.closedPast 1) z

theorem NavierStokes.JointResidualLimits.boundaryLimits_hasFDerivAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) (x : Space) : HasFDerivAt (fun (y : Space) => boundaryLimits f hext y n) ((boundaryLimits f hext x (n + 1)).curryLeft ∘SL ContinuousLinearMap.inr ℝ ℝ Space) x

Spatial differentiation of a boundary tensor is restriction of the next full spacetime tensor to a spatial first argument.

noncomputable def NavierStokes.JointResidualLimits.extendedResidual {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) (hext : AwayExtensions f) : SpaceTime → V

On t < 1 this is the original function; on t ≥ 1 this auxiliary closed-side extension is constant in time with the constructed boundary trace.

Equations

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

theorem NavierStokes.JointResidualLimits.extendedResidual_agrees {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) (hext : AwayExtensions f) : Set.EqOn (extendedResidual f hext) f (SpacetimeEndpoint.openPast 1)

theorem NavierStokes.JointResidualLimits.extendedResidual_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (hzero : VanishingJointJets f) (hext : AwayExtensions f) : ContDiffOn ℝ (↑⊤) (extendedResidual f hext) (SpacetimeEndpoint.closedPast 1)

theorem NavierStokes.JointResidualLimits.extendedResidual_boundary_jets {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) (x : Space) : iteratedFDerivWithin ℝ n (extendedResidual f hext) (SpacetimeEndpoint.closedPast 1) (1, x) = boundaryLimits f hext x n

theorem NavierStokes.JointResidualLimits.extendedResidual_flat_at_origin {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (hzero : VanishingJointJets f) (hext : AwayExtensions f) (n : ℕ) : iteratedFDerivWithin ℝ n (extendedResidual f hext) (SpacetimeEndpoint.closedPast 1) (1, 0) = 0

theorem NavierStokes.JointResidualLimits.extendedResidual_unit_periods {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (hext : AwayExtensions f) (hperiod : ProblemStatement.UnitSpatialPeriodsOn (Set.Iio 1) f) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (extendedResidual f hext)

theorem NavierStokes.JointResidualLimits.exists_residual_limits {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hzero : VanishingJointJets f) (hext : AwayExtensions f) : ∃ (L : Space → FormalMultilinearSeries ℝ SpaceTime V), (∀ (n : ℕ), L 0 n = 0) ∧ (∀ (n : ℕ) (x : Space), Filter.Tendsto (iteratedFDeriv ℝ n f) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds (L x n))) ∧ ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n f (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))

The limit portion of the CandidateFromLimits input is constructed solely from actual joint jet limits and one-sided local extensions.

theorem NavierStokes.JointResidualLimits.exists_smooth_compatible_limits {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f (SpacetimeEndpoint.openPast 1)) (hzero : VanishingJointJets f) (hext : AwayExtensions f) : ∃ (L : Space → FormalMultilinearSeries ℝ SpaceTime V), (∀ (n : ℕ), L 0 n = 0) ∧ (∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n f (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) ∧ (∀ (n : ℕ), ContDiff ℝ ↑⊤ fun (x : Space) => L x n) ∧ ∀ (n : ℕ) (x : Space), HasFDerivAt (fun (y : Space) => L y n) ((L x (n + 1)).curryLeft ∘SL ContinuousLinearMap.inr ℝ ℝ Space) x

Complete endpoint implication, including derived smoothness and exact compatibility of all boundary tensors.