Conservative difference equations tested on compactly supported functions

All integrals use Euclidean Lebesgue measure. Compact support is required only of the test function; the velocities and pressures need no support or decay assumptions for the identities in this module.

noncomputable def NavierStokesR3.ConservativeDifference.scalarLaplacian (f : NavierStokes.ProblemStatement.Space → ℝ) (x : NavierStokes.ProblemStatement.Space) : ℝ

The ordinary scalar Laplacian, with the same coordinate directions as the vector Laplacian in the Navier--Stokes residual.

Equations

• NavierStokesR3.ConservativeDifference.scalarLaplacian f x = ∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial i f) x

theorem NavierStokesR3.ConservativeDifference.scalarLaplacian_contDiff {f : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (scalarLaplacian f)

theorem NavierStokesR3.ConservativeDifference.compact_scalarLaplacian {f : NavierStokes.ProblemStatement.Space → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (scalarLaplacian f)

theorem NavierStokesR3.ConservativeDifference.partial_mul {f g : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => f y * g y) x = f x * NavierStokes.SolutionDifference.spatialPartial i g x + g x * NavierStokes.SolutionDifference.spatialPartial i f x

theorem NavierStokesR3.ConservativeDifference.partial_sub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : NavierStokes.ProblemStatement.Space → V} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => f y - g y) x = NavierStokes.SolutionDifference.spatialPartial i f x - NavierStokes.SolutionDifference.spatialPartial i g x

theorem NavierStokesR3.ConservativeDifference.partial_component {f : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (i k : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => (f y).ofLp k) x = (NavierStokes.SolutionDifference.spatialPartial i f x).ofLp k

theorem NavierStokesR3.ConservativeDifference.pressureGradient_component (p : NavierStokes.ProblemStatement.PressureField) (t : ℝ) (x : NavierStokes.ProblemStatement.Space) (k : Fin 3) : (NavierStokes.ProblemStatement.pressureGradient p t x).ofLp k = NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => p (t, y)) x

theorem NavierStokesR3.ConservativeDifference.spatialLaplacian_component {u : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (x : NavierStokes.ProblemStatement.Space) (k : Fin 3) : (NavierStokes.ProblemStatement.spatialLaplacian u t x).ofLp k = scalarLaplacian (fun (y : NavierStokes.ProblemStatement.Space) => (u (t, y)).ofLp k) x

theorem NavierStokesR3.ConservativeDifference.advection_component {u : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (x : NavierStokes.ProblemStatement.Space) (k : Fin 3) : (NavierStokes.ProblemStatement.advection u t x).ofLp k = ∑ i : Fin 3, (u (t, x)).ofLp i * NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => (u (t, y)).ofLp k) x

theorem NavierStokesR3.ConservativeDifference.outerProduct_divergence {u : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (x : NavierStokes.ProblemStatement.Space) (k : Fin 3) : ∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => (u (t, y)).ofLp k * (u (t, y)).ofLp i) x = (u (t, x)).ofLp k * NavierStokes.ProblemStatement.spatialDivergence u t x + (NavierStokes.ProblemStatement.advection u t x).ofLp k

Divergence of the velocity outer product, before using incompressibility.

theorem NavierStokesR3.ConservativeDifference.tensorDiff_contDiff {u v : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (i j : Fin 3) : ContDiff ℝ (↑⊤) (Comparison.tensorDiff u v t i j)

theorem NavierStokesR3.ConservativeDifference.tensorDiff_divergence {u v : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (x : NavierStokes.ProblemStatement.Space) (k : Fin 3) (hdivu : NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hdivv : NavierStokes.ProblemStatement.spatialDivergence v t x = 0) : ∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial i (Comparison.tensorDiff u v t k i) x = (NavierStokes.ProblemStatement.advection u t x).ofLp k - (NavierStokes.ProblemStatement.advection v t x).ofLp k

theorem NavierStokesR3.ConservativeDifference.conservative_difference_equation {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} {t : ℝ} {x : NavierStokes.ProblemStatement.Space} (hu : ContDiff ℝ ↑⊤ fun (y : NavierStokes.ProblemStatement.Space) => u (t, y)) (hv : ContDiff ℝ ↑⊤ fun (y : NavierStokes.ProblemStatement.Space) => v (t, y)) (hp : ContDiff ℝ ↑⊤ fun (y : NavierStokes.ProblemStatement.Space) => p (t, y)) (hq : ContDiff ℝ ↑⊤ fun (y : NavierStokes.ProblemStatement.Space) => q (t, y)) (htu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (htv : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) (hdivu : NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hdivv : NavierStokes.ProblemStatement.spatialDivergence v t x = 0) (hNS : NavierStokes.ProblemStatement.navierStokesResidual u p t x = NavierStokes.ProblemStatement.navierStokesResidual v q t x) (k : Fin 3) : (NavierStokes.ProblemStatement.temporalDerivative (u - v) t x).ofLp k = (NavierStokes.ProblemStatement.spatialLaplacian (u - v) t x).ofLp k - ∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial i (Comparison.tensorDiff u v t k i) x - NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x

The exact conservative equation for a difference of smooth solutions having the same viscosity-one residual.

theorem NavierStokesR3.ConservativeDifference.integral_scalarLaplacian_mul {f ψ : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) : ∫ (x : NavierStokes.ProblemStatement.Space), scalarLaplacian f x * ψ x = ∫ (x : NavierStokes.ProblemStatement.Space), f x * scalarLaplacian ψ x

Twice integrating by parts transfers a scalar Laplacian to the compact test function, regardless of growth of the other smooth function.

theorem NavierStokesR3.ConservativeDifference.integrable_mul_test {f ψ : NavierStokes.ProblemStatement.Space → ℝ} (hf : Continuous f) (hψ : Continuous ψ) (hcψ : HasCompactSupport ψ) : MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => f x * ψ x) MeasureTheory.volume

theorem NavierStokesR3.ConservativeDifference.integral_tensorDiff_divergence_mul {u v : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), (∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial i (Comparison.tensorDiff u v t k i) x) * ψ x = -∑ i : Fin 3, ∫ (x : ProblemStatement.Space), Comparison.tensorDiff u v t k i x * NavierStokes.SolutionDifference.spatialPartial i ψ x

theorem NavierStokesR3.ConservativeDifference.weak_pressure_gradient {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} {t : ℝ} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (hp : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => p (t, x)) (hq : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => q (t, x)) (htu : ∀ (x : NavierStokes.ProblemStatement.Space), DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (htv : ∀ (x : NavierStokes.ProblemStatement.Space), DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) (hdivu : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hdivv : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence v t x = 0) (hNS : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = NavierStokes.ProblemStatement.navierStokesResidual v q t x) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ψ x = ((∫ (x : NavierStokes.ProblemStatement.Space), ((u - v) (t, x)).ofLp k * scalarLaplacian ψ x) - ∫ (x : NavierStokes.ProblemStatement.Space), (NavierStokes.ProblemStatement.temporalDerivative (u - v) t x).ofLp k * ψ x) + ∑ i : Fin 3, ∫ (x : ProblemStatement.Space), Comparison.tensorDiff u v t k i x * NavierStokes.SolutionDifference.spatialPartial i ψ x

Testing the conservative equation against a compact scalar test transfers all spatial derivatives off the velocity difference and tensor difference. No global integrability assumption is imposed on either pressure.

theorem NavierStokesR3.ConservativeDifference.weak_pressure_gradient_on_slab {a b t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hu : ContDiffOn ℝ (↑⊤) u (Comparison.slab a b)) (hv : ContDiffOn ℝ (↑⊤) v (Comparison.slab a b)) (hp : ContDiffOn ℝ (↑⊤) p (Comparison.slab a b)) (hq : ContDiffOn ℝ (↑⊤) q (Comparison.slab a b)) (ht : t ∈ Set.Ioo a b) (hdivu : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hdivv : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence v t x = 0) (hNS : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = NavierStokes.ProblemStatement.navierStokesResidual v q t x) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ψ x = ((∫ (x : NavierStokes.ProblemStatement.Space), ((u - v) (t, x)).ofLp k * scalarLaplacian ψ x) - ∫ (x : NavierStokes.ProblemStatement.Space), (NavierStokes.ProblemStatement.temporalDerivative (u - v) t x).ofLp k * ψ x) + ∑ i : Fin 3, ∫ (x : ProblemStatement.Space), Comparison.tensorDiff u v t k i x * NavierStokes.SolutionDifference.spatialPartial i ψ x

A slab version of the compact weak identity with time differentiability supplied by joint smoothness.

theorem NavierStokesR3.ConservativeDifference.partial_partial_eq_fderiv {f : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial j f) x = ((fderiv ℝ (fderiv ℝ f) x) (NavierStokes.ProblemStatement.coordinateVector i)) (NavierStokes.ProblemStatement.coordinateVector j)

theorem NavierStokesR3.ConservativeDifference.partial_comm {f : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial j f) x = NavierStokes.SolutionDifference.spatialPartial j (NavierStokes.SolutionDifference.spatialPartial i f) x

theorem NavierStokesR3.ConservativeDifference.partial_sum {f : Fin 3 → NavierStokes.ProblemStatement.Space → ℝ} (hf : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (f i)) (k : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => ∑ i : Fin 3, f i y) x = ∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial k (f i) x

theorem NavierStokesR3.ConservativeDifference.partial_scalarLaplacian {f : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (k : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial k (scalarLaplacian f) x = scalarLaplacian (NavierStokes.SolutionDifference.spatialPartial k f) x

theorem NavierStokesR3.ConservativeDifference.integral_divergence_free_test {w : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hw : ContDiff ℝ (↑⊤) w) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i w x).ofLp i = 0) : ∑ i : Fin 3, ∫ (x : NavierStokes.ProblemStatement.Space), (w x).ofLp i * NavierStokes.SolutionDifference.spatialPartial i ψ x = 0

A compact scalar test detects the ordinary divergence, even when the vector field has no compact support.

theorem NavierStokesR3.ConservativeDifference.component_test_hasDerivAt {a b t : ℝ} {w : NavierStokes.ProblemStatement.VelocityField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hw : ContDiffOn ℝ (↑⊤) w (Comparison.slab a b)) (ht : t ∈ Set.Ioo a b) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : HasDerivAt (fun (s : ℝ) => ∫ (x : NavierStokes.ProblemStatement.Space), (w (s, x)).ofLp k * ψ x) (∫ (x : NavierStokes.ProblemStatement.Space), (NavierStokes.ProblemStatement.temporalDerivative w t x).ofLp k * ψ x) t

Differentiation of one component paired with a fixed compact spatial test. The compact support supplies a common spatial domain for differentiation.

theorem NavierStokesR3.ConservativeDifference.integral_time_derivative_divergence_free {a b t : ℝ} {w : NavierStokes.ProblemStatement.VelocityField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hw : ContDiffOn ℝ (↑⊤) w (Comparison.slab a b)) (ht : t ∈ Set.Ioo a b) (hdiv : ∀ s ∈ Set.Ioo a b, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence w s x = 0) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) : ∑ k : Fin 3, ∫ (x : NavierStokes.ProblemStatement.Space), (NavierStokes.ProblemStatement.temporalDerivative w t x).ofLp k * NavierStokes.SolutionDifference.spatialPartial k ψ x = 0

The time derivative has zero distributional divergence. This follows by differentiating a compact pairing that is identically zero on the time interval.

theorem NavierStokesR3.ConservativeDifference.integral_gradient_pairing {f ψ : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) : ∑ k : Fin 3, ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k f x * NavierStokes.SolutionDifference.spatialPartial k ψ x = -∫ (x : NavierStokes.ProblemStatement.Space), f x * scalarLaplacian ψ x

theorem NavierStokesR3.ConservativeDifference.weak_pressure_poisson {a b t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hu : ContDiffOn ℝ (↑⊤) u (Comparison.slab a b)) (hv : ContDiffOn ℝ (↑⊤) v (Comparison.slab a b)) (hp : ContDiffOn ℝ (↑⊤) p (Comparison.slab a b)) (hq : ContDiffOn ℝ (↑⊤) q (Comparison.slab a b)) (ht : t ∈ Set.Ioo a b) (hdivu : ∀ s ∈ Set.Ioo a b, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u s x = 0) (hdivv : ∀ s ∈ Set.Ioo a b, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence v s x = 0) (hNS : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = NavierStokes.ProblemStatement.navierStokesResidual v q t x) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) : ∫ (x : NavierStokes.ProblemStatement.Space), (p - q) (t, x) * scalarLaplacian ψ x = -∑ k : Fin 3, ∑ i : Fin 3, ∫ (x : ProblemStatement.Space), Comparison.tensorDiff u v t k i x * NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial k ψ) x

The pressure difference solves the compact-test Poisson equation obtained from the actual Navier--Stokes residual and incompressibility. No pressure normalization, growth hypothesis, or integrability at infinity is used.