The compact whole-space fields behind the periodic construction

Keep the cut potential, direct field, and pressure before periodization. They agree locally with the periodic fields on the inner cube, and vanish outside the fixed support cylinder. A second, larger cutoff applied to the already extended smooth force gives a force on ℝ³ with compact spatial support. Locality of the derivatives proves the exact equation.

This construction makes no uniqueness assertion about comparison solutions.

Space-time decay from compact spatial and future time support

Unlike the periodic force bound, these estimates use one compact subset of Euclidean space. They bound the full one-sided space-time derivative tensors, including time zero, and allow every real decay exponent.

def NavierStokes.CompactSpatialForceDecay.SupportedIn (K : Set ProblemStatement.Space) (f : ProblemStatement.VelocityField) : Prop

A single spatial support set works at every physical time.

Equations

• NavierStokes.CompactSpatialForceDecay.SupportedIn K f = ∀ (t : ℝ), 0 ≤ t → ∀ x ∉ K, f (t, x) = 0

theorem NavierStokes.CompactSpatialForceDecay.jet_zero_outside {K : Set ProblemStatement.Space} (hK : IsClosed K) {f : ProblemStatement.VelocityField} (hf : SupportedIn K f) (m : ℕ) {t : ℝ} (ht : 0 ≤ t) {x : ProblemStatement.Space} (hx : x ∉ K) : iteratedFDerivWithin ℝ m f ProblemStatement.futureDomain (t, x) = 0

theorem NavierStokes.CompactSpatialForceDecay.jet_zero_after {f : ProblemStatement.VelocityField} {T : ℝ} (hf : ∀ (t : ℝ), T ≤ t → ∀ (x : ProblemStatement.Space), f (t, x) = 0) (m : ℕ) {t : ℝ} (ht : T < t) (x : ProblemStatement.Space) : iteratedFDerivWithin ℝ m f ProblemStatement.futureDomain (t, x) = 0

theorem NavierStokes.CompactSpatialForceDecay.jet_decay {S : Set ProblemStatement.Space} (hS : IsCompact S) {f : ProblemStatement.VelocityField} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) (hs : SupportedIn S f) (htime : ProblemStatement.CompactFutureTimeSupport f) (m : ℕ) (K : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ‖iteratedFDerivWithin ℝ m f ProblemStatement.futureDomain (t, x)‖ ≤ C / (1 + ‖x‖ + t) ^ K

Compactness bounds the weighted jet itself, so no restriction on K is needed.

theorem NavierStokes.CompactSpatialForceDecay.rescale_supported {S : Set ProblemStatement.Space} {f : ProblemStatement.VelocityField} (hf : SupportedIn S f) (a : ℝ) {c : ℝ} (hc : 0 ≤ c) : SupportedIn S (ComparatorBridge.rescale a c f)

theorem NavierStokes.CompactSpatialForceDecay.forceConditionDecay {S : Set ProblemStatement.Space} (hS : IsCompact S) {f : ProblemStatement.VelocityField} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) (hs : SupportedIn S f) (htime : ProblemStatement.CompactFutureTimeSupport f) : Comparator.ForceConditionDecay (ComparatorBridge.toComparator f)

structure NavierStokes.R3CompactCandidate.Properties (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (f : ProblemStatement.VelocityField) : Prop

The whole-space candidate conditions needed for option (C).

• velocity_smooth : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain
• pressure_smooth : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain
• force_smooth : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain
• velocity_support : ∃ (K : Set ProblemStatement.Space), IsCompact K ∧ ∀ t ∈ Set.Ico 0 1, ∀ x ∉ K, u (t, x) = 0
• pressure_support : ∃ (K : Set ProblemStatement.Space), IsCompact K ∧ ∀ t ∈ Set.Ico 0 1, ∀ x ∉ K, p (t, x) = 0
• force_support : ∃ (K : Set ProblemStatement.Space), IsCompact K ∧ CompactSpatialForceDecay.SupportedIn K f
• zero_initial_velocity (x : ProblemStatement.Space) : u (0, x) = 0
• force_time_support : ProblemStatement.CompactFutureTimeSupport f
• divergence_free (t : ℝ) : t ∈ Set.Ico 0 1 → ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0
• navier_stokes (t : ℝ) : t ∈ Set.Ioo 0 1 → ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual u p t x = f (t, x)
• speed_unbounded : ProblemStatement.SpeedUnboundedAtOne u

theorem NavierStokes.R3CompactCandidate.Properties.toSolutionOn {u f : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (candidate : Properties u p f) : SolutionOn 1 0 (fun (x : ProblemStatement.Space) => 0) (Set.Ico 0 1) f u p

Forget compact support and blow-up to retain the common local solution contract.

noncomputable def NavierStokes.R3CompactCandidate.outerCutoff (x : ProblemStatement.Space) : ℝ

Outer cutoff, given by spatialCutoff ((1 / 2 : ℝ) • x).

Equations

• NavierStokes.R3CompactCandidate.outerCutoff x = NavierStokes.SpatialLocalization.spatialCutoff ((1 / 2) • x)

def NavierStokes.R3CompactCandidate.outerSupport : Set ProblemStatement.Space

Outer support, given by (fun x : Space => (2 : ℝ) • x) '' supportCylinder.

Equations

• NavierStokes.R3CompactCandidate.outerSupport = (fun (x : NavierStokes.ProblemStatement.Space) => 2 • x) '' NavierStokes.SpatialLocalization.supportCylinder

theorem NavierStokes.R3CompactCandidate.outerSupport_compact : IsCompact outerSupport

theorem NavierStokes.R3CompactCandidate.outerCutoff_smooth : ContDiff ℝ (↑⊤) outerCutoff

theorem NavierStokes.R3CompactCandidate.outerCutoff_one {x : ProblemStatement.Space} (hx : x ∈ SpatialLocalization.supportCylinder) : outerCutoff x = 1

theorem NavierStokes.R3CompactCandidate.outerCutoff_zero_outside {x : ProblemStatement.Space} (hx : x ∉ outerSupport) : outerCutoff x = 0

theorem NavierStokes.R3CompactCandidate.outerCutoff_ne_zero_inner {x : ProblemStatement.Space} (hx : outerCutoff x ≠ 0) : x ∈ PeriodicLocalization.innerCube (1 / 4)

theorem NavierStokes.R3CompactCandidate.supportCylinder_inner {x : ProblemStatement.Space} (hx : x ∈ SpatialLocalization.supportCylinder) : x ∈ PeriodicLocalization.innerCube (1 / 4)

noncomputable def NavierStokes.R3CompactCandidate.compactForce (f : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Compact force, defined pointwise by outerCutoff z.2 • f z.

Equations

• NavierStokes.R3CompactCandidate.compactForce f z = NavierStokes.R3CompactCandidate.outerCutoff z.2 • f z

theorem NavierStokes.R3CompactCandidate.compactForce_smooth {f : ProblemStatement.VelocityField} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) : ContDiffOn ℝ (↑⊤) (compactForce f) ProblemStatement.futureDomain

theorem NavierStokes.R3CompactCandidate.compactForce_supported (f : ProblemStatement.VelocityField) : CompactSpatialForceDecay.SupportedIn outerSupport (compactForce f)

theorem NavierStokes.R3CompactCandidate.compactForce_time_support {f : ProblemStatement.VelocityField} (hf : ProblemStatement.CompactFutureTimeSupport f) : ProblemStatement.CompactFutureTimeSupport (compactForce f)

theorem NavierStokes.R3CompactCandidate.eventually_zero_outside {V : Type u_1} [Zero V] {g : ProblemStatement.SpaceTime → V} (hg : ∀ (t : ℝ), ∀ x ∉ SpatialLocalization.supportCylinder, g (t, x) = 0) {z : ProblemStatement.SpaceTime} (hz : z.2 ∉ SpatialLocalization.supportCylinder) : g =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.R3CompactCandidate.local_model_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {g G : ProblemStatement.SpaceTime → V} (hG : ContDiffOn ℝ (↑⊤) G ProblemStatement.preSingularDomain) (hs : ∀ (t : ℝ), ∀ x ∉ SpatialLocalization.supportCylinder, g (t, x) = 0) (he : ∀ (z : ProblemStatement.SpaceTime), z.2 ∈ PeriodicLocalization.innerCube (1 / 4) → G =ᶠ[nhds z] g) : ContDiffOn ℝ (↑⊤) g ProblemStatement.preSingularDomain

theorem NavierStokes.R3CompactCandidate.local_model_divergence {u U : ProblemStatement.VelocityField} (hs : ∀ (t : ℝ), ∀ x ∉ SpatialLocalization.supportCylinder, u (t, x) = 0) (he : ∀ (z : ProblemStatement.SpaceTime), z.2 ∈ PeriodicLocalization.innerCube (1 / 4) → U =ᶠ[nhds z] u) {t : ℝ} (hd : ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence U t x = 0) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence u t x = 0

theorem NavierStokes.R3CompactCandidate.local_model_equation {u U : ProblemStatement.VelocityField} {p P : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (hu : ∀ (t : ℝ), ∀ x ∉ SpatialLocalization.supportCylinder, u (t, x) = 0) (hp : ∀ (t : ℝ), ∀ x ∉ SpatialLocalization.supportCylinder, p (t, x) = 0) (heu : ∀ (z : ProblemStatement.SpaceTime), z.2 ∈ PeriodicLocalization.innerCube (1 / 4) → U =ᶠ[nhds z] u) (hep : ∀ (z : ProblemStatement.SpaceTime), z.2 ∈ PeriodicLocalization.innerCube (1 / 4) → P =ᶠ[nhds z] p) {t : ℝ} (hNS : ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual U P t x = f (t, x)) (x : ProblemStatement.Space) : ProblemStatement.navierStokesResidual u p t x = compactForce f (t, x)

theorem NavierStokes.R3CompactCandidate.local_model_unbounded {u U : ProblemStatement.VelocityField} (hper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) U) (he : ∀ (z : ProblemStatement.SpaceTime), z.2 ∈ PeriodicLocalization.innerCube (1 / 4) → U =ᶠ[nhds z] u) (hb : ProblemStatement.SpeedUnboundedAtOne U) : ProblemStatement.SpeedUnboundedAtOne u

theorem NavierStokes.R3CompactCandidate.of_periodic_local_model {u U : ProblemStatement.VelocityField} {p P : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties U P f) (hu : ∀ (t : ℝ), ∀ x ∉ SpatialLocalization.supportCylinder, u (t, x) = 0) (hp : ∀ (t : ℝ), ∀ x ∉ SpatialLocalization.supportCylinder, p (t, x) = 0) (heu : ∀ (z : ProblemStatement.SpaceTime), z.2 ∈ PeriodicLocalization.innerCube (1 / 4) → U =ᶠ[nhds z] u) (hep : ∀ (z : ProblemStatement.SpaceTime), z.2 ∈ PeriodicLocalization.innerCube (1 / 4) → P =ᶠ[nhds z] p) : Properties u p (compactForce f)

Extract a compact whole-space candidate from its periodic local model.

noncomputable def NavierStokes.R3CompactCandidate.velocity (A B : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Velocity, given by TimeLocalization.activatedVelocity (fun z => cutVelocity A z + cutPotential B z).

Equations

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

noncomputable def NavierStokes.R3CompactCandidate.pressure (P : ProblemStatement.PressureField) : ProblemStatement.PressureField

Pressure, given by TimeLocalization.activatedPressure (cutPressure P).

Equations

• NavierStokes.R3CompactCandidate.pressure P = NavierStokes.TimeLocalization.activatedPressure (NavierStokes.SpatialLocalization.cutPressure P)

noncomputable def NavierStokes.R3CompactCandidate.periodicVelocity (A B : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Periodic velocity, constructed using TimeLocalization.activatedVelocity.

Equations

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

noncomputable def NavierStokes.R3CompactCandidate.periodicPressure (P : ProblemStatement.PressureField) : ProblemStatement.PressureField

Periodic pressure, given by TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure P).

Equations

• NavierStokes.R3CompactCandidate.periodicPressure P = NavierStokes.TimeLocalization.activatedPressure (NavierStokes.SpatialLocalization.periodicPressure P)

theorem NavierStokes.R3CompactCandidate.velocity_supported (A B : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hx : x ∉ SpatialLocalization.supportCylinder) : velocity A B (t, x) = 0

theorem NavierStokes.R3CompactCandidate.pressure_supported (P : ProblemStatement.PressureField) (t : ℝ) (x : ProblemStatement.Space) (hx : x ∉ SpatialLocalization.supportCylinder) : pressure P (t, x) = 0

theorem NavierStokes.R3CompactCandidate.velocity_locally_eq (A B : ProblemStatement.VelocityField) (z : ProblemStatement.SpaceTime) (hz : z.2 ∈ PeriodicLocalization.innerCube (1 / 4)) : periodicVelocity A B =ᶠ[nhds z] velocity A B

theorem NavierStokes.R3CompactCandidate.pressure_locally_eq (P : ProblemStatement.PressureField) (z : ProblemStatement.SpaceTime) (hz : z.2 ∈ PeriodicLocalization.innerCube (1 / 4)) : periodicPressure P =ᶠ[nhds z] pressure P

theorem NavierStokes.R3CompactCandidate.of_localized_fields {A B : ProblemStatement.VelocityField} {P : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties (periodicVelocity A B) (periodicPressure P) f) : Properties (velocity A B) (pressure P) (compactForce f)

Use the very same three raw sums retained by selected_witness; no new singular-field existence hypothesis is needed.

theorem NavierStokes.R3CompactCandidate.Properties.forceConditionDecay {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : Properties u p f) : Comparator.ForceConditionDecay (ComparatorBridge.toComparator f)

Every compact whole-space force constructed here satisfies the exact spatial and temporal decay requirements of the comparator.

theorem NavierStokes.R3CompactCandidate.Properties.not_global_agreement {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : Properties u p f) {v : ProblemStatement.VelocityField} (hv : ContDiffOn ℝ (↑⊤) v ProblemStatement.futureDomain) : ¬∀ t ∈ Set.Ico 0 1, ∀ (x : ProblemStatement.Space), u (t, x) = v (t, x)

After equality with the compact candidate has been proved, smoothness on a compact space-time neighborhood of time one gives the contradiction.