Spatial localization of a curl field and a direct angular field

The manuscript cuts direct angular means as vector fields, separately from the potentials whose curls give the other components. The construction here keeps that distinction. The existing spatial cutoff is axisymmetric; its action on direct angular means can therefore be supplied by the angular-field calculus. No compactly supported potential for an arbitrary angular mean is postulated.

The endpoint results below take the original mixed fields, their actual one-sided extensions, and the joint residual limits as inputs. They construct the periodic fields and their residual limits. They do not establish the correction iteration or the existence of singular incoming fields.

noncomputable def NavierStokes.MixedPeriodicAssembly.velocity (A v : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

The direct field is added after taking the curl.

Equations

• NavierStokes.MixedPeriodicAssembly.velocity A v z = NavierStokes.SpatialCurl.spatialCurl A z + v z

noncomputable def NavierStokes.MixedPeriodicAssembly.cutVelocity (A v : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Spatial localization keeps every potential-cutoff derivative.

Equations

• NavierStokes.MixedPeriodicAssembly.cutVelocity A v z = NavierStokes.SpatialLocalization.cutVelocity A z + NavierStokes.SpatialLocalization.cutPotential v z

noncomputable def NavierStokes.MixedPeriodicAssembly.periodicVelocity (A v : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Periodize the cut potential and the cut direct field separately.

Equations

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

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

Original residual, defined pointwise by navierStokesResidual (velocity A v) p z.1 z.2.

Equations

• NavierStokes.MixedPeriodicAssembly.originalResidual A v p z = NavierStokes.ProblemStatement.navierStokesResidual (NavierStokes.MixedPeriodicAssembly.velocity A v) p z.1 z.2

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

Cut residual, defined pointwise by navierStokesResidual (cutVelocity A v) (SpatialLocalization.cutPressure p) z.1 z.2.

Equations

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

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

Periodic residual, defined pointwise by navierStokesResidual (periodicVelocity A v) (SpatialLocalization.periodicPressure p) z.1 z.2.

Equations

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

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

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

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

theorem NavierStokes.MixedPeriodicAssembly.cutVelocity_eventuallyEq (A v : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ SpatialLocalization.plateau) : cutVelocity A v =ᶠ[nhds z] velocity A v

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

theorem NavierStokes.MixedPeriodicAssembly.periodicVelocity_origin (A v : ProblemStatement.VelocityField) (t : ℝ) : periodicVelocity A v (t, 0) = velocity A v (t, 0)

theorem NavierStokes.MixedPeriodicAssembly.periodicResidual_eventuallyEq_cut (A v : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (hz : z.2 ∈ PeriodicLocalization.innerCube (1 / 4)) : periodicResidual A v p =ᶠ[nhds z] cutResidual A v p

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

theorem NavierStokes.MixedPeriodicAssembly.spatialDivergence_congr {u v : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (he : u =ᶠ[nhds z] v) : ProblemStatement.spatialDivergence u z.1 z.2 = ProblemStatement.spatialDivergence v z.1 z.2

theorem NavierStokes.MixedPeriodicAssembly.spatialDivergence_periodic {u : ProblemStatement.VelocityField} {times : Set ℝ} (hu : ProblemStatement.UnitSpatialPeriodsOn times u) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => ProblemStatement.spatialDivergence u z.1 z.2

theorem NavierStokes.MixedPeriodicAssembly.periodize_divergence_free {v : ProblemStatement.VelocityField} (hs : PeriodicLocalization.SupportedInCube (1 / 4) v) (t : ℝ) (hd : ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (PeriodicLocalization.periodize v) t x = 0

Disjoint support permits checking the divergence on one local copy. No convergence or differentiability of a formal infinite sum is assumed.

theorem NavierStokes.MixedPeriodicAssembly.spatialDivergence_add {u v : ProblemStatement.VelocityField} {t : ℝ} {x : ProblemStatement.Space} (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) (hv : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => v (t, y)) x) : ProblemStatement.spatialDivergence (fun (z : ProblemStatement.SpaceTime) => u z + v z) t x = ProblemStatement.spatialDivergence u t x + ProblemStatement.spatialDivergence v t x

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

The angular-field calculus supplies hd from axisymmetry. The curl component and the lattice periodization introduce no new divergence.

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

theorem NavierStokes.MixedPeriodicAssembly.cutResidual_eventuallyEq {A A' v v' : ProblemStatement.VelocityField} {p p' : ProblemStatement.PressureField} {z : ProblemStatement.SpaceTime} (hA : A =ᶠ[nhds z] A') (hv : v =ᶠ[nhds z] v') (hp : p =ᶠ[nhds z] p') : cutResidual A v p =ᶠ[nhds z] cutResidual A' v' p'

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

All three original components have genuine smooth local extensions.

Equations

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

theorem NavierStokes.MixedPeriodicAssembly.cutResidual_awayExtensions {A v : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (eA : JointResidualLimits.AwayExtensions A) (ev : JointResidualLimits.AwayExtensions v) (ep : JointResidualLimits.AwayExtensions p) : JointResidualLimits.AwayExtensions (cutResidual A v p)

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

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

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

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

Constructed tensor limits for every point, including all lattice copies of the singular point. No continuity of the chosen representative is used.

Equations

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

@[simp]

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

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

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

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

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

theorem NavierStokes.MixedPeriodicAssembly.exists_candidate_force {A v : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hv : ContDiffOn ℝ (↑⊤) v (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hd : ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (SpatialLocalization.cutPotential v) t x = 0) (hz : JointResidualLimits.VanishingJointJets (originalResidual A v p)) (eA : JointResidualLimits.AwayExtensions A) (ev : JointResidualLimits.AwayExtensions v) (ep : JointResidualLimits.AwayExtensions p) (haxis : Filter.Tendsto (fun (t : ℝ) => ‖velocity A v (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ∃ (F : ProblemStatement.VelocityField), ProblemStatement.CandidateProperties (TimeLocalization.activatedVelocity (periodicVelocity A v)) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure p)) F ∧ ContDiff ℝ (↑⊤) F ∧ ∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDeriv ℝ n F (1, x) = boundaryLimits A v p eA ev ep x n

Apply the existing force construction to the actual mixed periodic velocity. All remaining analytic assumptions concern the incoming fields.

noncomputable def NavierStokes.MixedPeriodicAssembly.angularDiagonal (h : ℝ) (a : ℕ → ℝ) (D : ℕ → DirectAngularDiagonal.AngularData DirectAngularDiagonal.preterminalSlow) : ProblemStatement.VelocityField

The actual angular stage sum, with the manuscript's implicit physical similarity scale and the same cutoff schedule as the other components.

Equations

• NavierStokes.MixedPeriodicAssembly.angularDiagonal h a D = NavierStokes.DirectAngularDiagonal.angularSum a (NavierStokes.PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar

theorem NavierStokes.MixedPeriodicAssembly.angularDiagonal_origin (h : ℝ) (a : ℕ → ℝ) (D : ℕ → DirectAngularDiagonal.AngularData DirectAngularDiagonal.preterminalSlow) (t : ℝ) : angularDiagonal h a D (t, 0) = 0

The direct angular sum is zero on the axis, without changing the potential's axial value or requiring a radial integral cancellation.

theorem NavierStokes.MixedPeriodicAssembly.exists_force_for_angular_stages {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → DirectAngularDiagonal.AngularData DirectAngularDiagonal.preterminalSlow) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {A : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hA : ContDiffOn ℝ (↑⊤) A (SpacetimeEndpoint.openPast 1)) (hp : ContDiffOn ℝ (↑⊤) p (SpacetimeEndpoint.openPast 1)) (hz : JointResidualLimits.VanishingJointJets (originalResidual A (angularDiagonal h a D) p)) (eA : JointResidualLimits.AwayExtensions A) (ev : JointResidualLimits.AwayExtensions (angularDiagonal h a D)) (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 (TimeLocalization.activatedVelocity (periodicVelocity A (angularDiagonal h a D))) (TimeLocalization.activatedPressure (SpatialLocalization.periodicPressure p)) F ∧ ContDiff ℝ (↑⊤) F ∧ ∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDeriv ℝ n F (1, x) = boundaryLimits A (angularDiagonal h a D) p eA ev ep x n

The angular hypotheses are only its actual smooth supported scalar stages. Its smoothness, localized divergence and zero axis value are proved before applying the force construction. Residual flatness and extensions of the complete incoming fields remain separate analytic obligations.