Differential identities for Navier–Stokes solution differences

Subtraction of the physical differential operators, the difference equation, and pointwise energy identities are independent of boundary conditions and integration domains. This module provides that common API for periodic and whole-space energy estimates. Spatial and temporal slice regularity works over arbitrary real normed spaces, and the nonlinear energy bound works in any real inner product space.

This separation of the common differential API follows Code4me2's refactor. The original periodic names remain available as compatibility lemmas.

def NavierStokes.SolutionDifference.slab {X : Type u_1} (a b : ℝ) : Set (ℝ × X)

The closed time interval [a, b] with unrestricted spatial coordinates.

Equations

• NavierStokes.SolutionDifference.slab a b = Set.Icc a b ×ˢ Set.univ

@[simp]

theorem NavierStokes.SolutionDifference.mem_slab {X : Type u_1} {a b : ℝ} {z : ℝ × X} : z ∈ slab a b ↔ z.1 ∈ Set.Icc a b

theorem NavierStokes.SolutionDifference.slab_mono {X : Type u_1} {a b c d : ℝ} (hca : c ≤ a) (hbd : b ≤ d) : slab a b ⊆ slab c d

Enlarging the time interval enlarges its slab.

noncomputable def NavierStokes.SolutionDifference.spatialPartial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i : Fin 3) (f : ProblemStatement.Space → E) (x : ProblemStatement.Space) : E

Differentiate a spatial field in the ith standard coordinate direction.

Equations

• NavierStokes.SolutionDifference.spatialPartial i f x = (fderiv ℝ f x) (NavierStokes.ProblemStatement.coordinateVector i)

theorem NavierStokes.SolutionDifference.continuous_partial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) (i : Fin 3) : Continuous (spatialPartial i f)

Coordinate partial derivatives of a continuously differentiable field are continuous.

theorem NavierStokes.SolutionDifference.spatial_smooth {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b t : ℝ} {u : ℝ × X → V} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Icc a b) : ContDiff ℝ ↑⊤ fun (x : X) => u (t, x)

theorem NavierStokes.SolutionDifference.smooth_at_interior {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b t : ℝ} {u : ℝ × X → V} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Ioo a b) (x : X) : ContDiffAt ℝ (↑⊤) u (t, x)

theorem NavierStokes.SolutionDifference.spatialDerivative_sub {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.spatialDerivative (u - v) t x = ProblemStatement.spatialDerivative u t x - ProblemStatement.spatialDerivative v t x

theorem NavierStokes.SolutionDifference.spatialDivergence_sub {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (u - v) t x = ProblemStatement.spatialDivergence u t x - ProblemStatement.spatialDivergence v t x

theorem NavierStokes.SolutionDifference.advection_difference {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.advection u t x - ProblemStatement.advection v t x = (ProblemStatement.spatialDerivative u t x) ((u - v) (t, x)) + (ProblemStatement.spatialDerivative (u - v) t x) (v (t, x))

theorem NavierStokes.SolutionDifference.spatialLaplacian_sub {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.spatialLaplacian (u - v) t x = ProblemStatement.spatialLaplacian u t x - ProblemStatement.spatialLaplacian v t x

theorem NavierStokes.SolutionDifference.pressureGradient_sub {p q : ProblemStatement.PressureField} {t : ℝ} (hp : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => p (t, x)) (hq : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => q (t, x)) (x : ProblemStatement.Space) : ProblemStatement.pressureGradient (p - q) t x = ProblemStatement.pressureGradient p t x - ProblemStatement.pressureGradient q t x

theorem NavierStokes.SolutionDifference.temporalDerivative_sub {u v : ProblemStatement.VelocityField} {t : ℝ} {x : ProblemStatement.Space} (hu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (hv : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) : ProblemStatement.temporalDerivative (u - v) t x = ProblemStatement.temporalDerivative u t x - ProblemStatement.temporalDerivative v t x

theorem NavierStokes.SolutionDifference.difference_equation {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {t : ℝ} {x : ProblemStatement.Space} (hu : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => u (t, y)) (hv : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => v (t, y)) (hp : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => p (t, y)) (hq : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => q (t, y)) (htu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (htv : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) (hNS : ProblemStatement.navierStokesResidual u p t x = ProblemStatement.navierStokesResidual v q t x) : ProblemStatement.temporalDerivative (u - v) t x = ProblemStatement.spatialLaplacian (u - v) t x - (ProblemStatement.spatialDerivative u t x) ((u - v) (t, x)) - (ProblemStatement.spatialDerivative (u - v) t x) (v (t, x)) - ProblemStatement.pressureGradient (p - q) t x

Subtract the actual Navier--Stokes residuals, retaining the favorable transport decomposition Du(w) + Dw(v).

theorem NavierStokes.SolutionDifference.nonlinear_energy_bound {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A : V →L[ℝ] V) (w : V) {B : ℝ} (hB : ‖A‖ ≤ B) : -inner ℝ w (A w) ≤ B * ‖w‖ ^ 2

The adverse quadratic energy term is bounded by an operator norm bound in any real inner product space.

theorem NavierStokes.SolutionDifference.spatialDerivative_eq_within_comp {a b t : ℝ} {u : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Icc a b) (x : ProblemStatement.Space) : ProblemStatement.spatialDerivative u t x = fderivWithin ℝ u (slab a b) (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ ProblemStatement.Space

The ordinary spatial derivative at a time endpoint is the restriction of the joint within-derivative to spatial directions.

theorem NavierStokes.SolutionDifference.exists_gradient_bound {a b : ℝ} (hab : a < b) {u : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) {K : Set ProblemStatement.Space} (hK : IsCompact K) : ∃ (B : ℝ), 0 < B ∧ ∀ t ∈ Set.Icc a b, ∀ x ∈ K, ‖ProblemStatement.spatialDerivative u t x‖ ≤ B

Compactness supplies the spatial-gradient bound used by the energy estimate; it is a conclusion from smoothness, not an input to uniqueness.

theorem NavierStokes.SolutionDifference.sum_coordinates (x : ProblemStatement.Space) : ∑ i : Fin 3, x.ofLp i • ProblemStatement.coordinateVector i = x

Reconstruction in the standard Euclidean coordinate basis.

theorem NavierStokes.SolutionDifference.spatial_partial_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.Space → V} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => (fderiv ℝ f x) (ProblemStatement.coordinateVector i)

theorem NavierStokes.SolutionDifference.component_contDiff {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (j : Fin 3) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => (f x).ofLp j

theorem NavierStokes.SolutionDifference.fderiv_component {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (j : Fin 3) (x v : ProblemStatement.Space) : (fderiv ℝ (fun (y : ProblemStatement.Space) => (f y).ofLp j) x) v = ((fderiv ℝ f x) v).ofLp j

theorem NavierStokes.SolutionDifference.fderiv_apply_eq_sum (f : ProblemStatement.Space → ℝ) (x v : ProblemStatement.Space) : (fderiv ℝ f x) v = ∑ i : Fin 3, v.ofLp i * (fderiv ℝ f x) (ProblemStatement.coordinateVector i)

theorem NavierStokes.SolutionDifference.fderiv_normsq {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {f : X → V} (hf : ContDiff ℝ (↑⊤) f) (x v : X) : (fderiv ℝ (fun (y : X) => ‖f y‖ ^ 2) x) v = 2 * inner ℝ (f x) ((fderiv ℝ f x) v)

theorem NavierStokes.SolutionDifference.fderiv_inner {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {f g : X → V} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x v : X) : (fderiv ℝ (fun (y : X) => inner ℝ (f y) (g y)) x) v = inner ℝ (f x) ((fderiv ℝ g x) v) + inner ℝ ((fderiv ℝ f x) v) (g x)

theorem NavierStokes.SolutionDifference.inner_pressureGradient (p : ProblemStatement.PressureField) (t : ℝ) (x w : ProblemStatement.Space) : inner ℝ w (ProblemStatement.pressureGradient p t x) = (fderiv ℝ (fun (y : ProblemStatement.Space) => p (t, y)) x) w

The pressure term paired with a vector is its scalar directional derivative. This uses exactly the gradient definition in the target.

theorem NavierStokes.SolutionDifference.energy_density_derivative {u : ProblemStatement.VelocityField} {t : ℝ} {x : ProblemStatement.Space} (hu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) : HasDerivAt (fun (s : ℝ) => ‖u (s, x)‖ ^ 2) (2 * inner ℝ (u (t, x)) (ProblemStatement.temporalDerivative u t x)) t

theorem NavierStokes.SolutionDifference.spatialLaplacian_contDiff {w : ProblemStatement.VelocityField} {t : ℝ} (hw : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => w (t, x)) : ContDiff ℝ (↑⊤) (ProblemStatement.spatialLaplacian w t)

theorem NavierStokes.SolutionDifference.pressureGradient_contDiff {p : ProblemStatement.PressureField} {t : ℝ} (hp : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => p (t, x)) : ContDiff ℝ (↑⊤) (ProblemStatement.pressureGradient p t)

theorem NavierStokes.SolutionDifference.time_differentiable_at_interior {X : Type u_1} {V : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b t : ℝ} {u : ℝ × X → V} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Ioo a b) (x : X) : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t