Canonical pressure flux

The pressure is paired with compact smooth tests through its canonical Riesz functional. Every integral used to split the weighted pairing is shown to be integrable before its norm is estimated.

Compact time tests of the conservative pressure identity

The temporal test has topological support inside the open time interval. The spatial test is smooth and compactly supported. Consequently all pairings are ordinary Lebesgue integrals even when the pressure grows at spatial infinity.

theorem NavierStokesR3.PressureTemporalIdentity.continuous_cutoff_mul {a F : ℝ → ℝ} {s : Set ℝ} (ha : Continuous a) (hF : ContinuousOn F s) (hs : IsOpen s) (hsupp : tsupport a ⊆ s) : Continuous fun (t : ℝ) => a t * F t

A time cutoff supported in an open set turns a continuous function on that set into a globally continuous product, regardless of its values outside.

theorem NavierStokesR3.PressureTemporalIdentity.component_test_continuousOn {T : ℝ} {w : NavierStokes.ProblemStatement.VelocityField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hw : ContinuousOn w (Comparison.slab 0 T)) (hψ : Continuous ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ContinuousOn (fun (t : ℝ) => ∫ (x : NavierStokes.ProblemStatement.Space), (w (t, x)).ofLp k * ψ x) (Set.Icc 0 T)

theorem NavierStokesR3.PressureTemporalIdentity.component_time_test_continuousOn {T : ℝ} {w : NavierStokes.ProblemStatement.VelocityField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hw : ContDiffOn ℝ (↑⊤) w (Comparison.slab 0 T)) (hψ : Continuous ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ContinuousOn (fun (t : ℝ) => ∫ (x : NavierStokes.ProblemStatement.Space), (NavierStokes.ProblemStatement.temporalDerivative w t x).ofLp k * ψ x) (Set.Ioo 0 T)

theorem NavierStokesR3.PressureTemporalIdentity.tensor_test_continuousOn {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hu : ContinuousOn u (Comparison.slab 0 T)) (hv : ContinuousOn v (Comparison.slab 0 T)) (hψ : Continuous ψ) (hcψ : HasCompactSupport ψ) (i j : Fin 3) : ContinuousOn (fun (t : ℝ) => ∫ (x : ProblemStatement.Space), Comparison.tensorDiff u v t i j x * ψ x) (Set.Icc 0 T)

theorem NavierStokesR3.PressureTemporalIdentity.compact_time_integration_by_parts {T : ℝ} {a F D : ℝ → ℝ} (hT : 0 < T) (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) (hF : ContinuousOn F (Set.Icc 0 T)) (hD : ContinuousOn D (Set.Ioo 0 T)) (hderiv : ∀ t ∈ Set.Ioo 0 T, HasDerivAt F (D t) t) : ∫ (t : ℝ) in 0..T, a t * D t = -∫ (t : ℝ) in 0..T, deriv a t * F t

Integration by parts with a temporal test supported away from both endpoints. Only the cutoff-weighted derivative needs to be integrable.

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

The compact pressure-gradient identity integrated against a time test. Both derivatives of the velocity have transferred to the two test functions.

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

The same identity as an ordinary set integral over the closed time interval, convenient for subsequent Fubini and norm estimates.

Compact tests used in pressure recovery

Real compact smooth tests are embedded in the actual complex Schwartz space. The differential operators commute with this embedding. The pressure identities below continue to pair the physical pressure only with compact spatial tests.

def NavierStokesR3.PressureRecovery.realTest (ψ : NavierStokes.ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) : Comparison.ComplexTest

The canonical complex Schwartz test associated to a real compact test.

Equations

• NavierStokesR3.PressureRecovery.realTest ψ hψ hcψ = NavierStokesR3.CompactSchwartz.ofCompactSupport (fun (x : NavierStokesR3.ProblemStatement.Space) => ↑(ψ x)) ⋯ ⋯

@[simp]

theorem NavierStokesR3.PressureRecovery.realTest_apply (ψ : NavierStokes.ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (x : NavierStokes.ProblemStatement.Space) : (realTest ψ hψ hcψ) x = ↑(ψ x)

theorem NavierStokesR3.PressureRecovery.realTest_compact (ψ : NavierStokes.ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) : HasCompactSupport ⇑(realTest ψ hψ hcψ)

theorem NavierStokesR3.PressureRecovery.partial_ofReal {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (x : NavierStokes.ProblemStatement.Space) : NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => ↑(ψ y)) x = ↑(NavierStokes.SolutionDifference.spatialPartial i ψ x)

@[simp]

theorem NavierStokesR3.PressureRecovery.partialCLM_realTest (ψ : NavierStokes.ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (i : Fin 3) : (HarmonicTestFunctionals.partialCLM i) (realTest ψ hψ hcψ) = realTest (NavierStokes.SolutionDifference.spatialPartial i ψ) ⋯ ⋯

@[simp]

theorem NavierStokesR3.PressureRecovery.laplacianCLM_realTest (ψ : NavierStokes.ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) : HarmonicTestFunctionals.laplacianCLM (realTest ψ hψ hcψ) = realTest (ConservativeDifference.scalarLaplacian ψ) ⋯ ⋯

theorem NavierStokesR3.PressureRecovery.partial_laplacian_realTest (ψ : NavierStokes.ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : (HarmonicTestFunctionals.partialCLM k) (HarmonicTestFunctionals.laplacianCLM (realTest ψ hψ hcψ)) = HarmonicTestFunctionals.laplacianCLM ((HarmonicTestFunctionals.partialCLM k) (realTest ψ hψ hcψ))

theorem NavierStokesR3.PressureRecovery.compact_test_decomposition (ψ : Comparison.ComplexTest) (hcψ : HasCompactSupport ⇑ψ) : ψ = realTest (fun (x : NavierStokes.ProblemStatement.Space) => (ψ x).re) ⋯ ⋯ + Complex.I • realTest (fun (x : NavierStokes.ProblemStatement.Space) => (ψ x).im) ⋯ ⋯

A compact complex Schwartz test splits into two compact real tests.

theorem NavierStokesR3.PressureRecovery.compact_harmonic_of_real (F : Comparison.ComplexTest →ₗ[ℂ] ℂ) (hreal : ∀ (ψ : NavierStokes.ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ), F (HarmonicTestFunctionals.laplacianCLM (realTest ψ hψ hcψ)) = 0) (ψ : Comparison.ComplexTest) : HasCompactSupport ⇑ψ → F (HarmonicTestFunctionals.laplacianCLM ψ) = 0

Compact harmonicity of a complex linear functional can be verified using real scalar tests alone.

theorem NavierStokesR3.PressureRecovery.gradient_poisson_test {T t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hu : ContDiffOn ℝ (↑⊤) u (Comparison.slab 0 T)) (hv : ContDiffOn ℝ (↑⊤) v (Comparison.slab 0 T)) (hp : ContDiffOn ℝ (↑⊤) p (Comparison.slab 0 T)) (hq : ContDiffOn ℝ (↑⊤) q (Comparison.slab 0 T)) (ht : t ∈ Set.Ioo 0 T) (hdivu : ∀ s ∈ Set.Ioo 0 T, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u s x = 0) (hdivv : ∀ s ∈ Set.Ioo 0 T, ∀ (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 ψ) (k : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ConservativeDifference.scalarLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : ProblemStatement.Space), Comparison.tensorDiff u v t i j x * NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial j (NavierStokes.SolutionDifference.spatialPartial k ψ)) x

The differentiated pressure Poisson equation, still tested only against compact smooth functions. The derivative order agrees with the Riesz symbol.

theorem NavierStokesR3.PressureRecovery.pressure_gradient_pairing_continuousOn {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hu : ContDiffOn ℝ (↑⊤) u (Comparison.slab 0 T)) (hv : ContDiffOn ℝ (↑⊤) v (Comparison.slab 0 T)) (hp : ContDiffOn ℝ (↑⊤) p (Comparison.slab 0 T)) (hq : ContDiffOn ℝ (↑⊤) q (Comparison.slab 0 T)) (hdivu : ∀ t ∈ Set.Ioo 0 T, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hdivv : ∀ t ∈ Set.Ioo 0 T, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence v t x = 0) (hNS : ∀ t ∈ Set.Ioo 0 T, ∀ (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) : ContinuousOn (fun (t : ℝ) => ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ψ x) (Set.Ioo 0 T)

The compact physical pressure-gradient pairing is continuous at interior times. Joint smoothness and the local equation suffice.

Weak time continuity from uniform spatial L¹ bounds

A jointly continuous scalar field with uniformly bounded spatial L¹ norm has continuous pairings with every continuous test vanishing at infinity. Only the test is approximated by compactly supported functions; no support or derivative bound is imposed on the field.

theorem NavierStokesR3.WeakTimeContinuity.exists_test_bound {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) (hψzero : Filter.Tendsto ψ (Filter.cocompact ProblemStatement.Space) (nhds 0)) : ∃ (C : ℝ), ∀ (x : ProblemStatement.Space), ‖ψ x‖ ≤ C

A test function vanishing at infinity is bounded.

theorem NavierStokesR3.WeakTimeContinuity.integrable_pairing_of_bounded {f : ProblemStatement.Space → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) (hbound : ∃ (C : ℝ), ∀ (x : ProblemStatement.Space), ‖ψ x‖ ≤ C) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f x) * ψ x) MeasureTheory.volume

Pairing an L¹ scalar field with a bounded continuous complex test is integrable.

theorem NavierStokesR3.WeakTimeContinuity.integrable_pairing {f : ProblemStatement.Space → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) (hψzero : Filter.Tendsto ψ (Filter.cocompact ProblemStatement.Space) (nhds 0)) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f x) * ψ x) MeasureTheory.volume

The original, untruncated pairing is a genuine Bochner integral.

noncomputable def NavierStokesR3.WeakTimeContinuity.cutoffTest (R : ℝ) (ψ : ProblemStatement.Space → ℂ) (x : ProblemStatement.Space) : ℂ

The compact approximation to the spatial test.

Equations

• NavierStokesR3.WeakTimeContinuity.cutoffTest R ψ x = ↑(NavierStokesR3.ComparisonCutoffs.cutoff R x) * ψ x

theorem NavierStokesR3.WeakTimeContinuity.cutoffTest_continuous {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) (R : ℝ) : Continuous (cutoffTest R ψ)

theorem NavierStokesR3.WeakTimeContinuity.norm_cutoffTest_le (R : ℝ) (ψ : ProblemStatement.Space → ℂ) (x : ProblemStatement.Space) : ‖cutoffTest R ψ x‖ ≤ ‖ψ x‖

theorem NavierStokesR3.WeakTimeContinuity.integrable_cutoff_pairing {f : ProblemStatement.Space → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) (hψzero : Filter.Tendsto ψ (Filter.cocompact ProblemStatement.Space) (nhds 0)) (R : ℝ) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f x) * cutoffTest R ψ x) MeasureTheory.volume

theorem NavierStokesR3.WeakTimeContinuity.norm_sub_cutoffTest_le (R : ℝ) (ψ : ProblemStatement.Space → ℂ) (x : ProblemStatement.Space) : ‖ψ x - cutoffTest R ψ x‖ ≤ ‖ψ x‖

Cutting off the test cannot enlarge its pointwise error beyond its norm.

theorem NavierStokesR3.WeakTimeContinuity.tendstoUniformly_cutoffTest {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) (hψzero : Filter.Tendsto ψ (Filter.cocompact ProblemStatement.Space) (nhds 0)) : TendstoUniformly (fun (R : ℝ) => cutoffTest R ψ) ψ Filter.atTop

The compact approximations converge uniformly on all of space.

theorem NavierStokesR3.WeakTimeContinuity.norm_pairing_sub_le {f : ProblemStatement.Space → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {ψ φ : ProblemStatement.Space → ℂ} (hψ : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f x) * ψ x) MeasureTheory.volume) (hφ : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f x) * φ x) MeasureTheory.volume) {ε : ℝ} (herror : ∀ (x : ProblemStatement.Space), ‖ψ x - φ x‖ ≤ ε) : ‖(∫ (x : ProblemStatement.Space), ↑(f x) * ψ x) - ∫ (x : ProblemStatement.Space), ↑(f x) * φ x‖ ≤ ε * ∫ (x : ProblemStatement.Space), ‖f x‖

Uniform error in the test controls error in its pairing by the L¹ norm of the scalar field.

theorem NavierStokesR3.WeakTimeContinuity.continuousOn_cutoff_pairing {s : Set ℝ} {g : ProblemStatement.SpaceTime → ℝ} (hg : ContinuousOn g (s ×ˢ Set.univ)) {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) {R : ℝ} (hR : 0 < R) : ContinuousOn (fun (t : ℝ) => ∫ (x : ProblemStatement.Space), ↑(g (t, x)) * cutoffTest R ψ x) s

Compactly truncated pairings are continuous on an arbitrary time set.

theorem NavierStokesR3.WeakTimeContinuity.continuousOn_pairing {s : Set ℝ} {g : ProblemStatement.SpaceTime → ℝ} {M : ℝ} (hg : ContinuousOn g (s ×ˢ Set.univ)) (hints : ∀ t ∈ s, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => g (t, x)) MeasureTheory.volume) (hbound : ∀ t ∈ s, ∫ (x : ProblemStatement.Space), ‖g (t, x)‖ ≤ M) {ψ : ProblemStatement.Space → ℂ} (hψ : Continuous ψ) (hψzero : Filter.Tendsto ψ (Filter.cocompact ProblemStatement.Space) (nhds 0)) : ContinuousOn (fun (t : ℝ) => ∫ (x : ProblemStatement.Space), ↑(g (t, x)) * ψ x) s

Uniform spatial L¹ bounds upgrade compact-test continuity to continuity for every continuous test vanishing at infinity.

Pressure recovery for smooth finite-energy comparisons

The physical pressure is tested only against compact smooth functions. Its canonical representative is recovered from the conservative equation, time averaging, and the vanishing theorem for harmonic Sobolev-bounded functionals.

Time averages of finite-energy fields

These averages use the ordinary Bochner integral on a finite closed time interval. Their spatial integrability follows from joint continuity and the uniform spatial integral bounds; no time derivative or global spatial derivative bound is used.

noncomputable def NavierStokesR3.Comparison.timeAverage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (a : ℝ → ℝ) (f : ProblemStatement.SpaceTime → E) (x : ProblemStatement.Space) : E

The time average against a scalar weight on the comparison interval.

Equations

• NavierStokesR3.Comparison.timeAverage T a f x = ∫ (t : ℝ) in Set.Icc 0 T, a t • f (t, x)

theorem NavierStokesR3.Comparison.aestronglyMeasurable_slab {E : Type u_1} [NormedAddCommGroup E] {T : ℝ} {f : ProblemStatement.SpaceTime → E} (hf : ContinuousOn f (slab 0 T)) : MeasureTheory.AEStronglyMeasurable f ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)

Joint continuity supplies measurability for the product of restricted time measure and ordinary spatial volume.

theorem NavierStokesR3.Comparison.integrable_slab_of_integral_norm_le {E : Type u_1} [NormedAddCommGroup E] {T : ℝ} {f : ProblemStatement.SpaceTime → E} {B : ℝ → ℝ} (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => f (t, x)) MeasureTheory.volume) (hB : MeasureTheory.IntegrableOn B (Set.Icc 0 T) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ≤ B t) : MeasureTheory.Integrable f ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)

An integrable bound on the spatial norm integrals proves integrability on the whole slab.

theorem NavierStokesR3.Comparison.continuousOn_time_weight {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) : ContinuousOn (fun (z : ProblemStatement.SpaceTime) => a z.1 • f z) (slab 0 T)

Weighting by a continuous scalar preserves slab continuity.

theorem NavierStokesR3.Comparison.timeAverage_timeSlice_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (x : ProblemStatement.Space) : MeasureTheory.IntegrableOn (fun (t : ℝ) => a t • f (t, x)) (Set.Icc 0 T) MeasureTheory.volume

Each time slice at a fixed spatial point is integrable, including at the endpoints of the closed time interval.

theorem NavierStokesR3.Comparison.timeAverage_continuousLinearMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {T : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (L : E →L[ℝ] F) (x : ProblemStatement.Space) : timeAverage T a (fun (z : ProblemStatement.SpaceTime) => L (f z)) x = L (timeAverage T a f x)

Bounded linear maps commute with these time averages pointwise.

theorem NavierStokesR3.Comparison.timeAverage_integrand_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => f (t, x)) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ≤ M) : MeasureTheory.Integrable (fun (z : ProblemStatement.SpaceTime) => a z.1 • f z) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)

A field with a uniform spatial L¹ bound has an integrable weighted integrand on the time-space slab.

theorem NavierStokesR3.Comparison.timeAverage_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => f (t, x)) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ≤ M) : MeasureTheory.Integrable (timeAverage T a f) MeasureTheory.volume

The time average of a uniformly L¹ field lies in spatial L¹.

theorem NavierStokesR3.Comparison.timeAverage_norm_integral_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => f (t, x)) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ≤ M) : ∫ (x : ProblemStatement.Space), ‖timeAverage T a f x‖ ≤ M * ∫ (t : ℝ) in Set.Icc 0 T, ‖a t‖

The spatial L¹ norm of an average is bounded by the uniform spatial norm bound times the time integral of the weight's absolute value.

theorem NavierStokesR3.Comparison.integral_timeAverage_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => f (t, x)) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ≤ M) : ∫ (x : ProblemStatement.Space), timeAverage T a f x = ∫ (t : ℝ) in Set.Icc 0 T, a t • ∫ (x : ProblemStatement.Space), f (t, x)

Fubini for a uniformly L¹ field and a continuous time weight.

theorem NavierStokesR3.Comparison.norm_integral_sq_le_measure_mul_integral_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : α → E} (hf : MeasureTheory.MemLp f 2 μ) : ‖∫ (x : α), f x ∂μ‖ ^ 2 ≤ μ.real Set.univ * ∫ (x : α), ‖f x‖ ^ 2 ∂μ

Cauchy--Schwarz for a Bochner integral over a finite measure space.

theorem NavierStokesR3.Comparison.memLp_two_timeIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {f : ProblemStatement.SpaceTime → E} (hf : MeasureTheory.AEStronglyMeasurable f ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)) (hsq : MeasureTheory.Integrable (fun (z : ProblemStatement.SpaceTime) => ‖f z‖ ^ 2) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => ∫ (t : ℝ) in Set.Icc 0 T, f (t, x)) 2 MeasureTheory.volume

Integrating in the finite time variable sends a square-integrable joint field to a square-integrable spatial field.

theorem NavierStokesR3.Comparison.l2Sq_timeIntegral_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {f : ProblemStatement.SpaceTime → E} (hf : MeasureTheory.AEStronglyMeasurable f ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)) (hsq : MeasureTheory.Integrable (fun (z : ProblemStatement.SpaceTime) => ‖f z‖ ^ 2) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)) : (l2Sq fun (x : ProblemStatement.Space) => ∫ (t : ℝ) in Set.Icc 0 T, f (t, x)) ≤ (MeasureTheory.volume.restrict (Set.Icc 0 T)).real Set.univ * ∫ (t : ℝ) in Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ^ 2

The quantitative estimate behind square-integrability of the time integral.

theorem NavierStokesR3.Comparison.timeAverage_integrand_integrable_sq_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖f (t, x)‖ ^ 2) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ^ 2 ≤ M) : MeasureTheory.Integrable (fun (z : ProblemStatement.SpaceTime) => ‖a z.1 • f z‖ ^ 2) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)

Squared norm integrability of the weighted joint field follows from a uniform spatial square-integral bound.

theorem NavierStokesR3.Comparison.timeAverage_memLp_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖f (t, x)‖ ^ 2) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ^ 2 ≤ M) : MeasureTheory.MemLp (timeAverage T a f) 2 MeasureTheory.volume

The time average of a uniformly square-integrable field lies in spatial L².

theorem NavierStokesR3.Comparison.timeAverage_l2Sq_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} (hT : 0 ≤ T) (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖f (t, x)‖ ^ 2) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ^ 2 ≤ M) : l2Sq (timeAverage T a f) ≤ T * M * ∫ (t : ℝ) in Set.Icc 0 T, ‖a t‖ ^ 2

A quantitative square-integral estimate using only the time weight and the uniform spatial square-integral bound.

theorem NavierStokesR3.Comparison.timeAverage_memLp_two_of_uniformFiniteEnergy {T : ℝ} {a : ℝ → ℝ} {u : ProblemStatement.VelocityField} (ha : ContinuousOn a (Set.Icc 0 T)) (hu_cont : ContinuousOn u (slab 0 T)) (hu : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u) : MeasureTheory.MemLp (timeAverage T a u) 2 MeasureTheory.volume

Uniform finite kinetic energy gives square-integrability of every continuously weighted time average of a velocity.

theorem NavierStokesR3.Comparison.timeAverage_difference_memLp_two {T : ℝ} {a : ℝ → ℝ} {u v : ProblemStatement.VelocityField} (ha : ContinuousOn a (Set.Icc 0 T)) (hu_cont : ContinuousOn u (slab 0 T)) (hv_cont : ContinuousOn v (slab 0 T)) (hu : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u) (hv : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) v) : MeasureTheory.MemLp (timeAverage T a fun (z : ProblemStatement.SpaceTime) => u z - v z) 2 MeasureTheory.volume

In particular, the averaged difference of two finite-energy velocities belongs to spatial L². The weight can equally be a continuous derivative of a smooth time test function.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_component_l2Sq_bound {T : ℝ} {u : ProblemStatement.VelocityField} (hu_cont : ContinuousOn u (slab 0 T)) (hu : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u) (k : Fin 3) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖(u (t, x)).ofLp k‖ ^ 2) MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖(u (t, x)).ofLp k‖ ^ 2 ≤ M

A uniform finite-energy bound also bounds every scalar coordinate's ordinary spatial square integral.

theorem NavierStokesR3.Comparison.uniformFiniteEnergy_difference_component_l2Sq_bound {T : ℝ} {u v : ProblemStatement.VelocityField} (hu_cont : ContinuousOn u (slab 0 T)) (hv_cont : ContinuousOn v (slab 0 T)) (hu : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u) (hv : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) v) (k : Fin 3) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖(u (t, x) - v (t, x)).ofLp k‖ ^ 2) MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖(u (t, x) - v (t, x)).ofLp k‖ ^ 2 ≤ M

Coordinate square-integral bounds for the difference field.

theorem NavierStokesR3.Comparison.timeAverage_difference_component_memLp_two {T : ℝ} {a : ℝ → ℝ} {u v : ProblemStatement.VelocityField} (ha : ContinuousOn a (Set.Icc 0 T)) (hu_cont : ContinuousOn u (slab 0 T)) (hv_cont : ContinuousOn v (slab 0 T)) (hu : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u) (hv : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) v) (k : Fin 3) : MeasureTheory.MemLp (timeAverage T a fun (z : ProblemStatement.SpaceTime) => (u z - v z).ofLp k) 2 MeasureTheory.volume

A scalar coordinate of the averaged difference is in L², including when the continuous weight is a derivative of a time test function.

theorem NavierStokesR3.Comparison.continuousOn_tensorDiff_field {T : ℝ} {u v : ProblemStatement.VelocityField} (hu : ContinuousOn u (slab 0 T)) (hv : ContinuousOn v (slab 0 T)) (i j : Fin 3) : ContinuousOn (fun (z : ProblemStatement.SpaceTime) => tensorDiff u v z.1 i j z.2) (slab 0 T)

Each nonlinear tensor component is jointly continuous on the slab.

theorem NavierStokesR3.Comparison.timeAverage_tensorDiff_integrable {T : ℝ} {a : ℝ → ℝ} {u v : ProblemStatement.VelocityField} (ha : ContinuousOn a (Set.Icc 0 T)) (hu_cont : ContinuousOn u (slab 0 T)) (hv_cont : ContinuousOn v (slab 0 T)) (hu : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u) (hv : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) v) (i j : Fin 3) : MeasureTheory.Integrable (timeAverage T a fun (z : ProblemStatement.SpaceTime) => tensorDiff u v z.1 i j z.2) MeasureTheory.volume

Uniform finite kinetic energy gives spatial L¹ for each averaged nonlinear tensor component.

theorem NavierStokesR3.Comparison.l2_inner_integrable_and_norm_integral_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f g : ProblemStatement.Space → E} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => inner ℝ (f x) (g x)) MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖inner ℝ (f x) (g x)‖ ≤ l2Sq f + l2Sq g

A deliberately coarse bound for the L¹ norm of an L² pairing. It is sufficient for the Fubini argument and uses no pointwise bound on either field.

theorem NavierStokesR3.Comparison.timeAverage_inner_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → E} {ψ : ProblemStatement.Space → E} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖f (t, x)‖ ^ 2) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ^ 2 ≤ M) (hψcont : Continuous ψ) (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) : ∫ (x : ProblemStatement.Space), inner ℝ (ψ x) (timeAverage T a f x) = ∫ (t : ℝ) in Set.Icc 0 T, a t * ∫ (x : ProblemStatement.Space), inner ℝ (ψ x) (f (t, x))

The spatial L² pairing commutes with time averaging. Compact smooth spatial tests are covered as a special case of a continuous L² test.

theorem NavierStokesR3.Comparison.timeAverage_complex_mul (T : ℝ) (a : ℝ → ℝ) (f : ProblemStatement.SpaceTime → ℝ) (ψ : ProblemStatement.Space → ℂ) (x : ProblemStatement.Space) : timeAverage T a (fun (z : ProblemStatement.SpaceTime) => ↑(f z) * ψ z.2) x = ↑(timeAverage T a f x) * ψ x

A complex scalar spatial test factors out of the time integral.

theorem NavierStokesR3.Comparison.timeAverage_complex_pairing_of_integrable {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → ℝ} {ψ : ProblemStatement.Space → ℂ} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hψ : Continuous ψ) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f (t, x)) * ψ x) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖↑(f (t, x)) * ψ x‖ ≤ M) : ∫ (x : ProblemStatement.Space), ↑(timeAverage T a f x) * ψ x = ∫ (t : ℝ) in Set.Icc 0 T, ↑(a t) * ∫ (x : ProblemStatement.Space), ↑(f (t, x)) * ψ x

Fubini for a complex spatial test once the tested field has a uniform spatial L¹ bound.

theorem NavierStokesR3.Comparison.timeAverage_complex_pairing_of_bounded {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → ℝ} {ψ : ProblemStatement.Space → ℂ} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => f (t, x)) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ≤ M) (hψ : Continuous ψ) (hψbound : ∃ (C : ℝ), ∀ (x : ProblemStatement.Space), ‖ψ x‖ ≤ C) : ∫ (x : ProblemStatement.Space), ↑(timeAverage T a f x) * ψ x = ∫ (t : ℝ) in Set.Icc 0 T, ↑(a t) * ∫ (x : ProblemStatement.Space), ↑(f (t, x)) * ψ x

Uniformly L¹ real fields may be tested against every bounded continuous complex function before interchanging the time and spatial integrals.

theorem NavierStokesR3.Comparison.l2_complex_mul_integrable_and_norm_integral_le {f : ProblemStatement.Space → ℝ} {ψ : ProblemStatement.Space → ℂ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f x) * ψ x) MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖↑(f x) * ψ x‖ ≤ l2Sq f + l2Sq ψ

Spatial L² control makes a scalar field times a complex L² test integrable, with a coarse bound sufficient for Fubini.

theorem NavierStokesR3.Comparison.timeAverage_complex_pairing_of_memLp_two {T M : ℝ} {a : ℝ → ℝ} {f : ProblemStatement.SpaceTime → ℝ} {ψ : ProblemStatement.Space → ℂ} (ha : ContinuousOn a (Set.Icc 0 T)) (hf : ContinuousOn f (slab 0 T)) (hslice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖f (t, x)‖ ^ 2) MeasureTheory.volume) (hbound : ∀ t ∈ Set.Icc 0 T, ∫ (x : ProblemStatement.Space), ‖f (t, x)‖ ^ 2 ≤ M) (hψcont : Continuous ψ) (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) : ∫ (x : ProblemStatement.Space), ↑(timeAverage T a f x) * ψ x = ∫ (t : ℝ) in Set.Icc 0 T, ↑(a t) * ∫ (x : ProblemStatement.Space), ↑(f (t, x)) * ψ x

A uniformly square-integrable real field can be paired with a continuous complex L² spatial test before interchanging time and space.

Pointwise recovery from compact temporal tests

theorem NavierStokesR3.TemporalTestUniqueness.integral_eq_setIntegral {T : ℝ} {a : ℝ → ℝ} {f : ℝ → ℂ} (hs : tsupport a ⊆ Set.Ioo 0 T) : ∫ (t : ℝ), a t • f t = ∫ (t : ℝ) in Set.Icc 0 T, a t • f t

A compact temporal test supported in (0,T) has the same integral over [0,T] as over the line. No integrability of the untested function is needed.

theorem NavierStokesR3.TemporalTestUniqueness.eq_zero_on_Ioo_of_setIntegral_tests {T : ℝ} {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Ioo 0 T)) (htest : ∀ (a : ℝ → ℝ), ContDiff ℝ (↑⊤) a → HasCompactSupport a → tsupport a ⊆ Set.Ioo 0 T → ∫ (t : ℝ) in Set.Icc 0 T, a t • f t = 0) (t : ℝ) : t ∈ Set.Ioo 0 T → f t = 0

structure NavierStokesR3.PressureRecovery.Hypotheses (T : ℝ) (u v : NavierStokes.ProblemStatement.VelocityField) (p q : NavierStokes.ProblemStatement.PressureField) : Prop

These are exactly the local smooth equation and uniform finite-energy hypotheses of the comparison argument.

• positive : 0 < T
• smooth_u : ContDiffOn ℝ (↑⊤) u (Comparison.slab 0 T)
• smooth_v : ContDiffOn ℝ (↑⊤) v (Comparison.slab 0 T)
• smooth_p : ContDiffOn ℝ (↑⊤) p (Comparison.slab 0 T)
• smooth_q : ContDiffOn ℝ (↑⊤) q (Comparison.slab 0 T)
• div_u (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0
• div_v (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence v t x = 0
• equation (t : ℝ) : t ∈ Set.Ioo 0 T → ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = NavierStokes.ProblemStatement.navierStokesResidual v q t x
• energy_u : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u
• energy_v : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) v

noncomputable def NavierStokesR3.PressureRecovery.velocityAverage (T : ℝ) (a : ℝ → ℝ) (u v : NavierStokes.ProblemStatement.VelocityField) (k : Fin 3) : NavierStokes.ProblemStatement.Space → ℝ

Velocity average, given by timeAverage T a (fun z => (u - v) z k).

Equations

• NavierStokesR3.PressureRecovery.velocityAverage T a u v k = NavierStokesR3.Comparison.timeAverage T a fun (z : NavierStokesR3.ProblemStatement.SpaceTime) => ((u - v) z).ofLp k

noncomputable def NavierStokesR3.PressureRecovery.tensorAverage (T : ℝ) (a : ℝ → ℝ) (u v : NavierStokes.ProblemStatement.VelocityField) (i j : Fin 3) : NavierStokes.ProblemStatement.Space → ℝ

Tensor average, given by timeAverage T a (fun z => tensorDiff u v z.1 i j z.2).

Equations

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

theorem NavierStokesR3.PressureRecovery.continuous_deriv_of_smooth {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) : Continuous (deriv a)

theorem NavierStokesR3.PressureRecovery.Hypotheses.velocityAverage_memLp {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContinuousOn a (Set.Icc 0 T)) (k : Fin 3) : MeasureTheory.MemLp (velocityAverage T a u v k) 2 MeasureTheory.volume

theorem NavierStokesR3.PressureRecovery.Hypotheses.tensorAverage_integrable {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContinuousOn a (Set.Icc 0 T)) (i j : Fin 3) : MeasureTheory.Integrable (tensorAverage T a u v i j) MeasureTheory.volume

theorem NavierStokesR3.PressureRecovery.Hypotheses.tensor_bound {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), MeasureTheory.Integrable (Comparison.tensorDiff u v t i j) MeasureTheory.volume ∧ ∫ (x : ProblemStatement.Space), ‖Comparison.tensorDiff u v t i j x‖ ≤ M

theorem NavierStokesR3.PressureRecovery.velocityAverage_pairing {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContinuousOn a (Set.Icc 0 T)) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), velocityAverage T a u v k x * ψ x = ∫ (t : ℝ) in Set.Icc 0 T, a t * ∫ (x : NavierStokes.ProblemStatement.Space), ((u - v) (t, x)).ofLp k * ψ x

theorem NavierStokesR3.PressureRecovery.tensorAverage_pairing {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContinuousOn a (Set.Icc 0 T)) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (i j : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), tensorAverage T a u v i j x * ψ x = ∫ (t : ℝ) in Set.Icc 0 T, a t * ∫ (x : ProblemStatement.Space), Comparison.tensorDiff u v t i j x * ψ x

theorem NavierStokesR3.PressureRecovery.pressurePair_tensorAverage {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContinuousOn a (Set.Icc 0 T)) (i j : Fin 3) (ψ : Comparison.ComplexTest) : Comparison.pressurePair i j (tensorAverage T a u v i j) ψ = ∫ (t : ℝ) in Set.Icc 0 T, ↑(a t) * Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ψ

Fubini for the actual canonical pressure pairing. The Riesz test is bounded, so the uniform tensor L¹ bound controls the whole product.

theorem NavierStokesR3.PressureRecovery.noncanonical_average_identity {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ((∫ (x : NavierStokes.ProblemStatement.Space), ↑(velocityAverage T a u v k x) * (HarmonicTestFunctionals.laplacianCLM (realTest ψ hψ hcψ)) x) + ∫ (x : NavierStokes.ProblemStatement.Space), ↑(velocityAverage T (deriv a) u v k x) * (realTest ψ hψ hcψ) x) + ∑ i : Fin 3, ∫ (x : NavierStokes.ProblemStatement.Space), ↑(tensorAverage T a u v k i x) * ((HarmonicTestFunctionals.partialCLM i) (realTest ψ hψ hcψ)) x = ↑(∫ (t : ℝ) in Set.Icc 0 T, a t * ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ψ x)

theorem NavierStokesR3.PressureRecovery.averaged_value_realTest {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : PressureFunctionals.averagedPressureDifferenceValue (velocityAverage T a u v k) (velocityAverage T (deriv a) u v k) (tensorAverage T a u v) k (realTest ψ hψ hcψ) = ↑(∫ (t : ℝ) in Set.Icc 0 T, a t * ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ψ x) + ∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (tensorAverage T a u v i j) ((HarmonicTestFunctionals.partialCLM k) (realTest ψ hψ hcψ))

theorem NavierStokesR3.PressureRecovery.averaged_gradient_poisson {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ∫ (t : ℝ) in Set.Icc 0 T, a t * ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ConservativeDifference.scalarLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : NavierStokes.ProblemStatement.Space), tensorAverage T a u v i j x * NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial j (NavierStokes.SolutionDifference.spatialPartial k ψ)) x

Averaging the differentiated Poisson equation commutes with each compact tensor pairing. All derivatives remain on the compact test.

theorem NavierStokesR3.PressureRecovery.averaged_gradient_poisson_complex {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ↑(∫ (t : ℝ) in Set.Icc 0 T, a t * ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ConservativeDifference.scalarLaplacian ψ x) = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : NavierStokes.ProblemStatement.Space), ↑(tensorAverage T a u v i j x) * ((HarmonicTestFunctionals.partialCLM i) ((HarmonicTestFunctionals.partialCLM j) ((HarmonicTestFunctionals.partialCLM k) (realTest ψ hψ hcψ)))) x

theorem NavierStokesR3.PressureRecovery.averaged_value_real_harmonic {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : PressureFunctionals.averagedPressureDifferenceValue (velocityAverage T a u v k) (velocityAverage T (deriv a) u v k) (tensorAverage T a u v) k (HarmonicTestFunctionals.laplacianCLM (realTest ψ hψ hcψ)) = 0

The averaged physical-minus-canonical pressure-gradient functional is harmonic on every compact real test, by the two actual Poisson identities.

theorem NavierStokesR3.PressureRecovery.averaged_value_zero {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) (k : Fin 3) (ψ : Comparison.ComplexTest) : PressureFunctionals.averagedPressureDifferenceValue (velocityAverage T a u v k) (velocityAverage T (deriv a) u v k) (tensorAverage T a u v) k ψ = 0

The genuine H³ bound and compact harmonicity force the whole averaged functional to vanish. No representative of the physical pressure on Schwartz tests has been introduced.

theorem NavierStokesR3.PressureRecovery.pressurePair_continuousOn {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) (i j : Fin 3) (ψ : Comparison.ComplexTest) : ContinuousOn (fun (t : ℝ) => Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ψ) (Set.Icc 0 T)

The uniform tensor bound and spatial decay of a Riesz test give continuity of its canonical pairing in time, including the slab endpoints.

theorem NavierStokesR3.PressureRecovery.canonical_sum_continuousOn {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) (ψ : Comparison.ComplexTest) : ContinuousOn (fun (t : ℝ) => ∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ψ) (Set.Icc 0 T)

theorem NavierStokesR3.PressureRecovery.canonical_sum_timeAverage {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContinuousOn a (Set.Icc 0 T)) (ψ : Comparison.ComplexTest) : ∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (tensorAverage T a u v i j) ψ = ∫ (t : ℝ) in Set.Icc 0 T, ↑(a t) * ∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ψ

theorem NavierStokesR3.PressureRecovery.time_test_gradient_difference_zero {T : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hsupp : tsupport a ⊆ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ) (k : Fin 3) : ∫ (t : ℝ) in Set.Icc 0 T, a t • (↑(∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial k (fun (y : NavierStokes.ProblemStatement.Space) => (p - q) (t, y)) x * ψ x) + ∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ((HarmonicTestFunctionals.partialCLM k) (realTest ψ hψ hcψ))) = 0

Every compact temporal test annihilates the difference between the physical and canonical pressure gradients, at a fixed compact spatial test.

theorem NavierStokesR3.PressureRecovery.gradient_recovery_complex {T t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) (ht : t ∈ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (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) = -∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ((HarmonicTestFunctionals.partialCLM k) (realTest ψ hψ hcψ))

Actual pressure-gradient recovery at every interior time. This equality is obtained from the equation and uniform finite energy, rather than assumed as a pressure normalization.

theorem NavierStokesR3.PressureRecovery.gradient_recovery {T t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : Hypotheses T u v p q) (ht : t ∈ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (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 = -(∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ((HarmonicTestFunctionals.partialCLM k) (realTest ψ hψ hcψ))).re

theorem NavierStokesR3.PressureRecovery.pressure_gradient_recovery {T t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (hT : 0 < T) (hu : ContDiffOn ℝ (↑⊤) u (Comparison.slab 0 T)) (hv : ContDiffOn ℝ (↑⊤) v (Comparison.slab 0 T)) (hp : ContDiffOn ℝ (↑⊤) p (Comparison.slab 0 T)) (hq : ContDiffOn ℝ (↑⊤) q (Comparison.slab 0 T)) (hdivu : ∀ s ∈ Set.Ioo 0 T, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u s x = 0) (hdivv : ∀ s ∈ Set.Ioo 0 T, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence v s x = 0) (hNS : ∀ s ∈ Set.Ioo 0 T, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p s x = NavierStokes.ProblemStatement.navierStokesResidual v q s x) (heu : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) u) (hev : ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) v) (ht : t ∈ Set.Ioo 0 T) {ψ : NavierStokes.ProblemStatement.Space → ℝ} (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 = -∑ i : Fin 3, ∑ j : Fin 3, (Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) ((HarmonicTestFunctionals.partialCLM k) (realTest ψ hψ hcψ))).re

The explicit comparison-hypothesis form of pressure recovery. Only the spatial test is compactly supported; both velocities and both pressures are allowed on all of Euclidean space.

The compact test function in the pressure flux

The identity φ² r = D(φ⁸)[w] places the localized pressure flux in the commutator form. Its estimates use only the unweighted velocity energy and the weighted velocity and gradient norms.

noncomputable def NavierStokesR3.PressureFluxTest.r (φ : ProblemStatement.Space → ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ℝ

The scalar test function for the pressure commutator.

Equations

• NavierStokesR3.PressureFluxTest.r φ w x = 8 * φ x ^ 5 * (fderiv ℝ φ x) (w x)

theorem NavierStokesR3.PressureFluxTest.multiplier_r_eq_weight_deriv {φ : ProblemStatement.Space → ℝ} (w : ProblemStatement.Space → ProblemStatement.Space) {x : ProblemStatement.Space} (hφ : DifferentiableAt ℝ φ x) : φ x ^ 2 * r φ w x = (fderiv ℝ (fun (y : ProblemStatement.Space) => φ y ^ 8) x) (w x)

theorem NavierStokesR3.PressureFluxTest.r_smooth {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hw : ContDiff ℝ (↑⊤) w) : ContDiff ℝ (↑⊤) (r φ w)

theorem NavierStokesR3.PressureFluxTest.r_hasCompactSupport {φ : ProblemStatement.Space → ℝ} (hs : HasCompactSupport φ) (w : ProblemStatement.Space → ProblemStatement.Space) : HasCompactSupport (r φ w)

theorem NavierStokesR3.PressureFluxTest.memLp_r {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ (↑⊤) w) (p : ENNReal) : MeasureTheory.MemLp (r φ w) p MeasureTheory.volume

theorem NavierStokesR3.PressureFluxTest.memLp_fderiv_r {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ (↑⊤) w) (p : ENNReal) : MeasureTheory.MemLp (fderiv ℝ (r φ w)) p MeasureTheory.volume

theorem NavierStokesR3.PressureFluxTest.norm_r_le {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} {x : ProblemStatement.Space} (hφ0 : 0 ≤ φ x) (hφ1 : φ x ≤ 1) {L : ℝ} (hL0 : 0 ≤ L) (hL : ‖fderiv ℝ φ x‖ ≤ L) : ‖r φ w x‖ ≤ 8 * L * ‖φ x ^ 3 • w x‖

theorem NavierStokesR3.PressureFluxTest.memLp_and_lpNorm_r_four_le {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hφ1 : ∀ (x : ProblemStatement.Space), φ x ≤ 1) {L : ℝ} (hL0 : 0 ≤ L) (hL : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ φ x‖ ≤ L) : MeasureTheory.MemLp (r φ w) 4 MeasureTheory.volume ∧ Comparison.comparisonLpNorm 4 (r φ w) ≤ 8 * L * Comparison.comparisonLpNorm 2 w ^ (1 / 4) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ^ (3 / 4)

The test belongs to L⁴, with the exact endpoint interpolation exponents.

theorem NavierStokesR3.PressureFluxTest.norm_fderiv_r_le_raw {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hw : ContDiff ℝ (↑⊤) w) (x : ProblemStatement.Space) (hφ0 : 0 ≤ φ x) : ‖fderiv ℝ (r φ w) x‖ ≤ 8 * (φ x ^ 5 * ‖fderiv ℝ φ x‖ * ‖fderiv ℝ w x‖ + φ x ^ 5 * ‖fderiv ℝ (fderiv ℝ φ) x‖ * ‖w x‖ + 5 * φ x ^ 4 * ‖fderiv ℝ φ x‖ ^ 2 * ‖w x‖)

Product differentiation before replacing the cutoff derivative norms by constants.

theorem NavierStokesR3.PressureFluxTest.norm_fderiv_r_le_amplitude {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hw : ContDiff ℝ (↑⊤) w) (x : ProblemStatement.Space) (hφ0 : 0 ≤ φ x) (hφ1 : φ x ≤ 1) {L J : ℝ} (hL0 : 0 ≤ L) (hL : ‖fderiv ℝ φ x‖ ≤ L) (hJ : ‖fderiv ℝ (fderiv ℝ φ) x‖ ≤ J) : ‖fderiv ℝ (r φ w) x‖ ≤ 24 * L * WeightedSobolev.cutoffGradientAmplitude φ w x + (40 * L ^ 2 + 8 * J) * ‖w x‖

Only the weighted velocity derivative occurs in the pointwise bound.

theorem NavierStokesR3.PressureFluxTest.memLp_and_lpNorm_fderiv_r_two_le {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hφ1 : ∀ (x : ProblemStatement.Space), φ x ≤ 1) {L J : ℝ} (hL0 : 0 ≤ L) (hJ0 : 0 ≤ J) (hL : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ φ x‖ ≤ L) (hJ : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ (fderiv ℝ φ) x‖ ≤ J) : MeasureTheory.MemLp (fderiv ℝ (r φ w)) 2 MeasureTheory.volume ∧ Comparison.comparisonLpNorm 2 (fderiv ℝ (r φ w)) ≤ 24 * L * √(∫ (x : ProblemStatement.Space), φ x ^ 8 * Comparison.gradientSq w x) + (40 * L ^ 2 + 8 * J) * Comparison.comparisonLpNorm 2 w

The derivative is square integrable and controlled by weighted dissipation.

theorem NavierStokesR3.PressureFluxTest.lpNorm_fderiv_r_two_le {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ (↑⊤) φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hφ1 : ∀ (x : ProblemStatement.Space), φ x ≤ 1) {L J : ℝ} (hL0 : 0 ≤ L) (hJ0 : 0 ≤ J) (hL : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ φ x‖ ≤ L) (hJ : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ (fderiv ℝ φ) x‖ ≤ J) : Comparison.comparisonLpNorm 2 (fderiv ℝ (r φ w)) ≤ 40 * (L * √(∫ (x : ProblemStatement.Space), φ x ^ 8 * Comparison.gradientSq w x) + (L ^ 2 + J) * Comparison.comparisonLpNorm 2 w)

noncomputable def NavierStokesR3.PressureFluxTest.cutoffTest (R : ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) : ProblemStatement.Space → ℝ

The actual test at radius R in the fixed cutoff family.

Equations

• NavierStokesR3.PressureFluxTest.cutoffTest R w = NavierStokesR3.PressureFluxTest.r (NavierStokesR3.ComparisonCutoffs.cutoff R) w

theorem NavierStokesR3.PressureFluxTest.cutoffTest_flux_identity (R : ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ComparisonCutoffs.multiplier R x * cutoffTest R w x = (fderiv ℝ (ComparisonCutoffs.weight R) x) (w x)

theorem NavierStokesR3.PressureFluxTest.cutoffTest_smooth (R : ℝ) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) : ContDiff ℝ (↑⊤) (cutoffTest R w)

theorem NavierStokesR3.PressureFluxTest.cutoffTest_hasCompactSupport {R : ℝ} (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) : HasCompactSupport (cutoffTest R w)

theorem NavierStokesR3.PressureFluxTest.memLp_cutoffTest {R : ℝ} (hR : 0 < R) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (p : ENNReal) : MeasureTheory.MemLp (cutoffTest R w) p MeasureTheory.volume

theorem NavierStokesR3.PressureFluxTest.memLp_fderiv_cutoffTest {R : ℝ} (hR : 0 < R) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (p : ENNReal) : MeasureTheory.MemLp (fderiv ℝ (cutoffTest R w)) p MeasureTheory.volume

theorem NavierStokesR3.PressureFluxTest.cutoffTest_four_bound {R : ℝ} (hR : 0 < R) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) : MeasureTheory.MemLp (cutoffTest R w) 4 MeasureTheory.volume ∧ Comparison.comparisonLpNorm 4 (cutoffTest R w) ≤ 8 * ComparisonCutoffs.derivativeConstant 1 / R * Comparison.comparisonLpNorm 2 w ^ (1 / 4) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => ComparisonCutoffs.cutoff R x ^ 4 • w x) ^ (3 / 4)

noncomputable def NavierStokesR3.PressureFluxTest.cutoffDerivativeConstant : ℝ

A fixed constant for the derivative bound of the pressure test.

Equations

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

theorem NavierStokesR3.PressureFluxTest.cutoffDerivativeConstant_pos : 0 < cutoffDerivativeConstant

theorem NavierStokesR3.PressureFluxTest.cutoffTest_derivative_bound {R : ℝ} (hR : 0 < R) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) : MeasureTheory.MemLp (fderiv ℝ (cutoffTest R w)) 2 MeasureTheory.volume ∧ Comparison.comparisonLpNorm 2 (fderiv ℝ (cutoffTest R w)) ≤ cutoffDerivativeConstant / R * √(∫ (x : ProblemStatement.Space), ComparisonCutoffs.cutoff R x ^ 8 * Comparison.gradientSq w x) + cutoffDerivativeConstant / R ^ 2 * Comparison.comparisonLpNorm 2 w

The actual pressure flux equals the canonical pressure flux

The scalar gradient identification is supplied by the proved pressure recovery theorem. The only compact support in this identity is that of the cutoff.

From scalar pressure-gradient identification to the cutoff pressure flux

This module is an integration-by-parts bridge. Its input is an explicit identification of every compact scalar pressure-gradient pairing. It does not assume a pressure-flux formula or any bound on the pressure at infinity.

theorem NavierStokesR3.PressureFluxIdentity.fluxFunction_smooth {χ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => (fderiv ℝ χ x) (w x)

theorem NavierStokesR3.PressureFluxIdentity.fluxFunction_hasCompactSupport {χ : ProblemStatement.Space → ℝ} (hcχ : HasCompactSupport χ) (w : ProblemStatement.Space → ProblemStatement.Space) : HasCompactSupport fun (x : ProblemStatement.Space) => (fderiv ℝ χ x) (w x)

theorem NavierStokesR3.PressureFluxIdentity.integrable_pressure_flux {χ π : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hπ : ContDiff ℝ (↑⊤) π) (hw : ContDiff ℝ (↑⊤) w) (hcχ : HasCompactSupport χ) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => π x * (fderiv ℝ χ x) (w x)) MeasureTheory.volume

def NavierStokesR3.PressureFluxIdentity.weightedComponent (χ : ProblemStatement.Space → ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) (k : Fin 3) : ProblemStatement.Space → ℝ

The scalar compact test associated to one component of the weighted velocity.

Equations

• NavierStokesR3.PressureFluxIdentity.weightedComponent χ w k x = χ x * (w x).ofLp k

theorem NavierStokesR3.PressureFluxIdentity.weightedComponent_smooth {χ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) (k : Fin 3) : ContDiff ℝ (↑⊤) (weightedComponent χ w k)

theorem NavierStokesR3.PressureFluxIdentity.weightedComponent_hasCompactSupport {χ : ProblemStatement.Space → ℝ} (hcχ : HasCompactSupport χ) (w : ProblemStatement.Space → ProblemStatement.Space) (k : Fin 3) : HasCompactSupport (weightedComponent χ w k)

theorem NavierStokesR3.PressureFluxIdentity.sum_partial_weightedComponent {χ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) (hdiv : ∀ (x : ProblemStatement.Space), ∑ k : Fin 3, (Comparison.partialD k w x).ofLp k = 0) (x : ProblemStatement.Space) : ∑ k : Fin 3, Comparison.partialD k (weightedComponent χ w k) x = (fderiv ℝ χ x) (w x)

theorem NavierStokesR3.PressureFluxIdentity.sum_partial_realTest_weightedComponent {χ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) (hcχ : HasCompactSupport χ) (hdiv : ∀ (x : ProblemStatement.Space), ∑ k : Fin 3, (Comparison.partialD k w x).ofLp k = 0) : ∑ k : Fin 3, (HarmonicTestFunctionals.partialCLM k) (PressureRecovery.realTest (weightedComponent χ w k) ⋯ ⋯) = PressureRecovery.realTest (fun (x : ProblemStatement.Space) => (fderiv ℝ χ x) (w x)) ⋯ ⋯

The compact flux test is the sum of the differentiated component tests.

noncomputable def NavierStokesR3.PressureFluxIdentity.canonicalPressureLinear (g : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ) (hg : ∀ (i j : Fin 3), MeasureTheory.Integrable (g i j) MeasureTheory.volume) : Comparison.ComplexTest →ₗ[ℂ] ℂ

The sum of all canonical pressure pairings is a complex-linear functional.

Equations

• NavierStokesR3.PressureFluxIdentity.canonicalPressureLinear g hg = ∑ i : Fin 3, ∑ j : Fin 3, NavierStokesR3.PressureFunctionals.pressurePairLinear i j (g i j) ⋯

@[simp]

theorem NavierStokesR3.PressureFluxIdentity.canonicalPressureLinear_apply (g : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ) (hg : ∀ (i j : Fin 3), MeasureTheory.Integrable (g i j) MeasureTheory.volume) (ψ : Comparison.ComplexTest) : (canonicalPressureLinear g hg) ψ = ∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (g i j) ψ

theorem NavierStokesR3.PressureFluxIdentity.integrable_canonical_flux_terms {χ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) (hcχ : HasCompactSupport χ) {g : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ} (hg : ∀ (i j : Fin 3), MeasureTheory.Integrable (g i j) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(g i j x) * Comparison.rieszTest i j (PressureRecovery.realTest (fun (y : ProblemStatement.Space) => (fderiv ℝ χ y) (w y)) ⋯ ⋯) x) MeasureTheory.volume

theorem NavierStokesR3.PressureFluxIdentity.pressure_flux_eq_of_gradient_identification {π χ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} {g : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ} (hπ : ContDiff ℝ (↑⊤) π) (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) (hcχ : HasCompactSupport χ) (hg : ∀ (i j : Fin 3), MeasureTheory.Integrable (g i j) MeasureTheory.volume) (hdiv : ∀ (x : ProblemStatement.Space), ∑ k : Fin 3, (Comparison.partialD k w x).ofLp k = 0) (hgrad : ∀ (k : Fin 3) (ψ : ProblemStatement.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hcψ : HasCompactSupport ψ), ∫ (x : ProblemStatement.Space), Comparison.partialD k π x * ψ x = -(∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (g i j) ((HarmonicTestFunctionals.partialCLM k) (PressureRecovery.realTest ψ hψ hcψ))).re) : ∫ (x : ProblemStatement.Space), π x * (fderiv ℝ χ x) (w x) = (∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (g i j) (PressureRecovery.realTest (fun (x : ProblemStatement.Space) => (fderiv ℝ χ x) (w x)) ⋯ ⋯)).re

Compact integration by parts turns the given scalar pressure-gradient identification into the actual cutoff pressure flux.

theorem NavierStokesR3.ActualPressureFlux.difference_slice_smooth {T t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : PressureRecovery.Hypotheses T u v p q) (ht : t ∈ Set.Ioo 0 T) : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)

theorem NavierStokesR3.ActualPressureFlux.actual_pressure_flux_integrable {T t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : PressureRecovery.Hypotheses T u v p q) (ht : t ∈ Set.Ioo 0 T) {χ : NavierStokes.ProblemStatement.Space → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hcχ : HasCompactSupport χ) : MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => (p - q) (t, x) * (fderiv ℝ χ x) ((u - v) (t, x))) MeasureTheory.volume

theorem NavierStokesR3.ActualPressureFlux.pressure_flux_eq_canonical {T t : ℝ} {u v : NavierStokes.ProblemStatement.VelocityField} {p q : NavierStokes.ProblemStatement.PressureField} (H : PressureRecovery.Hypotheses T u v p q) (ht : t ∈ Set.Ioo 0 T) {χ : NavierStokes.ProblemStatement.Space → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hcχ : HasCompactSupport χ) : ∫ (x : NavierStokes.ProblemStatement.Space), (p - q) (t, x) * (fderiv ℝ χ x) ((u - v) (t, x)) = (∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) (PressureRecovery.realTest (fun (x : NavierStokes.ProblemStatement.Space) => (fderiv ℝ χ x) ((u - v) (t, x))) ⋯ ⋯)).re

The pressure flux of the actual difference equation has the canonical Riesz-pairing representation, with no additional pressure hypothesis.

Weighted tensor bounds for the localized pressure

The tensor difference is expanded around the reference velocity. Its two cross terms use L³ of that velocity and L² of the difference; the quadratic term uses the cutoff interpolation estimate. All norms remain finite explicitly.

theorem NavierStokesR3.LocalizedTensorBounds.scalar_product_bound {p q r : ENNReal} [p.HolderTriple q r] {f g : ProblemStatement.Space → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g q MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => f x * g x) r MeasureTheory.volume ∧ (Comparison.comparisonLpNorm r fun (x : ProblemStatement.Space) => f x * g x) ≤ Comparison.comparisonLpNorm p f * Comparison.comparisonLpNorm q g

Scalar Hölder with finite real-valued norms.

theorem NavierStokesR3.LocalizedTensorBounds.cross_norm_bound {u w : ProblemStatement.Space → ProblemStatement.Space} (hu : MeasureTheory.MemLp u 3 MeasureTheory.volume) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => ‖u x‖ * ‖w x‖) (6 / 5) MeasureTheory.volume ∧ (Comparison.comparisonLpNorm (6 / 5) fun (x : ProblemStatement.Space) => ‖u x‖ * ‖w x‖) ≤ Comparison.comparisonLpNorm 3 u * Comparison.comparisonLpNorm 2 w

The scalar product of the two vector magnitudes belongs to L^(6/5).

theorem NavierStokesR3.LocalizedTensorBounds.quadratic_cutoff_bound {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφm : MeasureTheory.AEStronglyMeasurable φ MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hweighted : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) 6 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => ‖φ x • w x‖ ^ 2) (6 / 5) MeasureTheory.volume ∧ (Comparison.comparisonLpNorm (6 / 5) fun (x : ProblemStatement.Space) => ‖φ x • w x‖ ^ 2) ≤ Comparison.comparisonLpNorm 2 w ^ (3 / 2) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ^ (1 / 2)

The quadratic weighted difference has the endpoint interpolation bound.

theorem NavierStokesR3.LocalizedTensorBounds.tensorDiff_eq (u v : ProblemStatement.VelocityField) (t : ℝ) (i j : Fin 3) (x : ProblemStatement.Space) : Comparison.tensorDiff u v t i j x = (u (t, x)).ofLp i * ((u - v) (t, x)).ofLp j + ((u - v) (t, x)).ofLp i * (u (t, x)).ofLp j - ((u - v) (t, x)).ofLp i * ((u - v) (t, x)).ofLp j

The tensor identity uses the actual difference of the two velocities.

theorem NavierStokesR3.LocalizedTensorBounds.continuous_component {f : ProblemStatement.Space → ProblemStatement.Space} (hf : Continuous f) (i : Fin 3) : Continuous fun (x : ProblemStatement.Space) => (f x).ofLp i

theorem NavierStokesR3.LocalizedTensorBounds.continuous_tensorDiff {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : Continuous fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : Continuous fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (i j : Fin 3) : Continuous (Comparison.tensorDiff u v t i j)

theorem NavierStokesR3.LocalizedTensorBounds.norm_weighted_tensorDiff_le (u v : ProblemStatement.VelocityField) (t : ℝ) (i j : Fin 3) (x : ProblemStatement.Space) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : ‖s ^ 2 * Comparison.tensorDiff u v t i j x‖ ≤ 2 * (‖u (t, x)‖ * ‖(u - v) (t, x)‖) + ‖s • (u - v) (t, x)‖ ^ 2

Pointwise domination is uniform in both tensor indices.

theorem NavierStokesR3.LocalizedTensorBounds.weighted_tensorDiff_memLp {φ : ProblemStatement.Space → ℝ} {u v : ProblemStatement.VelocityField} {t : ℝ} (hφ : Continuous φ) (hs : HasCompactSupport φ) (hu : Continuous fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : Continuous fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (i j : Fin 3) (p : ENNReal) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 2 * Comparison.tensorDiff u v t i j x) p MeasureTheory.volume

Compactness supplies finite weighted tensor norms without any growth assumption on either velocity.

theorem NavierStokesR3.LocalizedTensorBounds.weighted_tensorDiff_bound {φ : ProblemStatement.Space → ℝ} {u v : ProblemStatement.VelocityField} {t : ℝ} (hφ : Continuous φ) (hs : HasCompactSupport φ) (hu : Continuous fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : Continuous fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (hw2 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)) 2 MeasureTheory.volume) (hu3 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) 3 MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hφ1 : ∀ (x : ProblemStatement.Space), φ x ≤ 1) (i j : Fin 3) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ 2 * Comparison.tensorDiff u v t i j x) (6 / 5) MeasureTheory.volume ∧ (Comparison.comparisonLpNorm (6 / 5) fun (x : ProblemStatement.Space) => φ x ^ 2 * Comparison.tensorDiff u v t i j x) ≤ (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ^ (3 / 2) * Comparison.cutoffL6 φ (u - v) t ^ (1 / 2) + (2 * Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) * Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => u (t, x)

The weighted tensor estimate used by the localized pressure argument. It has the same constant for every pair of indices.

theorem NavierStokesR3.PressureFlux.lpNorm_ofReal (p : ENNReal) (f : ProblemStatement.Space → ℝ) : (Comparison.comparisonLpNorm p fun (x : ProblemStatement.Space) => ↑(f x)) = Comparison.comparisonLpNorm p f

theorem NavierStokesR3.PressureFlux.norm_fderiv_ofReal {f : ProblemStatement.Space → ℝ} {x : ProblemStatement.Space} (hf : DifferentiableAt ℝ f x) : ‖fderiv ℝ (fun (y : ProblemStatement.Space) => ↑(f y)) x‖ = ‖fderiv ℝ f x‖

theorem NavierStokesR3.PressureFlux.lpNorm_fderiv_realTest (p : ENNReal) (f : ProblemStatement.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : Comparison.comparisonLpNorm p (fderiv ℝ fun (x : ProblemStatement.Space) => (PressureRecovery.realTest f hf hc) x) = Comparison.comparisonLpNorm p (fderiv ℝ f)

theorem NavierStokesR3.PressureFlux.cutoff_lipschitz {R : ℝ} (hR : 0 < R) (x y : ProblemStatement.Space) : |ComparisonCutoffs.cutoff R x - ComparisonCutoffs.cutoff R y| ≤ ComparisonCutoffs.derivativeConstant 1 / R * ‖x - y‖

theorem NavierStokesR3.PressureFlux.integrable_holder_pair {f : ProblemStatement.Space → ℝ} {g : ProblemStatement.Space → ℂ} (hf : MeasureTheory.MemLp f (6 / 5) MeasureTheory.volume) (hg : MeasureTheory.MemLp g 6 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(f x) * g x) MeasureTheory.volume

theorem NavierStokesR3.PressureFlux.norm_holder_pair_le {f : ProblemStatement.Space → ℝ} {g : ProblemStatement.Space → ℂ} (hf : MeasureTheory.MemLp f (6 / 5) MeasureTheory.volume) (hg : MeasureTheory.MemLp g 6 MeasureTheory.volume) : ‖∫ (x : ProblemStatement.Space), ↑(f x) * g x‖ ≤ Comparison.comparisonLpNorm (6 / 5) f * Comparison.comparisonLpNorm 6 g

noncomputable def NavierStokesR3.PressureFlux.fluxFunction (χ : ProblemStatement.Space → ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ℝ

The scalar test in the localized pressure flux.

Equations

• NavierStokesR3.PressureFlux.fluxFunction χ w x = (fderiv ℝ χ x) (w x)

theorem NavierStokesR3.PressureFlux.fluxFunction_smooth {χ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hχ : ContDiff ℝ (↑⊤) χ) (hw : ContDiff ℝ (↑⊤) w) : ContDiff ℝ (↑⊤) (fluxFunction χ w)

theorem NavierStokesR3.PressureFlux.fluxFunction_compact {χ : ProblemStatement.Space → ℝ} (hc : HasCompactSupport χ) (w : ProblemStatement.Space → ProblemStatement.Space) : HasCompactSupport (fluxFunction χ w)

noncomputable def NavierStokesR3.PressureFlux.canonicalFlux (g : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ) (f : ProblemStatement.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : ℂ

The raw complex canonical pairing, with no pressure function selected.

Equations

• NavierStokesR3.PressureFlux.canonicalFlux g f hf hc = ∑ i : Fin 3, ∑ j : Fin 3, NavierStokesR3.Comparison.pressurePair i j (g i j) (NavierStokesR3.PressureRecovery.realTest f hf hc)

theorem NavierStokesR3.PressureFlux.canonical_pair_integrable (g : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ) (f : ProblemStatement.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) (hg : ∀ (i j : Fin 3), MeasureTheory.Integrable (g i j) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(g i j x) * Comparison.rieszTest i j (PressureRecovery.realTest f hf hc) x) MeasureTheory.volume

theorem NavierStokesR3.PressureFlux.norm_canonicalFlux_le {g : Fin 3 → Fin 3 → ProblemStatement.Space → ℝ} {f : ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) {C : ℝ} (hbound : ∀ (i j : Fin 3), ‖Comparison.pressurePair i j (g i j) (PressureRecovery.realTest f hf hc)‖ ≤ C) : ‖canonicalFlux g f hf hc‖ ≤ 9 * C

noncomputable def NavierStokesR3.PressureFlux.rTest (R : ℝ) (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) (hw : ContDiff ℝ (↑⊤) w) : Comparison.ComplexTest

The compact Schwartz test used on the uncommuted side of the Riesz operator.

Equations

• NavierStokesR3.PressureFlux.rTest R hR w hw = NavierStokesR3.PressureRecovery.realTest (NavierStokesR3.PressureFluxTest.cutoffTest R w) ⋯ ⋯

noncomputable def NavierStokesR3.PressureFlux.fluxTest (R : ℝ) (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) (hw : ContDiff ℝ (↑⊤) w) : Comparison.ComplexTest

The actual flux test Dχ_R[w], represented in the Schwartz space.

Equations

• NavierStokesR3.PressureFlux.fluxTest R hR w hw = NavierStokesR3.PressureRecovery.realTest (NavierStokesR3.PressureFlux.fluxFunction (NavierStokesR3.ComparisonCutoffs.weight R) w) ⋯ ⋯

@[simp]

theorem NavierStokesR3.PressureFlux.rTest_apply (R : ℝ) (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) (hw : ContDiff ℝ (↑⊤) w) (x : ProblemStatement.Space) : (rTest R hR w hw) x = ↑(PressureFluxTest.cutoffTest R w x)

@[simp]

theorem NavierStokesR3.PressureFlux.fluxTest_apply (R : ℝ) (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) (hw : ContDiff ℝ (↑⊤) w) (x : ProblemStatement.Space) : (fluxTest R hR w hw) x = ↑((fderiv ℝ (ComparisonCutoffs.weight R) x) (w x))

theorem NavierStokesR3.PressureFlux.fluxTest_eq_multiplier_rTest (R : ℝ) (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) (hw : ContDiff ℝ (↑⊤) w) (x : ProblemStatement.Space) : (fluxTest R hR w hw) x = ComparisonCutoffs.cutoff R x ^ 2 • (rTest R hR w hw) x

theorem NavierStokesR3.PressureFlux.lpNorm_rTest (R : ℝ) (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) (hw : ContDiff ℝ (↑⊤) w) (p : ENNReal) : Comparison.comparisonLpNorm p ⇑(rTest R hR w hw) = Comparison.comparisonLpNorm p (PressureFluxTest.cutoffTest R w)

theorem NavierStokesR3.PressureFlux.lpNorm_fderiv_rTest (R : ℝ) (hR : 0 < R) (w : ProblemStatement.Space → ProblemStatement.Space) (hw : ContDiff ℝ (↑⊤) w) : Comparison.comparisonLpNorm 2 (fderiv ℝ fun (x : ProblemStatement.Space) => (rTest R hR w hw) x) = Comparison.comparisonLpNorm 2 (fderiv ℝ (PressureFluxTest.cutoffTest R w))

noncomputable def NavierStokesR3.PressureFlux.canonicalCutoffFlux (R : ℝ) (hR : 0 < R) (u v : ProblemStatement.VelocityField) (t : ℝ) (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) : ℂ

Canonical flux for a time slice of the difference of two velocities.

Equations

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

theorem NavierStokesR3.PressureFlux.canonicalCutoffFlux_eq_sum (R : ℝ) (hR : 0 < R) (u v : ProblemStatement.VelocityField) (t : ℝ) (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) : canonicalCutoffFlux R hR u v t hu hv = ∑ i : Fin 3, ∑ j : Fin 3, Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) (fluxTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯)

theorem NavierStokesR3.PressureFlux.norm_canonicalCutoffFlux_le (R : ℝ) (hR : 0 < R) (u v : ProblemStatement.VelocityField) (t : ℝ) (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) {C : ℝ} (hbound : ∀ (i j : Fin 3), ‖Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) (fluxTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯)‖ ≤ C) : ‖canonicalCutoffFlux R hR u v t hu hv‖ ≤ 9 * C

theorem NavierStokesR3.PressureFlux.actual_flux_eq_canonicalCutoffFlux {T t R : ℝ} {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} (H : PressureRecovery.Hypotheses T u v p q) (ht : t ∈ Set.Ioo 0 T) (hR : 0 < R) (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) : ∫ (x : NavierStokes.ProblemStatement.Space), (p - q) (t, x) * (fderiv ℝ (ComparisonCutoffs.weight R) x) ((u - v) (t, x)) = (canonicalCutoffFlux R hR u v t hu hv).re

theorem NavierStokesR3.PressureFlux.actual_flux_integrable_and_le_canonicalNorm {T t R : ℝ} {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} (H : PressureRecovery.Hypotheses T u v p q) (ht : t ∈ Set.Ioo 0 T) (hR : 0 < R) (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) : MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => (p - q) (t, x) * (fderiv ℝ (ComparisonCutoffs.weight R) x) ((u - v) (t, x))) MeasureTheory.volume ∧ |∫ (x : NavierStokes.ProblemStatement.Space), (p - q) (t, x) * (fderiv ℝ (ComparisonCutoffs.weight R) x) ((u - v) (t, x))| ≤ ‖canonicalCutoffFlux R hR u v t hu hv‖

noncomputable def NavierStokesR3.PressureFlux.commutatorPair (i j : Fin 3) (h g : ProblemStatement.Space → ℝ) (ψ ψh : Comparison.ComplexTest) : ℂ

The commutator integral in the heat-kernel estimate.

Equations

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

theorem NavierStokesR3.PressureFlux.integrable_commutator_pair (i j : Fin 3) {h g : ProblemStatement.Space → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hhg : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => h x * g x) (6 / 5) MeasureTheory.volume) (ψ ψh : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => g x • (Comparison.rieszTest i j ψh x - h x • Comparison.rieszTest i j ψ x)) MeasureTheory.volume

theorem NavierStokesR3.PressureFlux.pressurePair_decomposition (i j : Fin 3) {h g : ProblemStatement.Space → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hhg : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => h x * g x) (6 / 5) MeasureTheory.volume) (ψ ψh : Comparison.ComplexTest) : Comparison.pressurePair i j g ψh = (∫ (x : ProblemStatement.Space), ↑(h x * g x) * Comparison.rieszTest i j ψ x) + commutatorPair i j h g ψ ψh

theorem NavierStokesR3.PressureFlux.norm_pressurePair_le_local_commutator (i j : Fin 3) {h g : ProblemStatement.Space → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hhg : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => h x * g x) (6 / 5) MeasureTheory.volume) (ψ ψh : Comparison.ComplexTest) : ‖Comparison.pressurePair i j g ψh‖ ≤ (Comparison.comparisonLpNorm (6 / 5) fun (x : ProblemStatement.Space) => h x * g x) * Comparison.comparisonLpNorm 6 (Comparison.rieszTest i j ψ) + ‖commutatorPair i j h g ψ ψh‖

noncomputable def NavierStokesR3.PressureFlux.rieszSobolevConstant : ℝ

The fixed constant in the actual Riesz-test Sobolev inequality.

Equations

• NavierStokesR3.PressureFlux.rieszSobolevConstant = 3 * NavierStokesR3.WeightedSobolev.sobolevConstant

theorem NavierStokesR3.PressureFlux.rieszSobolevConstant_nonneg : 0 ≤ rieszSobolevConstant

noncomputable def NavierStokesR3.PressureFlux.localPairConstant : ℝ

Local pair constant, given by rieszSobolevConstant * PressureFluxTest.cutoffDerivativeConstant.

Equations

• NavierStokesR3.PressureFlux.localPairConstant = NavierStokesR3.PressureFlux.rieszSobolevConstant * NavierStokesR3.PressureFluxTest.cutoffDerivativeConstant

theorem NavierStokesR3.PressureFlux.localPairConstant_nonneg : 0 ≤ localPairConstant

theorem NavierStokesR3.PressureFlux.riesz_rTest_bound {R : ℝ} (hR : 0 < R) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (i j : Fin 3) : Comparison.comparisonLpNorm 6 (Comparison.rieszTest i j (rTest R hR w hw)) ≤ localPairConstant * (√(∫ (x : ProblemStatement.Space), ComparisonCutoffs.cutoff R x ^ 8 * Comparison.gradientSq w x) / R + Comparison.comparisonLpNorm 2 w / R ^ 2)

theorem NavierStokesR3.PressureFlux.rTest_four_bound {R : ℝ} (hR : 0 < R) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) : Comparison.comparisonLpNorm 4 ⇑(rTest R hR w hw) ≤ 8 * ComparisonCutoffs.derivativeConstant 1 / R * Comparison.comparisonLpNorm 2 w ^ (1 / 4) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => ComparisonCutoffs.cutoff R x ^ 4 • w x) ^ (3 / 4)

theorem NavierStokesR3.PressureFlux.localized_pair_bound {R : ℝ} (hR : 0 < R) {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (hw2 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)) 2 MeasureTheory.volume) (hu3 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) 3 MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ↑(ComparisonCutoffs.multiplier R x * Comparison.tensorDiff u v t i j x) * Comparison.rieszTest i j (rTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯) x) MeasureTheory.volume ∧ ‖∫ (x : ProblemStatement.Space), ↑(ComparisonCutoffs.multiplier R x * Comparison.tensorDiff u v t i j x) * Comparison.rieszTest i j (rTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯) x‖ ≤ localPairConstant * ((Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ^ (3 / 2) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (1 / 2) + (2 * Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) * Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => u (t, x)) * (Comparison.dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) / R ^ 2)

The local part of one canonical pressure component is an actual integrable pairing.

theorem NavierStokesR3.PressureFlux.norm_cutoff_pressurePair_le_local_commutator {R : ℝ} (hR : 0 < R) {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (hw2 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)) 2 MeasureTheory.volume) (hu3 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) 3 MeasureTheory.volume) (i j : Fin 3) (hg : MeasureTheory.Integrable (Comparison.tensorDiff u v t i j) MeasureTheory.volume) : ‖Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) (fluxTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯)‖ ≤ localPairConstant * ((Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ^ (3 / 2) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (1 / 2) + (2 * Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) * Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => u (t, x)) * (Comparison.dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) / R ^ 2) + ‖commutatorPair i j (ComparisonCutoffs.multiplier R) (Comparison.tensorDiff u v t i j) (rTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯) (fluxTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯)‖

noncomputable def NavierStokesR3.PressureFlux.uniformCoefficient (C₁ C₂ M₀ U₀ G₀ : ℝ) : ℝ

The coefficient after fixing uniform bounds for the three data norms.

Equations

• NavierStokesR3.PressureFlux.uniformCoefficient C₁ C₂ M₀ U₀ G₀ = C₁ * (M₀ ^ (3 / 2) + 2 * M₀ * U₀) * (M₀ + 1) + C₂ * G₀ * M₀ ^ (1 / 4)

theorem NavierStokesR3.PressureFlux.uniformCoefficient_nonneg {C₁ C₂ M₀ U₀ G₀ : ℝ} (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hM₀ : 0 ≤ M₀) (hU₀ : 0 ≤ U₀) (hG₀ : 0 ≤ G₀) : 0 ≤ uniformCoefficient C₁ C₂ M₀ U₀ G₀

theorem NavierStokesR3.PressureFlux.uniform_expression_bound {C₁ C₂ M₀ U₀ G₀ M U G A B R : ℝ} (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hM₀ : 0 ≤ M₀) (hU₀ : 0 ≤ U₀) (hG₀ : 0 ≤ G₀) (hM : 0 ≤ M) (hU : 0 ≤ U) (_hG : 0 ≤ G) (hA : 0 ≤ A) (hB : 0 ≤ B) (hMM : M ≤ M₀) (hUU : U ≤ U₀) (hGG : G ≤ G₀) (hR : 0 < R) : C₁ * (M ^ (3 / 2) * B ^ (1 / 2) + 2 * M * U) * (A / R + M / R ^ 2) + C₂ * G * M ^ (1 / 4) * R ^ (-(7 / 4)) * B ^ (3 / 4) ≤ uniformCoefficient C₁ C₂ M₀ U₀ G₀ * ((B ^ (1 / 2) + 1) * (A / R + 1 / R ^ 2) + R ^ (-(7 / 4)) * B ^ (3 / 4))

Collecting constants uses only the fixed data-norm bounds, not the radius.

theorem NavierStokesR3.PressureFlux.rpow_three_fourths_div {R : ℝ} (hR : 0 < R) : R ^ (-(3 / 4)) / R = R ^ (-(7 / 4))

noncomputable def NavierStokesR3.PressureFlux.commutatorConstant : ℝ

The fixed coefficient after combining the commutator and test-function bounds.

Equations

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

theorem NavierStokesR3.PressureFlux.commutatorConstant_nonneg : 0 ≤ commutatorConstant

theorem NavierStokesR3.PressureFlux.cutoff_commutator_bound {R : ℝ} (hR : 0 < R) {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) {g : ProblemStatement.Space → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (i j : Fin 3) : ‖commutatorPair i j (ComparisonCutoffs.multiplier R) g (rTest R hR w hw) (fluxTest R hR w hw)‖ ≤ commutatorConstant * Comparison.comparisonLpNorm 1 g * Comparison.comparisonLpNorm 2 w ^ (1 / 4) * R ^ (-(7 / 4)) * (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => ComparisonCutoffs.cutoff R x ^ 4 • w x) ^ (3 / 4)

theorem NavierStokesR3.PressureFlux.cutoff_pressurePair_bound {R : ℝ} (hR : 0 < R) {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (hw2 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)) 2 MeasureTheory.volume) (hu3 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) 3 MeasureTheory.volume) (i j : Fin 3) (hg : MeasureTheory.Integrable (Comparison.tensorDiff u v t i j) MeasureTheory.volume) : ‖Comparison.pressurePair i j (Comparison.tensorDiff u v t i j) (fluxTest R hR (fun (x : ProblemStatement.Space) => (u - v) (t, x)) ⋯)‖ ≤ localPairConstant * ((Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ^ (3 / 2) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (1 / 2) + (2 * Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) * Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => u (t, x)) * (Comparison.dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) / R ^ 2) + commutatorConstant * Comparison.comparisonLpNorm 1 (Comparison.tensorDiff u v t i j) * (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ^ (1 / 4) * R ^ (-(7 / 4)) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (3 / 4)

One actual canonical pressure component, with the three data norms explicit.

theorem NavierStokesR3.PressureFlux.canonicalCutoffFlux_bound {R : ℝ} (hR : 0 < R) {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)) (hw2 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)) 2 MeasureTheory.volume) (hu3 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) 3 MeasureTheory.volume) (hg : ∀ (i j : Fin 3), MeasureTheory.Integrable (Comparison.tensorDiff u v t i j) MeasureTheory.volume) {G : ℝ} (hG : ∀ (i j : Fin 3), Comparison.comparisonLpNorm 1 (Comparison.tensorDiff u v t i j) ≤ G) : ‖canonicalCutoffFlux R hR u v t hu hv‖ ≤ 9 * (localPairConstant * ((Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ^ (3 / 2) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (1 / 2) + (2 * Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) * Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => u (t, x)) * (Comparison.dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) / R ^ 2) + commutatorConstant * G * (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ^ (1 / 4) * R ^ (-(7 / 4)) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (3 / 4))

The full canonical flux with an explicit bound on each tensor component's L¹ norm.

theorem NavierStokesR3.PressureFlux.exists_uniform_canonicalCutoffFlux_bound (M₀ U₀ G₀ : ℝ) (hM₀ : 0 ≤ M₀) (hU₀ : 0 ≤ U₀) (hG₀ : 0 ≤ G₀) : ∃ (CP : ℝ), 0 ≤ CP ∧ ∀ (R : ℝ) (hR : 1 ≤ R) (u v : ProblemStatement.VelocityField) (t : ℝ) (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => v (t, x)), MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)) 2 MeasureTheory.volume → MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) 3 MeasureTheory.volume → (∀ (i j : Fin 3), MeasureTheory.Integrable (Comparison.tensorDiff u v t i j) MeasureTheory.volume) → (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ≤ M₀ → (Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => u (t, x)) ≤ U₀ → (∀ (i j : Fin 3), Comparison.comparisonLpNorm 1 (Comparison.tensorDiff u v t i j) ≤ G₀) → ‖canonicalCutoffFlux R ⋯ u v t hu hv‖ ≤ CP * ((Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (1 / 2) + 1) * (Comparison.dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + 1 / R ^ 2) + R ^ (-(7 / 4)) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (3 / 4))

One constant works for all radii and all smooth slices satisfying the fixed norm bounds.

theorem NavierStokesR3.PressureFlux.exists_uniform_actual_pressure_flux_bound {T : ℝ} {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} (H : PressureRecovery.Hypotheses T u v p q) (M₀ U₀ G₀ : ℝ) (hM₀ : 0 ≤ M₀) (hU₀ : 0 ≤ U₀) (hG₀ : 0 ≤ G₀) (hM : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => (u - v) (t, x)) 2 MeasureTheory.volume ∧ (Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => (u - v) (t, x)) ≤ M₀) (hU : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) 3 MeasureTheory.volume ∧ (Comparison.comparisonLpNorm 3 fun (x : ProblemStatement.Space) => u (t, x)) ≤ U₀) (hG : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), MeasureTheory.Integrable (Comparison.tensorDiff u v t i j) MeasureTheory.volume ∧ Comparison.comparisonLpNorm 1 (Comparison.tensorDiff u v t i j) ≤ G₀) : ∃ (CP : ℝ), 0 ≤ CP ∧ ∀ (R : ℝ), 1 ≤ R → ∀ t ∈ Set.Ioo 0 T, |∫ (x : NavierStokes.ProblemStatement.Space), (p - q) (t, x) * (fderiv ℝ (ComparisonCutoffs.weight R) x) ((u - v) (t, x))| ≤ CP * ((Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (1 / 2) + 1) * (Comparison.dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + 1 / R ^ 2) + R ^ (-(7 / 4)) * Comparison.cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t ^ (3 / 4))

The physical pressure flux has a single bound uniform in time and cutoff radius. All hypotheses on the pressure are exactly those already present in pressure recovery.