Actual residual limits after spatial localization and periodization

The inputs concern the original potential and pressure: smoothness in the open past, actual local one-sided extensions off the origin, and joint vanishing of the actual residual jets at the origin. The boundary tensors of the periodized residual are constructed, including at every nonzero lattice copy of the origin. No residual identity or residual limit after periodization is assumed.

noncomputable def NavierStokes.PeriodicResidualLimits.originalResidual (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : ProblemStatement.VelocityField

The residual of the original, actual spatial curl.

Equations

• NavierStokes.PeriodicResidualLimits.originalResidual A p z = NavierStokes.ProblemStatement.navierStokesResidual (NavierStokes.SpatialCurl.spatialCurl A) p z.1 z.2

noncomputable def NavierStokes.PeriodicResidualLimits.cutResidual (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : ProblemStatement.VelocityField

The residual after cutting the potential, including all cutoff terms.

Equations

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

noncomputable def NavierStokes.PeriodicResidualLimits.periodicResidual (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : ProblemStatement.VelocityField

The residual of the actual lattice-periodized potential and pressure.

Equations

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

theorem NavierStokes.PeriodicResidualLimits.cutResidual_smoothOn {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) A U) (hp : ContDiffOn ℝ (↑⊤) p U) : ContDiffOn ℝ (↑⊤) (cutResidual A p) U

theorem NavierStokes.PeriodicResidualLimits.cutResidual_eventuallyEq {A B : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {z : ProblemStatement.SpaceTime} (hA : A =ᶠ[nhds z] B) (hp : p =ᶠ[nhds z] q) : cutResidual A p =ᶠ[nhds z] cutResidual B q

noncomputable def NavierStokes.PeriodicResidualLimits.cutResidualExtension {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {x : ProblemStatement.Space} (eA : JointResidualLimits.OneSidedExtension A x) (ep : JointResidualLimits.OneSidedExtension p x) : JointResidualLimits.OneSidedExtension (cutResidual A p) x

Cutoff and actual differentiation turn extensions of the two inputs into a local extension of their full nonlinear residual.

Equations

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

theorem NavierStokes.PeriodicResidualLimits.cutResidual_awayExtensions {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : JointResidualLimits.AwayExtensions A) (hp : JointResidualLimits.AwayExtensions p) : JointResidualLimits.AwayExtensions (cutResidual A p)

theorem NavierStokes.PeriodicResidualLimits.cutResidual_eventuallyEq_original (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ SpatialLocalization.plateau) : cutResidual A p =ᶠ[nhds z] originalResidual A p

theorem NavierStokes.PeriodicResidualLimits.cutResidual_vanishingJointJets {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) : JointResidualLimits.VanishingJointJets (cutResidual A p)

All cutoff-residual jets have the original joint zero limit because the cutoff is identically one on an actual neighborhood of the origin.

Exact translation and disjoint-support identities

theorem NavierStokes.PeriodicResidualLimits.periodicResidual_periodic (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (periodicResidual A p)

theorem NavierStokes.PeriodicResidualLimits.periodicResidual_jet_periodic (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (n : ℕ) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (iteratedFDeriv ℝ n (periodicResidual A p))

theorem NavierStokes.PeriodicResidualLimits.periodicResidual_jet_integerShift (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (n : ℕ) (k : Fin 3 → ℤ) (t : ℝ) (x : ProblemStatement.Space) : iteratedFDeriv ℝ n (periodicResidual A p) (t, x + CompactForceDecay.integerShift k) = iteratedFDeriv ℝ n (periodicResidual A p) (t, x)

theorem NavierStokes.PeriodicResidualLimits.periodicResidual_jet_sub_integerShift (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (n : ℕ) (k : Fin 3 → ℤ) (t : ℝ) (x : ProblemStatement.Space) : iteratedFDeriv ℝ n (periodicResidual A p) (t, x - CompactForceDecay.integerShift k) = iteratedFDeriv ℝ n (periodicResidual A p) (t, x)

theorem NavierStokes.PeriodicResidualLimits.periodicResidual_jets_eq_cut (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ PeriodicLocalization.innerCube (1 / 4)) (n : ℕ) : iteratedFDeriv ℝ n (periodicResidual A p) z = iteratedFDeriv ℝ n (cutResidual A p) z

This equality uses the no-overlap support theorem for the actual periodized potential and pressure before differentiating the residual.

noncomputable def NavierStokes.PeriodicResidualLimits.nearestIndex (x : ProblemStatement.Space) : Fin 3 → ℤ

A chosen fundamental-cube representative; its discontinuities will not be assumed to preserve continuity of the constructed boundary tensors.

Equations

• NavierStokes.PeriodicResidualLimits.nearestIndex x i = round (x.ofLp i)

noncomputable def NavierStokes.PeriodicResidualLimits.representative (x : ProblemStatement.Space) : ProblemStatement.Space

Representative, given by x - CompactForceDecay.integerShift (nearestIndex x).

Equations

• NavierStokes.PeriodicResidualLimits.representative x = x - NavierStokes.CompactForceDecay.integerShift (NavierStokes.PeriodicResidualLimits.nearestIndex x)

theorem NavierStokes.PeriodicResidualLimits.representative_mem_innerCube (x : ProblemStatement.Space) : representative x ∈ PeriodicLocalization.innerCube (1 / 4)

@[simp]

theorem NavierStokes.PeriodicResidualLimits.representative_zero : representative 0 = 0

theorem NavierStokes.PeriodicResidualLimits.spatial_sub_tendsto_past (a x : ProblemStatement.Space) : Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => (z.1, z.2 - a)) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhdsWithin (1, x - a) (SpacetimeEndpoint.openPast 1))

theorem NavierStokes.PeriodicResidualLimits.periodicResidual_jets_locally_cut (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (x : ProblemStatement.Space) (n : ℕ) : iteratedFDeriv ℝ n (periodicResidual A p) =ᶠ[nhds (1, x)] fun (z : ℝ × ProblemStatement.Space) => iteratedFDeriv ℝ n (cutResidual A p) (z.1, z.2 - CompactForceDecay.integerShift (nearestIndex x))

Near any point, every jet is exactly a translated cutoff-residual jet. In particular this handles a whole neighborhood of each nonzero lattice copy.

The constructed boundary series

noncomputable def NavierStokes.PeriodicResidualLimits.boundaryLimits (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (x : ProblemStatement.Space) : FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space

Boundary limits, given by JointResidualLimits.boundaryLimits (cutResidual A p) (cutResidual_awayExtensions eA ep) (representative x).

Equations

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

@[simp]

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_zero (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) : boundaryLimits A p eA ep 0 n = 0

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_joint {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) (x : ProblemStatement.Space) : Filter.Tendsto (iteratedFDeriv ℝ n (periodicResidual A p)) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds (boundaryLimits A p eA ep x n))

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_continuous {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) : Continuous fun (x : ProblemStatement.Space) => boundaryLimits A p eA ep x n

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_locallyUniform {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (periodicResidual A p) (t, x)) (fun (x : ProblemStatement.Space) => boundaryLimits A p eA ep x n) (nhdsWithin 1 (Set.Iio 1))

The locally uniform limits are a conclusion of joint convergence; neither uniform convergence nor continuity of the chosen representatives is input.

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_uniformOn_compact {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) {K : Set ProblemStatement.Space} (hK : IsCompact K) : TendstoUniformlyOn (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (periodicResidual A p) (t, x)) (fun (x : ProblemStatement.Space) => boundaryLimits A p eA ep x n) (nhdsWithin 1 (Set.Iio 1)) K

@[simp]

theorem NavierStokes.PeriodicResidualLimits.representative_integerShift (k : Fin 3 → ℤ) : representative (CompactForceDecay.integerShift k) = 0

theorem NavierStokes.PeriodicResidualLimits.integerShift_eq_lattice (k : PeriodicLocalization.Lattice) : CompactForceDecay.integerShift k = PeriodicLocalization.lattice k

@[simp]

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_lattice (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (k : PeriodicLocalization.Lattice) (n : ℕ) : boundaryLimits A p eA ep (PeriodicLocalization.lattice k) n = 0

Every lattice copy of the distinguished origin has the same zero jets.

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_independent {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA eA' : JointResidualLimits.AwayExtensions A) (ep ep' : JointResidualLimits.AwayExtensions p) : boundaryLimits A p eA ep = boundaryLimits A p eA' ep'

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_add_integerShift {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (k : Fin 3 → ℤ) (n : ℕ) (x : ProblemStatement.Space) : boundaryLimits A p eA ep (x + CompactForceDecay.integerShift k) n = boundaryLimits A p eA ep x n

theorem NavierStokes.PeriodicResidualLimits.periodicResidual_smooth {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) : ContDiffOn ℝ (↑⊤) (periodicResidual A p) (SpacetimeEndpoint.openPast 1)

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_smooth {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => boundaryLimits A p eA ep x n

theorem NavierStokes.PeriodicResidualLimits.extendedJets_compatible {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) (z : ProblemStatement.SpaceTime) (h : z ∈ SpacetimeEndpoint.closedPast 1) : HasFDerivWithinAt (fun (y : SpacetimeEndpoint.SpaceTime) => SpacetimeEndpoint.extendJets 1 (ftaylorSeries ℝ (periodicResidual A p)) (boundaryLimits A p eA ep) y n) (SpacetimeEndpoint.extendJets 1 (ftaylorSeries ℝ (periodicResidual A p)) (boundaryLimits A p eA ep) z (n + 1)).curryLeft (SpacetimeEndpoint.closedPast 1) z

theorem NavierStokes.PeriodicResidualLimits.boundaryLimits_hasFDerivAt {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) (x : ProblemStatement.Space) : HasFDerivAt (fun (y : ProblemStatement.Space) => boundaryLimits A p eA ep y n) ((boundaryLimits A p eA ep x (n + 1)).curryLeft ∘SL ContinuousLinearMap.inr ℝ ℝ ProblemStatement.Space) x

noncomputable def NavierStokes.PeriodicResidualLimits.extendedResidual (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) : ProblemStatement.VelocityField

Fill the terminal trace with the derived tensors. Only relative smoothness on the closed past is asserted for this auxiliary extension.

Equations

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

theorem NavierStokes.PeriodicResidualLimits.extendedResidual_agrees (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) : Set.EqOn (extendedResidual A p eA ep) (periodicResidual A p) (SpacetimeEndpoint.openPast 1)

theorem NavierStokes.PeriodicResidualLimits.extendedResidual_smooth {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) : ContDiffOn ℝ (↑⊤) (extendedResidual A p eA ep) (SpacetimeEndpoint.closedPast 1)

theorem NavierStokes.PeriodicResidualLimits.extendedResidual_boundary_jets {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) (x : ProblemStatement.Space) : iteratedFDerivWithin ℝ n (extendedResidual A p eA ep) (SpacetimeEndpoint.closedPast 1) (1, x) = boundaryLimits A p eA ep x n

theorem NavierStokes.PeriodicResidualLimits.localizedResidual_joint {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) (x : ProblemStatement.Space) : Filter.Tendsto (iteratedFDeriv ℝ n fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual (SpatialLocalization.localizedVelocity A) (SpatialLocalization.localizedPressure p) z.1 z.2) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds (boundaryLimits A p eA ep x n))

Time activation preserves these same limits at every spatial point.

theorem NavierStokes.PeriodicResidualLimits.localizedResidual_locallyUniform {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (n : ℕ) : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual (SpatialLocalization.localizedVelocity A) (SpatialLocalization.localizedPressure p) z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => boundaryLimits A p eA ep x n) (nhdsWithin 1 (Set.Iio 1))

theorem NavierStokes.PeriodicResidualLimits.exists_residual_limits {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) : ∃ (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space), (∀ (k : PeriodicLocalization.Lattice) (n : ℕ), L (PeriodicLocalization.lattice k) n = 0) ∧ ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (periodicResidual A p) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))

The entire family required by CandidateFromLimits is now derived from the original input fields and their local analytic data.

Direct candidate bridge with only original local analytic inputs

theorem NavierStokes.PeriodicResidualLimits.periodicVelocity_speed_unbounded {A : ProblemStatement.VelocityField} (haxis : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ProblemStatement.SpeedUnboundedAtOne (SpatialLocalization.periodicVelocity A)

theorem NavierStokes.PeriodicResidualLimits.exists_candidate_force {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (haxis : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ∃ (F : ProblemStatement.VelocityField), ProblemStatement.CandidateProperties (SpatialLocalization.localizedVelocity A) (SpatialLocalization.localizedPressure p) F ∧ ContDiff ℝ (↑⊤) F ∧ ∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDeriv ℝ n F (1, x) = boundaryLimits A p eA ep x n

A conditional candidate for the actual localized fields. No periodic residual estimates, force, boundary tensors, or divergence assumption are inputs. The potential extension input is essential and is not inferred from velocity regularity.

theorem NavierStokes.PeriodicResidualLimits.candidateStatement_of_potential_data {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A p)) (eA : JointResidualLimits.AwayExtensions A) (ep : JointResidualLimits.AwayExtensions p) (haxis : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ProblemStatement.candidateStatement