Spatial localization through actual Cartesian potentials

The fixed cutoff is a smooth function of x₀² + x₁² and x₂. It is one on an open cylinder containing the origin and has support strictly inside a unit period cube. We multiply the potential before taking any curl, and periodize the resulting potential by the actual locally finite lattice sum. The pressure is cut and periodized as a scalar.

The conclusions concern the spatial construction and the existing time activation. No terminal residual limit is assumed or asserted here.

Spatial periodization in physical Euclidean three-space

The periodization is the actual sum over integer lattice translations. A fixed spatial support bound makes this family locally finite, uniformly in time. Consequently every smoothness order is preserved. The construction agrees with the original field on an explicit cube whenever the other translates vanish.

@[reducible, inline]

abbrev NavierStokes.PeriodicLocalization.Lattice : Type

Lattice: an abbreviation for Fin 3 → ℤ.

Equations

• NavierStokes.PeriodicLocalization.Lattice = (Fin 3 → ℤ)

def NavierStokes.PeriodicLocalization.lattice (n : Lattice) : ProblemStatement.Space

The integer lattice embedded in the Euclidean space of the PDE statement.

Equations

• NavierStokes.PeriodicLocalization.lattice n = (WithLp.equiv 2 (Fin 3 → ℝ)).symm fun (i : Fin 3) => ↑(n i)

@[simp]

theorem NavierStokes.PeriodicLocalization.lattice_apply (n : Lattice) (i : Fin 3) : (lattice n).ofLp i = ↑(n i)

@[simp]

theorem NavierStokes.PeriodicLocalization.lattice_zero : lattice 0 = 0

@[simp]

theorem NavierStokes.PeriodicLocalization.lattice_add (m n : Lattice) : lattice (m + n) = lattice m + lattice n

@[simp]

theorem NavierStokes.PeriodicLocalization.lattice_single (i : Fin 3) : lattice (Pi.single i 1) = ProblemStatement.coordinateVector i

def NavierStokes.PeriodicLocalization.SupportedInCube {V : Type u_1} [NormedAddCommGroup V] (r : ℝ) (f : ProblemStatement.SpaceTime → V) : Prop

A spatial support bound, uniform over all physical times.

Equations

• NavierStokes.PeriodicLocalization.SupportedInCube r f = ∀ (z : NavierStokes.ProblemStatement.SpaceTime), f z ≠ 0 → ∀ (i : Fin 3), |z.2.ofLp i| ≤ r

def NavierStokes.PeriodicLocalization.translate {V : Type u_1} (f : ProblemStatement.SpaceTime → V) (n : Lattice) (z : ProblemStatement.SpaceTime) : V

Translate only in space; physical time is unchanged.

Equations

• NavierStokes.PeriodicLocalization.translate f n z = f (z.1, z.2 - NavierStokes.PeriodicLocalization.lattice n)

noncomputable def NavierStokes.PeriodicLocalization.periodize {V : Type u_1} [NormedAddCommGroup V] (f : ProblemStatement.SpaceTime → V) (z : ProblemStatement.SpaceTime) : V

The actual lattice sum, rather than an assumed periodic extension.

Equations

• NavierStokes.PeriodicLocalization.periodize f z = ∑' (n : NavierStokes.PeriodicLocalization.Lattice), NavierStokes.PeriodicLocalization.translate f n z

def NavierStokes.PeriodicLocalization.latticeBox (N : ℕ) : Set Lattice

A finite box in the three-dimensional integer lattice.

Equations

• NavierStokes.PeriodicLocalization.latticeBox N = {n : NavierStokes.PeriodicLocalization.Lattice | ∀ (i : Fin 3), n i ∈ Set.Icc (-↑N) ↑N}

theorem NavierStokes.PeriodicLocalization.finite_latticeBox (N : ℕ) : (latticeBox N).Finite

noncomputable def NavierStokes.PeriodicLocalization.latticeBoxFinset (N : ℕ) : Finset Lattice

Lattice box finset, given by (finite_latticeBox N).toFinset.

Equations

• NavierStokes.PeriodicLocalization.latticeBoxFinset N = ⋯.toFinset

@[simp]

theorem NavierStokes.PeriodicLocalization.mem_latticeBoxFinset (N : ℕ) (n : Lattice) : n ∈ latticeBoxFinset N ↔ n ∈ latticeBox N

theorem NavierStokes.PeriodicLocalization.mem_latticeBox_of_translate_ne_zero {V : Type u_1} [NormedAddCommGroup V] {r R : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) {N : ℕ} (hN : R + r ≤ ↑N) {z : ProblemStatement.SpaceTime} (hz : ‖z.2‖ ≤ R) {n : Lattice} (hn : translate f n z ≠ 0) : n ∈ latticeBox N

Only a finite lattice box can contribute on a bounded spatial region.

theorem NavierStokes.PeriodicLocalization.exists_local_latticeBox {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) (z : ProblemStatement.SpaceTime) : ∃ (N : ℕ), ∀ᶠ (w : ProblemStatement.SpaceTime) in nhds z, ∀ n ∉ latticeBoxFinset N, translate f n w = 0

Near any spacetime point, every translate outside one fixed finite integer box vanishes. No restriction on nearby time coordinates is needed.

theorem NavierStokes.PeriodicLocalization.locallyFinite_support_translate {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) : LocallyFinite fun (n : Lattice) => Function.support (translate f n)

The supports of the lattice translates form a locally finite family.

theorem NavierStokes.PeriodicLocalization.summable_translate {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) (z : ProblemStatement.SpaceTime) : Summable fun (n : Lattice) => translate f n z

The series is genuinely summable at every spacetime point.

theorem NavierStokes.PeriodicLocalization.periodize_locally_eq_sum {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) (z : ProblemStatement.SpaceTime) : ∃ (N : ℕ), periodize f =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ∑ n ∈ latticeBoxFinset N, translate f n w

Locally, the infinite sum equals a single finite sum of smooth translates.

theorem NavierStokes.PeriodicLocalization.contDiff_translate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} {m : WithTop ℕ∞} (hf : ContDiff ℝ m f) (n : Lattice) : ContDiff ℝ m (translate f n)

theorem NavierStokes.PeriodicLocalization.contDiff_periodize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} {m : WithTop ℕ∞} (hs : SupportedInCube r f) (hf : ContDiff ℝ m f) : ContDiff ℝ m (periodize f)

Spatial periodization preserves every given differentiability order, in particular m = ∞, through locally finite sums.

theorem NavierStokes.PeriodicLocalization.contDiffOn_translate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} {m : WithTop ℕ∞} {times : Set ℝ} (hf : ContDiffOn ℝ m f (times ×ˢ Set.univ)) (n : Lattice) : ContDiffOn ℝ m (translate f n) (times ×ˢ Set.univ)

A translation preserves smoothness relative to any set of times.

theorem NavierStokes.PeriodicLocalization.contDiffOn_periodize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} {m : WithTop ℕ∞} {times : Set ℝ} (hs : SupportedInCube r f) (hf : ContDiffOn ℝ m f (times ×ˢ Set.univ)) : ContDiffOn ℝ m (periodize f) (times ×ˢ Set.univ)

Periodization also preserves relative smoothness at time boundaries, including the closed initial-time boundary in the PDE specification.

theorem NavierStokes.PeriodicLocalization.periodize_add_lattice {V : Type u_1} [NormedAddCommGroup V] (f : ProblemStatement.SpaceTime → V) (t : ℝ) (x : ProblemStatement.Space) (m : Lattice) : periodize f (t, x + lattice m) = periodize f (t, x)

Reindexing the actual sum gives every integer lattice period.

theorem NavierStokes.PeriodicLocalization.unitSpatialPeriodsOn_periodize {V : Type u_1} [NormedAddCommGroup V] (f : ProblemStatement.SpaceTime → V) (times : Set ℝ) : ProblemStatement.UnitSpatialPeriodsOn times (periodize f)

The periods are the exact coordinate periods in the PDE specification.

def NavierStokes.PeriodicLocalization.innerCube (r : ℝ) : Set ProblemStatement.Space

The open spatial cube on which other copies are excluded.

Equations

• NavierStokes.PeriodicLocalization.innerCube r = {x : NavierStokes.ProblemStatement.Space | ∀ (i : Fin 3), |x.ofLp i| < 1 - r}

theorem NavierStokes.PeriodicLocalization.translate_eq_zero_on_innerCube {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) {x : ProblemStatement.Space} (hx : x ∈ innerCube r) (t : ℝ) {n : Lattice} (hn : n ≠ 0) : translate f n (t, x) = 0

In this cube, a nonzero translate must be the zero lattice translate.

theorem NavierStokes.PeriodicLocalization.periodize_eq_on_innerCube {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) {x : ProblemStatement.Space} (hx : x ∈ innerCube r) (t : ℝ) : periodize f (t, x) = f (t, x)

Exact equality on an explicit open cube, uniformly over time.

theorem NavierStokes.PeriodicLocalization.isOpen_innerCube (r : ℝ) : IsOpen (innerCube r)

theorem NavierStokes.PeriodicLocalization.periodize_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ innerCube r) : periodize f =ᶠ[nhds z] f

Equality holds on a neighborhood of every point in the inner cube, so local derivatives of the periodization also agree with those of the original.

theorem NavierStokes.PeriodicLocalization.periodize_eventuallyEq_at_origin {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) (hr : r < 1 / 2) (t : ℝ) : periodize f =ᶠ[nhds (t, 0)] f

A cube strictly inside the fundamental unit cube gives equality near the spatial origin at every time.

theorem NavierStokes.PeriodicLocalization.periodize_eq_on_unitCube {V : Type u_1} [NormedAddCommGroup V] {r : ℝ} {f : ProblemStatement.SpaceTime → V} (hf : SupportedInCube r f) (hr : r < 1 / 2) {x : ProblemStatement.Space} (hx : ∀ (i : Fin 3), |x.ofLp i| ≤ 1 / 2) (t : ℝ) : periodize f (t, x) = f (t, x)

For support strictly inside the fundamental cube, equality holds on the whole closed fundamental cube, including its boundary.

theorem NavierStokes.PeriodicLocalization.periodize_eq_zero_of_timeSlice {V : Type u_1} [NormedAddCommGroup V] {f : ProblemStatement.SpaceTime → V} {t : ℝ} (hf : ∀ (x : ProblemStatement.Space), f (t, x) = 0) (x : ProblemStatement.Space) : periodize f (t, x) = 0

Spatial periodization preserves every zero time slice.

theorem NavierStokes.PeriodicLocalization.compactFutureTimeSupport_periodize {f : ProblemStatement.VelocityField} (hf : ProblemStatement.CompactFutureTimeSupport f) : ProblemStatement.CompactFutureTimeSupport (periodize f)

In particular, the common future time-support endpoint is preserved.

noncomputable def NavierStokes.SpatialLocalization.radialSquare (x : ProblemStatement.Space) : ℝ

Squared distance to the symmetry axis, with no square-root singularity.

Equations

• NavierStokes.SpatialLocalization.radialSquare x = x.ofLp 0 ^ 2 + x.ofLp 1 ^ 2

theorem NavierStokes.SpatialLocalization.radialSquare_nonneg (x : ProblemStatement.Space) : 0 ≤ radialSquare x

theorem NavierStokes.SpatialLocalization.radialSquare_contDiff : ContDiff ℝ (↑⊤) radialSquare

noncomputable def NavierStokes.SpatialLocalization.cutoffProfile (p : ℝ × ℝ) : ℝ

A globally smooth profile in squared radius and axial position.

Equations

• NavierStokes.SpatialLocalization.cutoffProfile p = NavierStokes.SmoothCutoffs.cutoff (16 * p.1) * NavierStokes.SmoothCutoffs.cutoff (4 * p.2)

theorem NavierStokes.SpatialLocalization.cutoffProfile_contDiff : ContDiff ℝ (↑⊤) cutoffProfile

noncomputable def NavierStokes.SpatialLocalization.spatialCutoff (x : ProblemStatement.Space) : ℝ

The explicit spatial cutoff used in both the potential and the pressure.

Equations

• NavierStokes.SpatialLocalization.spatialCutoff x = NavierStokes.SpatialLocalization.cutoffProfile (NavierStokes.SpatialLocalization.radialSquare x, x.ofLp 2)

theorem NavierStokes.SpatialLocalization.spatialCutoff_contDiff : ContDiff ℝ (↑⊤) spatialCutoff

theorem NavierStokes.SpatialLocalization.spatialCutoff_mem_Icc (x : ProblemStatement.Space) : spatialCutoff x ∈ Set.Icc 0 1

theorem NavierStokes.SpatialLocalization.spatialCutoff_rotation (θ : ℝ) (x : ProblemStatement.Space) : spatialCutoff ((CylindricalResidual.frame θ) x) = spatialCutoff x

Invariance under the actual Cartesian rotation about the third axis.

noncomputable def NavierStokes.SpatialLocalization.supportCylinder : Set ProblemStatement.Space

The closed support cylinder has radius 1/4 and height 1/2.

Equations

• NavierStokes.SpatialLocalization.supportCylinder = {x : NavierStokes.ProblemStatement.Space | NavierStokes.SpatialLocalization.radialSquare x ≤ 1 / 16 ∧ |x.ofLp 2| ≤ 1 / 4}

theorem NavierStokes.SpatialLocalization.isClosed_supportCylinder : IsClosed supportCylinder

theorem NavierStokes.SpatialLocalization.isCompact_supportCylinder : IsCompact supportCylinder

theorem NavierStokes.SpatialLocalization.spatialCutoff_support_subset : Function.support spatialCutoff ⊆ supportCylinder

theorem NavierStokes.SpatialLocalization.spatialCutoff_tsupport_subset : tsupport spatialCutoff ⊆ supportCylinder

theorem NavierStokes.SpatialLocalization.spatialCutoff_hasCompactSupport : HasCompactSupport spatialCutoff

theorem NavierStokes.SpatialLocalization.supportCylinder_coordinate_bound {x : ProblemStatement.Space} (hx : x ∈ supportCylinder) (i : Fin 3) : |x.ofLp i| ≤ 1 / 4

theorem NavierStokes.SpatialLocalization.spatialCutoff_strictly_inside_cube {x : ProblemStatement.Space} (hx : x ∈ tsupport spatialCutoff) (i : Fin 3) : |x.ofLp i| < 1 / 2

The support is strictly inside the centered fundamental period cube.

noncomputable def NavierStokes.SpatialLocalization.plateau : Set ProblemStatement.Space

An open cylinder on which the cutoff is identically one.

Equations

• NavierStokes.SpatialLocalization.plateau = {x : NavierStokes.ProblemStatement.Space | NavierStokes.SpatialLocalization.radialSquare x < 1 / 32 ∧ |x.ofLp 2| < 1 / 8}

theorem NavierStokes.SpatialLocalization.isOpen_plateau : IsOpen plateau

theorem NavierStokes.SpatialLocalization.zero_mem_plateau : 0 ∈ plateau

theorem NavierStokes.SpatialLocalization.spatialCutoff_eq_one {x : ProblemStatement.Space} (hx : x ∈ plateau) : spatialCutoff x = 1

theorem NavierStokes.SpatialLocalization.spatialCutoff_eventually_one {x : ProblemStatement.Space} (hx : x ∈ plateau) : spatialCutoff =ᶠ[nhds x] fun (x : ProblemStatement.Space) => 1

theorem NavierStokes.SpatialLocalization.plateau_subset_innerCube : plateau ⊆ PeriodicLocalization.innerCube (1 / 4)

noncomputable def NavierStokes.SpatialLocalization.cutPotential (A : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Multiplication of the actual Cartesian potential, before any curl.

Equations

• NavierStokes.SpatialLocalization.cutPotential A z = NavierStokes.SpatialLocalization.spatialCutoff z.2 • A z

noncomputable def NavierStokes.SpatialLocalization.cutPressure (p : ProblemStatement.PressureField) : ProblemStatement.PressureField

Cut pressure, defined pointwise by spatialCutoff z.2 * p z.

Equations

• NavierStokes.SpatialLocalization.cutPressure p z = NavierStokes.SpatialLocalization.spatialCutoff z.2 * p z

noncomputable def NavierStokes.SpatialLocalization.cutVelocity (A : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Cut velocity, given by SpatialCurl.spatialCurl (cutPotential A).

Equations

• NavierStokes.SpatialLocalization.cutVelocity A = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.SpatialLocalization.cutPotential A)

theorem NavierStokes.SpatialLocalization.cutPotential_supported (A : ProblemStatement.VelocityField) : PeriodicLocalization.SupportedInCube (1 / 4) (cutPotential A)

theorem NavierStokes.SpatialLocalization.cutPressure_supported (p : ProblemStatement.PressureField) : PeriodicLocalization.SupportedInCube (1 / 4) (cutPressure p)

theorem NavierStokes.SpatialLocalization.cutVelocity_tsupport (A : ProblemStatement.VelocityField) (t : ℝ) : (tsupport fun (x : ProblemStatement.Space) => cutVelocity A (t, x)) ⊆ supportCylinder

theorem NavierStokes.SpatialLocalization.cutVelocity_hasCompactSupport (A : ProblemStatement.VelocityField) (t : ℝ) : HasCompactSupport fun (x : ProblemStatement.Space) => cutVelocity A (t, x)

theorem NavierStokes.SpatialLocalization.cutVelocity_product_rule (A : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hA : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => A (t, y)) x) : cutVelocity A (t, x) = spatialCutoff x • SpatialCurl.spatialCurl A (t, x) + SpatialCurl.curlLinear ((fderiv ℝ spatialCutoff x).smulRight (A (t, x)))

This identity displays the entire cutoff derivative term.

noncomputable def NavierStokes.SpatialLocalization.periodicPotential (A : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

The actual lattice sum of the cut potential.

Equations

• NavierStokes.SpatialLocalization.periodicPotential A = NavierStokes.PeriodicLocalization.periodize (NavierStokes.SpatialLocalization.cutPotential A)

noncomputable def NavierStokes.SpatialLocalization.periodicVelocity (A : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Periodic velocity, given by SpatialCurl.spatialCurl (periodicPotential A).

Equations

• NavierStokes.SpatialLocalization.periodicVelocity A = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.SpatialLocalization.periodicPotential A)

noncomputable def NavierStokes.SpatialLocalization.periodicPressure (p : ProblemStatement.PressureField) : ProblemStatement.PressureField

Periodic pressure, given by PeriodicLocalization.periodize (cutPressure p).

Equations

• NavierStokes.SpatialLocalization.periodicPressure p = NavierStokes.PeriodicLocalization.periodize (NavierStokes.SpatialLocalization.cutPressure p)

theorem NavierStokes.SpatialLocalization.periodicPotential_locally_finite (A : ProblemStatement.VelocityField) : LocallyFinite fun (n : PeriodicLocalization.Lattice) => Function.support (PeriodicLocalization.translate (cutPotential A) n)

theorem NavierStokes.SpatialLocalization.periodicPressure_locally_finite (p : ProblemStatement.PressureField) : LocallyFinite fun (n : PeriodicLocalization.Lattice) => Function.support (PeriodicLocalization.translate (cutPressure p) n)

theorem NavierStokes.SpatialLocalization.periodicPotential_smoothOn {A : ProblemStatement.VelocityField} {times : Set ℝ} (hA : ContDiffOn ℝ (↑⊤) A (times ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (periodicPotential A) (times ×ˢ Set.univ)

theorem NavierStokes.SpatialLocalization.periodicVelocity_smoothOn {A : ProblemStatement.VelocityField} {times : Set ℝ} (hA : ContDiffOn ℝ (↑⊤) A (times ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (periodicVelocity A) (times ×ˢ Set.univ)

theorem NavierStokes.SpatialLocalization.periodicPressure_smoothOn {p : ProblemStatement.PressureField} {times : Set ℝ} (hp : ContDiffOn ℝ (↑⊤) p (times ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (periodicPressure p) (times ×ˢ Set.univ)

theorem NavierStokes.SpatialLocalization.periodicPotential_periodic (A : ProblemStatement.VelocityField) (times : Set ℝ) : ProblemStatement.UnitSpatialPeriodsOn times (periodicPotential A)

theorem NavierStokes.SpatialLocalization.periodicVelocity_periodic (A : ProblemStatement.VelocityField) (times : Set ℝ) : ProblemStatement.UnitSpatialPeriodsOn times (periodicVelocity A)

theorem NavierStokes.SpatialLocalization.periodicPressure_periodic (p : ProblemStatement.PressureField) (times : Set ℝ) : ProblemStatement.UnitSpatialPeriodsOn times (periodicPressure p)

theorem NavierStokes.SpatialLocalization.periodicVelocity_divergence_free {A : ProblemStatement.VelocityField} {times : Set ℝ} (hA : ContDiffOn ℝ (↑⊤) A (times ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ times) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (periodicVelocity A) t x = 0

theorem NavierStokes.SpatialLocalization.periodicVelocity_eventuallyEq_cut (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ PeriodicLocalization.innerCube (1 / 4)) : periodicVelocity A =ᶠ[nhds z] cutVelocity A

Throughout the central no-overlap cube, periodization agrees locally with the actual cut field, including its cutoff derivative terms.

theorem NavierStokes.SpatialLocalization.periodicPressure_eventuallyEq_cut (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ PeriodicLocalization.innerCube (1 / 4)) : periodicPressure p =ᶠ[nhds z] cutPressure p

theorem NavierStokes.SpatialLocalization.periodic_residual_eventuallyEq_cut (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ PeriodicLocalization.innerCube (1 / 4)) : (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (periodicVelocity A) (periodicPressure p) w.1 w.2) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (cutVelocity A) (cutPressure p) w.1 w.2

theorem NavierStokes.SpatialLocalization.periodic_fields_eq_cut_on_unitCube (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (t : ℝ) {x : ProblemStatement.Space} (hx : ∀ (i : Fin 3), |x.ofLp i| ≤ 1 / 2) : periodicVelocity A (t, x) = cutVelocity A (t, x) ∧ periodicPressure p (t, x) = cutPressure p (t, x) ∧ ProblemStatement.navierStokesResidual (periodicVelocity A) (periodicPressure p) t x = ProblemStatement.navierStokesResidual (cutVelocity A) (cutPressure p) t x

theorem NavierStokes.SpatialLocalization.cutPotential_eventuallyEq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : cutPotential A =ᶠ[nhds z] A

theorem NavierStokes.SpatialLocalization.cutPressure_eventuallyEq (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : cutPressure p =ᶠ[nhds z] p

theorem NavierStokes.SpatialLocalization.periodicPotential_eventuallyEq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : periodicPotential A =ᶠ[nhds z] A

Local equality includes all nearby physical times and all spatial directions.

theorem NavierStokes.SpatialLocalization.periodicVelocity_eventuallyEq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : periodicVelocity A =ᶠ[nhds z] SpatialCurl.spatialCurl A

theorem NavierStokes.SpatialLocalization.periodicPressure_eventuallyEq (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : periodicPressure p =ᶠ[nhds z] p

theorem NavierStokes.SpatialLocalization.periodicVelocity_eq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : periodicVelocity A z = SpatialCurl.spatialCurl A z

theorem NavierStokes.SpatialLocalization.periodicPressure_eq (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : periodicPressure p z = p z

theorem NavierStokes.SpatialLocalization.periodicVelocity_jets_eq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) (m : ℕ) : iteratedFDeriv ℝ m (periodicVelocity A) z = iteratedFDeriv ℝ m (SpatialCurl.spatialCurl A) z

theorem NavierStokes.SpatialLocalization.periodicPressure_jets_eq (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) (m : ℕ) : iteratedFDeriv ℝ m (periodicPressure p) z = iteratedFDeriv ℝ m p z

theorem NavierStokes.SpatialLocalization.periodic_residual_eventuallyEq (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (periodicVelocity A) (periodicPressure p) w.1 w.2) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A) p w.1 w.2

theorem NavierStokes.SpatialLocalization.periodic_residual_eq (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) : ProblemStatement.navierStokesResidual (periodicVelocity A) (periodicPressure p) z.1 z.2 = ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A) p z.1 z.2

theorem NavierStokes.SpatialLocalization.periodic_residual_jets_eq (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ plateau) (m : ℕ) : iteratedFDeriv ℝ m (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (periodicVelocity A) (periodicPressure p) w.1 w.2) z = iteratedFDeriv ℝ m (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A) p w.1 w.2) z

theorem NavierStokes.SpatialLocalization.periodicVelocity_origin (A : ProblemStatement.VelocityField) (t : ℝ) : periodicVelocity A (t, 0) = SpatialCurl.spatialCurl A (t, 0)

theorem NavierStokes.SpatialLocalization.periodicPressure_origin (p : ProblemStatement.PressureField) (t : ℝ) : periodicPressure p (t, 0) = p (t, 0)

theorem NavierStokes.SpatialLocalization.periodicVelocity_origin_blowup (A : ProblemStatement.VelocityField) (hA : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖periodicVelocity A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

noncomputable def NavierStokes.SpatialLocalization.localizedVelocity (A : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

The previously constructed time switch is applied to the spatially localized fields. It is independent of the spatial variables.

Equations

• NavierStokes.SpatialLocalization.localizedVelocity A = NavierStokes.TimeLocalization.activatedVelocity (NavierStokes.SpatialLocalization.periodicVelocity A)

noncomputable def NavierStokes.SpatialLocalization.localizedPressure (p : ProblemStatement.PressureField) : ProblemStatement.PressureField

Localized pressure, given by TimeLocalization.activatedPressure (periodicPressure p).

Equations

• NavierStokes.SpatialLocalization.localizedPressure p = NavierStokes.TimeLocalization.activatedPressure (NavierStokes.SpatialLocalization.periodicPressure p)

noncomputable def NavierStokes.SpatialLocalization.localizedPotential (A : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

The same time activation can be performed on the actual potential.

Equations

• NavierStokes.SpatialLocalization.localizedPotential A = NavierStokes.TimeLocalization.activatedVelocity (NavierStokes.SpatialLocalization.periodicPotential A)

theorem NavierStokes.SpatialLocalization.localizedPotential_smoothOn {A : ProblemStatement.VelocityField} {times : Set ℝ} (hA : ContDiffOn ℝ (↑⊤) A (times ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (localizedPotential A) (times ×ˢ Set.univ)

theorem NavierStokes.SpatialLocalization.localizedVelocity_eq_curl {A : ProblemStatement.VelocityField} {times : Set ℝ} (hA : ContDiffOn ℝ (↑⊤) A (times ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ times) (x : ProblemStatement.Space) : localizedVelocity A (t, x) = SpatialCurl.spatialCurl (localizedPotential A) (t, x)

theorem NavierStokes.SpatialLocalization.localizedVelocity_smooth {A : ProblemStatement.VelocityField} (hA : ContDiffOn ℝ (↑⊤) A ProblemStatement.preSingularDomain) : ContDiffOn ℝ (↑⊤) (localizedVelocity A) ProblemStatement.preSingularDomain

theorem NavierStokes.SpatialLocalization.localizedPressure_smooth {p : ProblemStatement.PressureField} (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) : ContDiffOn ℝ (↑⊤) (localizedPressure p) ProblemStatement.preSingularDomain

theorem NavierStokes.SpatialLocalization.localizedVelocity_smooth_before {A : ProblemStatement.VelocityField} (hA : ContDiffOn ℝ (↑⊤) A (Set.Iio 1 ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (localizedVelocity A) ProblemStatement.preSingularDomain

theorem NavierStokes.SpatialLocalization.localizedPressure_smooth_before {p : ProblemStatement.PressureField} (hp : ContDiffOn ℝ (↑⊤) p (Set.Iio 1 ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (localizedPressure p) ProblemStatement.preSingularDomain

theorem NavierStokes.SpatialLocalization.localizedVelocity_periodic (A : ProblemStatement.VelocityField) (times : Set ℝ) : ProblemStatement.UnitSpatialPeriodsOn times (localizedVelocity A)

theorem NavierStokes.SpatialLocalization.localizedPressure_periodic (p : ProblemStatement.PressureField) (times : Set ℝ) : ProblemStatement.UnitSpatialPeriodsOn times (localizedPressure p)

theorem NavierStokes.SpatialLocalization.localizedVelocity_zero_initial (A : ProblemStatement.VelocityField) (x : ProblemStatement.Space) : localizedVelocity A (0, x) = 0

theorem NavierStokes.SpatialLocalization.localizedPressure_zero_initial (p : ProblemStatement.PressureField) (x : ProblemStatement.Space) : localizedPressure p (0, x) = 0

theorem NavierStokes.SpatialLocalization.localizedVelocity_zero_early (A : ProblemStatement.VelocityField) {t : ℝ} (ht : |t| ≤ 3 / 8) (x : ProblemStatement.Space) : localizedVelocity A (t, x) = 0

theorem NavierStokes.SpatialLocalization.localizedPressure_zero_early (p : ProblemStatement.PressureField) {t : ℝ} (ht : |t| ≤ 3 / 8) (x : ProblemStatement.Space) : localizedPressure p (t, x) = 0

theorem NavierStokes.SpatialLocalization.localizedVelocity_divergence_free {A : ProblemStatement.VelocityField} (hA : ContDiffOn ℝ (↑⊤) A ProblemStatement.preSingularDomain) (t : ℝ) : t ∈ Set.Ico 0 1 → ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (localizedVelocity A) t x = 0

theorem NavierStokes.SpatialLocalization.localizedVelocity_eventuallyEq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) : localizedVelocity A =ᶠ[nhds z] SpatialCurl.spatialCurl A

theorem NavierStokes.SpatialLocalization.localizedPressure_eventuallyEq (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) : localizedPressure p =ᶠ[nhds z] p

theorem NavierStokes.SpatialLocalization.localizedVelocity_eq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 ≤ z.1) (hz : z.2 ∈ plateau) : localizedVelocity A z = SpatialCurl.spatialCurl A z

theorem NavierStokes.SpatialLocalization.localizedPressure_eq (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 ≤ z.1) (hz : z.2 ∈ plateau) : localizedPressure p z = p z

theorem NavierStokes.SpatialLocalization.localized_residual_eventuallyEq (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) : (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (localizedVelocity A) (localizedPressure p) w.1 w.2) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A) p w.1 w.2

theorem NavierStokes.SpatialLocalization.localized_residual_eq (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) : ProblemStatement.navierStokesResidual (localizedVelocity A) (localizedPressure p) z.1 z.2 = ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A) p z.1 z.2

theorem NavierStokes.SpatialLocalization.localized_residual_of_potential_germ (A u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) (hAu : SpatialCurl.spatialCurl A =ᶠ[nhds z] u) : (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (localizedVelocity A) (localizedPressure p) w.1 w.2) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p w.1 w.2

An existing physical potential representation can be supplied as a local identity. No additional regularity is needed to transfer the residual germ.

theorem NavierStokes.SpatialLocalization.localizedVelocity_jets_eq (A : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) (m : ℕ) : iteratedFDeriv ℝ m (localizedVelocity A) z = iteratedFDeriv ℝ m (SpatialCurl.spatialCurl A) z

theorem NavierStokes.SpatialLocalization.localizedPressure_jets_eq (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) (m : ℕ) : iteratedFDeriv ℝ m (localizedPressure p) z = iteratedFDeriv ℝ m p z

theorem NavierStokes.SpatialLocalization.localized_residual_jets_eq (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : 3 / 4 < z.1) (hz : z.2 ∈ plateau) (m : ℕ) : iteratedFDeriv ℝ m (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (localizedVelocity A) (localizedPressure p) w.1 w.2) z = iteratedFDeriv ℝ m (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A) p w.1 w.2) z

theorem NavierStokes.SpatialLocalization.localizedVelocity_origin (A : ProblemStatement.VelocityField) {t : ℝ} (ht : 3 / 4 ≤ t) : localizedVelocity A (t, 0) = SpatialCurl.spatialCurl A (t, 0)

theorem NavierStokes.SpatialLocalization.localizedVelocity_origin_blowup (A : ProblemStatement.VelocityField) (hA : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖localizedVelocity A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.SpatialLocalization.localizedVelocity_speed_unbounded (A : ProblemStatement.VelocityField) (hA : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ProblemStatement.SpeedUnboundedAtOne (localizedVelocity A)

theorem NavierStokes.SpatialLocalization.localization_properties (A : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hA : ContDiffOn ℝ (↑⊤) A (Set.Iio 1 ×ˢ Set.univ)) (hp : ContDiffOn ℝ (↑⊤) p (Set.Iio 1 ×ˢ Set.univ)) (haxis : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ContDiffOn ℝ (↑⊤) (localizedVelocity A) ProblemStatement.preSingularDomain ∧ ContDiffOn ℝ (↑⊤) (localizedPressure p) ProblemStatement.preSingularDomain ∧ ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) (localizedVelocity A) ∧ ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) (localizedPressure p) ∧ (∀ (x : ProblemStatement.Space), localizedVelocity A (0, x) = 0) ∧ (∀ t ∈ Set.Ico 0 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (localizedVelocity A) t x = 0) ∧ ProblemStatement.SpeedUnboundedAtOne (localizedVelocity A) ∧ ∀ (z : ProblemStatement.SpaceTime), 3 / 4 < z.1 → z.2 ∈ plateau → localizedVelocity A z = SpatialCurl.spatialCurl A z ∧ localizedPressure p z = p z ∧ ProblemStatement.navierStokesResidual (localizedVelocity A) (localizedPressure p) z.1 z.2 = ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A) p z.1 z.2

The actual constructed pair, including its initial data and genuine local Navier--Stokes residual equality. The only blowup input is at the origin of the original curl field; no localization or residual-output estimate is assumed.