Coordinate and viscosity bridge to the Clay statements

This module translates the project's physical differential operators to the comparator's operators, and normalizes any positive viscosity to one. It uses only the independent comparator definitions; no reference theorem is imported. The applications to the periodic and finite-energy candidates share the same normalization theorem, normalized_solution_core.

The shared normalization API adapts work by Code4me2: https://github.com/Code4me2/NavierStokesAndEuler/tree/26e896edbdbe1215c0d50ddba24b2b6453646f5f.

def NavierStokes.ComparatorBridge.toComparator {V : Type u_1} (f : ProblemStatement.SpaceTime → V) : ProblemStatement.Space → ℝ → V

Change the argument order from (time, space) to space, time.

Equations

• NavierStokes.ComparatorBridge.toComparator f x t = f (t, x)

def NavierStokes.ComparatorBridge.fromComparator {V : Type u_1} (f : ProblemStatement.Space → ℝ → V) : ProblemStatement.SpaceTime → V

Change the argument order from space, time to (time, space).

Equations

• NavierStokes.ComparatorBridge.fromComparator f z = f z.2 z.1

theorem NavierStokes.ComparatorBridge.divergence_eq (v : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence v t x = Comparator.divergence (fun (y : EuclideanSpace ℝ (Fin 3)) => v (t, y)) x

theorem NavierStokes.ComparatorBridge.gradient_eq (p : ProblemStatement.PressureField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.pressureGradient p t x = gradient (fun (y : ProblemStatement.Space) => p (t, y)) x

theorem NavierStokes.ComparatorBridge.laplacian_eq (v : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hv : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => v (t, y)) : ProblemStatement.spatialLaplacian v t x = Laplacian.laplacian (fun (y : ProblemStatement.Space) => v (t, y)) x

theorem NavierStokes.ComparatorBridge.temporalDerivative_eq (v : ProblemStatement.VelocityField) {t : ℝ} (ht : 0 < t) (x : ProblemStatement.Space) : ProblemStatement.temporalDerivative v t x = derivWithin (fun (s : ℝ) => v (s, x)) (Set.Ici 0) t

def NavierStokes.ComparatorBridge.rescale {V : Type u_1} [SMul ℝ V] (a c : ℝ) (f : ProblemStatement.SpaceTime → V) : ProblemStatement.SpaceTime → V

Time change and amplitude change for a spacetime field.

Equations

• NavierStokes.ComparatorBridge.rescale a c f z = a • f (c * z.1, z.2)

def NavierStokes.ComparatorBridge.rescaledForce (ν : ℝ) (f : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

The force for viscosity ν, starting with a force for viscosity one.

Equations

• NavierStokes.ComparatorBridge.rescaledForce ν f = NavierStokes.ComparatorBridge.rescale (ν ^ 2) ν f

theorem NavierStokes.ComparatorBridge.rescale_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) (a : ℝ) {c : ℝ} (hc : 0 ≤ c) : ContDiffOn ℝ (↑⊤) (rescale a c f) ProblemStatement.futureDomain

theorem NavierStokes.ComparatorBridge.rescale_periodic {V : Type u_1} [SMul ℝ V] {f : ProblemStatement.SpaceTime → V} (hf : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) f) (a : ℝ) {c : ℝ} (hc : 0 ≤ c) : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) (rescale a c f)

theorem NavierStokes.ComparatorBridge.rescale_support {f : ProblemStatement.VelocityField} (hf : ProblemStatement.CompactFutureTimeSupport f) (a : ℝ) {c : ℝ} (hc : 0 < c) : ProblemStatement.CompactFutureTimeSupport (rescale a c f)

theorem NavierStokes.ComparatorBridge.fromComparator_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.Space → ℝ → V} (hf : ContDiffOn ℝ (↑⊤) (↿f) (Set.univ ×ˢ Set.Ici 0)) : ContDiffOn ℝ (↑⊤) (fromComparator f) ProblemStatement.futureDomain

theorem NavierStokes.ComparatorBridge.toComparator_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) : ContDiffOn ℝ (↑⊤) (↿(toComparator f)) (Set.univ ×ˢ Set.Ici 0)

theorem NavierStokes.ComparatorBridge.toComparator_jet_norm (f : ProblemStatement.VelocityField) (m : ℕ) (x : ProblemStatement.Space) {t : ℝ} (ht : 0 ≤ t) : ‖iteratedFDerivWithin ℝ m (↿(toComparator f)) (Set.univ ×ˢ Set.Ici 0) (x, t)‖ = ‖iteratedFDerivWithin ℝ m f ProblemStatement.futureDomain (t, x)‖

theorem NavierStokes.ComparatorBridge.forceConditionPeriodic_of_decay {f : ProblemStatement.VelocityField} (hf : ContDiffOn ℝ (↑⊤) f ProblemStatement.futureDomain) (hp : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) f) (hd : ∀ (m : ℕ) (K : ℝ), 0 ≤ K → ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ‖iteratedFDerivWithin ℝ m f ProblemStatement.futureDomain (t, x)‖ ≤ C * (1 + t) ^ (-K)) : Comparator.ForceConditionPeriodic (toComparator f)

All real decay exponents follow from the nonnegative-exponent jet bounds.

theorem NavierStokes.ComparatorBridge.zero_initial_condition : Comparator.InitialVelocityConditionPeriodic fun (x : ProblemStatement.Space) => 0

theorem NavierStokes.ComparatorBridge.rescale_spatialDerivative (a c : ℝ) (v : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.spatialDerivative (rescale a c v) t x = a • ProblemStatement.spatialDerivative v (c * t) x

theorem NavierStokes.ComparatorBridge.rescale_divergence (a c : ℝ) (v : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (rescale a c v) t x = a * ProblemStatement.spatialDivergence v (c * t) x

theorem NavierStokes.ComparatorBridge.rescale_advection (a c : ℝ) (v : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.advection (rescale a c v) t x = a ^ 2 • ProblemStatement.advection v (c * t) x

theorem NavierStokes.ComparatorBridge.rescale_gradient (a c : ℝ) (p : ProblemStatement.PressureField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.pressureGradient (rescale a c p) t x = a • ProblemStatement.pressureGradient p (c * t) x

theorem NavierStokes.ComparatorBridge.rescale_laplacian (a c : ℝ) (v : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.spatialLaplacian (rescale a c v) t x = a • ProblemStatement.spatialLaplacian v (c * t) x

theorem NavierStokes.ComparatorBridge.rescale_temporalDerivative (a c : ℝ) (v : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hv : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) (c * t)) : ProblemStatement.temporalDerivative (rescale a c v) t x = (a * c) • ProblemStatement.temporalDerivative v (c * t) x

theorem NavierStokes.ComparatorBridge.smooth_space_slice {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : ProblemStatement.SpaceTime → V} (hv : ContDiffOn ℝ (↑⊤) v ProblemStatement.futureDomain) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)

theorem NavierStokes.ComparatorBridge.differentiable_time_slice {v : ProblemStatement.VelocityField} (hv : ContDiffOn ℝ (↑⊤) v ProblemStatement.futureDomain) {t : ℝ} (ht : 0 < t) (x : ProblemStatement.Space) : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t

structure NavierStokes.ComparatorBridge.GlobalSolutionOne (f v : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : Prop

The original project conventions for a global viscosity-one solution.

• velocity_smooth : ContDiffOn ℝ (↑⊤) v ProblemStatement.futureDomain
• pressure_smooth : ContDiffOn ℝ (↑⊤) p ProblemStatement.futureDomain
• velocity_periodic : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) v
• pressure_periodic : ProblemStatement.UnitSpatialPeriodsOn (Set.Ici 0) p
• initial_velocity (x : ProblemStatement.Space) : v (0, x) = 0
• divergence_free (t : ℝ) : 0 ≤ t → ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0
• navier_stokes (t : ℝ) : 0 < t → ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual v p t x = f (t, x)

theorem NavierStokes.ComparatorBridge.GlobalSolutionOne.toSolutionOn {f v : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (solution : GlobalSolutionOne f v p) : SolutionOn 1 0 (fun (x : ProblemStatement.Space) => 0) (Set.Ici 0) f v p

Forget periodicity while preserving the global equation and initial data.

theorem NavierStokes.ComparatorBridge.comparator_equation_core {ν : ℝ} {u₀ : ProblemStatement.Space → ProblemStatement.Space} {f v : ProblemStatement.Space → ℝ → ProblemStatement.Space} {p : ProblemStatement.Space → ℝ → ℝ} (h : Comparator.NavierStokesExistenceAndSmoothness ν u₀ f v p) {t : ℝ} (ht : 0 < t) (x : ProblemStatement.Space) : ProblemStatement.temporalDerivative (fromComparator v) t x + ProblemStatement.advection (fromComparator v) t x - ν • ProblemStatement.spatialLaplacian (fromComparator v) t x + ProblemStatement.pressureGradient (fromComparator p) t x = f x t

The equation in project coordinates, assuming only the common comparator contract.

theorem NavierStokes.ComparatorBridge.comparator_equation {ν : ℝ} {u₀ : ProblemStatement.Space → ProblemStatement.Space} {f v : ProblemStatement.Space → ℝ → ProblemStatement.Space} {p : ProblemStatement.Space → ℝ → ℝ} (h : Comparator.NavierStokesExistenceAndSmoothnessPeriodic ν u₀ f v p) {t : ℝ} (ht : 0 < t) (x : ProblemStatement.Space) : ProblemStatement.temporalDerivative (fromComparator v) t x + ProblemStatement.advection (fromComparator v) t x - ν • ProblemStatement.spatialLaplacian (fromComparator v) t x + ProblemStatement.pressureGradient (fromComparator p) t x = f x t

theorem NavierStokes.ComparatorBridge.rescale_residual_of_differentiable {ν : ℝ} (hν : ν ≠ 0) {v : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} {x : ProblemStatement.Space} (hv : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) (ν⁻¹ * t)) : ProblemStatement.navierStokesResidual (rescale ν⁻¹ ν⁻¹ v) (rescale (ν⁻¹ ^ 2) ν⁻¹ p) t x = ν⁻¹ ^ 2 • viscousResidual ν v p (ν⁻¹ * t) x

Residual scaling needs only a nonzero viscosity and differentiability of the single time slice at the rescaled point; no spatial regularity is assumed.

theorem NavierStokes.ComparatorBridge.rescale_residual {ν : ℝ} (hν : 0 < ν) {v : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hv : ContDiffOn ℝ (↑⊤) v ProblemStatement.futureDomain) {t : ℝ} (ht : 0 < t) (x : ProblemStatement.Space) : ProblemStatement.navierStokesResidual (rescale ν⁻¹ ν⁻¹ v) (rescale (ν⁻¹ ^ 2) ν⁻¹ p) t x = ν⁻¹ ^ 2 • viscousResidual ν v p (ν⁻¹ * t) x

Normalizing time and amplitudes converts the viscosity-ν residual to viscosity one.

theorem NavierStokes.ComparatorBridge.normalized_solution_core {ν : ℝ} (hν : 0 < ν) {f : ProblemStatement.VelocityField} {v : ProblemStatement.Space → ℝ → ProblemStatement.Space} {p : ProblemStatement.Space → ℝ → ℝ} (h : Comparator.NavierStokesExistenceAndSmoothness ν (fun (x : EuclideanSpace ℝ (Fin 3)) => 0) (toComparator (rescaledForce ν f)) v p) : SolutionOn 1 0 (fun (x : ProblemStatement.Space) => 0) (Set.Ici 0) f (rescale ν⁻¹ ν⁻¹ (fromComparator v)) (rescale (ν⁻¹ ^ 2) ν⁻¹ (fromComparator p))

Normalize the common comparator contract; geometric and energy conditions can then be transported independently.

theorem NavierStokes.ComparatorBridge.normalized_solution {ν : ℝ} (hν : 0 < ν) {f : ProblemStatement.VelocityField} {v : ProblemStatement.Space → ℝ → ProblemStatement.Space} {p : ProblemStatement.Space → ℝ → ℝ} (h : Comparator.NavierStokesExistenceAndSmoothnessPeriodic ν (fun (x : EuclideanSpace ℝ (Fin 3)) => 0) (toComparator (rescaledForce ν f)) v p) : GlobalSolutionOne f (rescale ν⁻¹ ν⁻¹ (fromComparator v)) (rescale (ν⁻¹ ^ 2) ν⁻¹ (fromComparator p))

Pull a hypothetical viscosity-ν solution back to viscosity one.