Energy of compactly supported fields on Euclidean three-space

All integrals in this module are the standard Lebesgue volume integrals on ProblemStatement.Space. Compact support supplies integrability; no finite replacement measure or convention about nonintegrable functions is used.

A scalar bound for the forced energy inequality

The integrating factor controls an energy whose time derivative is bounded by the energy plus a constant. Only derivatives in the interior of the time interval are required.

theorem NavierStokesR3.ScalarEnergyBound.forced_gronwall_weighted {T C : ℝ} {E E' : ℝ → ℝ} (hT : 0 ≤ T) (hcont : ContinuousOn E (Set.Icc 0 T)) (hinitial : E 0 = 0) (hderiv : ∀ t ∈ Set.Ioo 0 T, HasDerivAt E (E' t) t) (hbound : ∀ t ∈ Set.Ioo 0 T, E' t ≤ E t + C) (t : ℝ) : t ∈ Set.Icc 0 T → (E t + C) * Real.exp (-t) ≤ C

The shifted energy has a nonincreasing integrating factor.

theorem NavierStokesR3.ScalarEnergyBound.forced_gronwall {T C : ℝ} {E E' : ℝ → ℝ} (hT : 0 ≤ T) (hcont : ContinuousOn E (Set.Icc 0 T)) (hinitial : E 0 = 0) (hderiv : ∀ t ∈ Set.Ioo 0 T, HasDerivAt E (E' t) t) (hbound : ∀ t ∈ Set.Ioo 0 T, E' t ≤ E t + C) (t : ℝ) : t ∈ Set.Icc 0 T → E t ≤ C * (Real.exp t - 1)

The scalar forced Gronwall estimate with zero initial energy.

theorem NavierStokesR3.ScalarEnergyBound.forced_gronwall_uniform {T C : ℝ} {E E' : ℝ → ℝ} (hT : 0 ≤ T) (hT1 : T ≤ 1) (hC : 0 ≤ C) (hcont : ContinuousOn E (Set.Icc 0 T)) (hinitial : E 0 = 0) (hderiv : ∀ t ∈ Set.Ioo 0 T, HasDerivAt E (E' t) t) (hbound : ∀ t ∈ Set.Ioo 0 T, E' t ≤ E t + C) (t : ℝ) : t ∈ Set.Icc 0 T → E t ≤ C * Real.exp 1

A bound independent of the endpoint of an interval contained in [0, 1].

A uniform spatial square-integral bound for compactly supported forces

Compact spacetime support gives one compact spatial set supporting all slices. Continuity of the parameterized integral then supplies a finite bound on the closed time interval [0, 1].

theorem NavierStokesR3.CompactForceBound.exists_uniform_l2sq_bound {f : NavierStokes.ProblemStatement.VelocityField} (hf : Continuous f) (hcf : HasCompactSupport f) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc 0 1, MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => ‖f (t, x)‖ ^ 2) MeasureTheory.volume ∧ ∫ (x : NavierStokes.ProblemStatement.Space), ‖f (t, x)‖ ^ 2 ≤ C

A continuous force of compact spacetime support has uniformly bounded spatial square integrals on the unit time interval.

theorem NavierStokesR3.CompactEnergy.compact_inner_left {f g : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : HasCompactSupport f) : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => inner ℝ (f x) (g x)

theorem NavierStokesR3.CompactEnergy.compact_norm_sq {f : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : HasCompactSupport f) : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => ‖f x‖ ^ 2

theorem NavierStokesR3.CompactEnergy.integrable_norm_sq {f : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : Continuous f) (hcf : HasCompactSupport f) : MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => ‖f x‖ ^ 2) MeasureTheory.volume

theorem NavierStokesR3.CompactEnergy.compact_component {f : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : HasCompactSupport f) (i : Fin 3) : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => (f x).ofLp i

theorem NavierStokesR3.CompactEnergy.integrable_inner_left {f g : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : Continuous f) (hg : Continuous g) (hcf : HasCompactSupport f) : MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => inner ℝ (f x) (g x)) MeasureTheory.volume

theorem NavierStokesR3.CompactEnergy.compact_partial {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : NavierStokes.ProblemStatement.Space → V} (hf : HasCompactSupport f) (i : Fin 3) : HasCompactSupport (NavierStokes.SolutionDifference.spatialPartial i f)

theorem NavierStokesR3.CompactEnergy.integral_partial_eq_zero {f : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hcf : HasCompactSupport f) (i : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), NavierStokes.SolutionDifference.spatialPartial i f x = 0

theorem NavierStokesR3.CompactEnergy.integral_mul_partial {f g : NavierStokes.ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hcf : HasCompactSupport f) (i : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), f x * NavierStokes.SolutionDifference.spatialPartial i g x = -∫ (x : NavierStokes.ProblemStatement.Space), g x * NavierStokes.SolutionDifference.spatialPartial i f x

theorem NavierStokesR3.CompactEnergy.integral_fderiv_apply {f : NavierStokes.ProblemStatement.Space → ℝ} {v : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (hcv : HasCompactSupport v) : ∫ (x : NavierStokes.ProblemStatement.Space), (fderiv ℝ f x) (v x) = -∫ (x : NavierStokes.ProblemStatement.Space), f x * ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i v x).ofLp i

Integration against a compactly supported vector field transfers a directional derivative to its divergence.

theorem NavierStokesR3.CompactEnergy.integral_fderiv_apply_zero {f : NavierStokes.ProblemStatement.Space → ℝ} {v : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (hcv : HasCompactSupport v) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i v x).ofLp i = 0) : ∫ (x : NavierStokes.ProblemStatement.Space), (fderiv ℝ f x) (v x) = 0

theorem NavierStokesR3.CompactEnergy.integral_transport_energy_zero {w v : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (hv : ContDiff ℝ (↑⊤) v) (hcv : HasCompactSupport v) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), ∑ i : Fin 3, (NavierStokes.SolutionDifference.spatialPartial i v x).ofLp i = 0) : ∫ (x : NavierStokes.ProblemStatement.Space), inner ℝ (w x) ((fderiv ℝ w x) (v x)) = 0

Divergence-free transport contributes zero to the whole-space energy.

theorem NavierStokesR3.CompactEnergy.integral_inner_partial {f g : NavierStokes.ProblemStatement.Space → NavierStokes.ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hcf : HasCompactSupport f) (i : Fin 3) : ∫ (x : NavierStokes.ProblemStatement.Space), inner ℝ (f x) (NavierStokes.SolutionDifference.spatialPartial i g x) = -∫ (x : NavierStokes.ProblemStatement.Space), inner ℝ (NavierStokes.SolutionDifference.spatialPartial i f x) (g x)

theorem NavierStokesR3.CompactEnergy.integral_laplacian_energy {u : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hcu : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) : ∫ (x : NavierStokes.ProblemStatement.Space), inner ℝ (u (t, x)) (NavierStokes.ProblemStatement.spatialLaplacian u t x) = -∑ i : Fin 3, ∫ (x : NavierStokes.ProblemStatement.Space), ‖NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => u (t, y)) x‖ ^ 2

theorem NavierStokesR3.CompactEnergy.integral_pressure_energy_zero {u : NavierStokes.ProblemStatement.VelocityField} {p : NavierStokes.ProblemStatement.PressureField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hp : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => p (t, x)) (hcu : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) : ∫ (x : NavierStokes.ProblemStatement.Space), inner ℝ (u (t, x)) (NavierStokes.ProblemStatement.pressureGradient p t x) = 0

The pressure need not have compact support: the compact velocity already makes every integration-by-parts product integrable.

noncomputable def NavierStokesR3.CompactEnergy.l2Sq (u : NavierStokes.ProblemStatement.VelocityField) (t : ℝ) : ℝ

The full squared spatial L2 norm with ordinary Euclidean volume.

Equations

• NavierStokesR3.CompactEnergy.l2Sq u t = ∫ (x : NavierStokes.ProblemStatement.Space), ‖u (t, x)‖ ^ 2

noncomputable def NavierStokesR3.CompactEnergy.energyRate (u : NavierStokes.ProblemStatement.VelocityField) (t : ℝ) : ℝ

Energy rate, given by ∫ x : Space, 2 * ⟪u (t, x), temporalDerivative u t x⟫_ℝ.

Equations

• NavierStokesR3.CompactEnergy.energyRate u t = ∫ (x : NavierStokes.ProblemStatement.Space), 2 * inner ℝ (u (t, x)) (NavierStokes.ProblemStatement.temporalDerivative u t x)

noncomputable def NavierStokesR3.CompactEnergy.dissipation (u : NavierStokes.ProblemStatement.VelocityField) (t : ℝ) : ℝ

Dissipation, given by ∑ i : Fin 3, ∫ x : Space, ‖spatialPartial i (fun y => u (t, y)) x‖ ^ 2.

Equations

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

theorem NavierStokesR3.CompactEnergy.dissipation_nonneg (u : NavierStokes.ProblemStatement.VelocityField) (t : ℝ) : 0 ≤ dissipation u t

theorem NavierStokesR3.CompactEnergy.energy_balance {u f : NavierStokes.ProblemStatement.VelocityField} {p : NavierStokes.ProblemStatement.PressureField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hp : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => p (t, x)) (hf : Continuous fun (x : NavierStokes.ProblemStatement.Space) => f (t, x)) (hcu : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hNS : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = f (t, x)) : energyRate u t = -2 * dissipation u t + 2 * ∫ (x : NavierStokes.ProblemStatement.Space), inner ℝ (u (t, x)) (f (t, x))

The exact forced Navier--Stokes energy balance on all of Euclidean space.

theorem NavierStokesR3.CompactEnergy.energy_rate_le {u f : NavierStokes.ProblemStatement.VelocityField} {p : NavierStokes.ProblemStatement.PressureField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hp : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => p (t, x)) (hf : Continuous fun (x : NavierStokes.ProblemStatement.Space) => f (t, x)) (hcu : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hfi : MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => ‖f (t, x)‖ ^ 2) MeasureTheory.volume) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hNS : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = f (t, x)) : energyRate u t ≤ l2Sq u t + l2Sq f t

Young's inequality controls the forcing by the two actual squared L2 norms. All terms are integrable before the integral is compared.

theorem NavierStokesR3.CompactEnergy.slice_compact {u : NavierStokes.ProblemStatement.VelocityField} {K : Set NavierStokes.ProblemStatement.Space} (hK : IsCompact K) {t : ℝ} (hsupp : (tsupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) ⊆ K) : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)

theorem NavierStokesR3.CompactEnergy.zero_outside {u : NavierStokes.ProblemStatement.VelocityField} {K : Set NavierStokes.ProblemStatement.Space} {t : ℝ} (hsupp : (tsupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) ⊆ K) {x : NavierStokes.ProblemStatement.Space} (hx : x ∉ K) : u (t, x) = 0

theorem NavierStokesR3.CompactEnergy.l2Sq_continuousOn {a b : ℝ} {u : NavierStokes.ProblemStatement.VelocityField} {K : Set NavierStokes.ProblemStatement.Space} (hK : IsCompact K) (hu : ContDiffOn ℝ (↑⊤) u (NavierStokes.SolutionDifference.slab a b)) (hsupp : ∀ t ∈ Set.Icc a b, (tsupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) ⊆ K) : ContinuousOn (l2Sq u) (Set.Icc a b)

theorem NavierStokesR3.CompactEnergy.energy_hasDerivAt {a b t : ℝ} {u : NavierStokes.ProblemStatement.VelocityField} {K : Set NavierStokes.ProblemStatement.Space} (hK : IsCompact K) (hu : ContDiffOn ℝ (↑⊤) u (NavierStokes.SolutionDifference.slab a b)) (hsupp : ∀ r ∈ Set.Icc a b, (tsupport fun (x : NavierStokes.ProblemStatement.Space) => u (r, x)) ⊆ K) (ht : t ∈ Set.Ioo a b) : HasDerivAt (l2Sq u) (energyRate u t) t

Differentiation under the ordinary whole-space energy integral follows from joint smoothness and fixed compact spatial support.

theorem NavierStokesR3.CompactEnergy.integrable_dissipation_terms {u : NavierStokes.ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (hcu : HasCompactSupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) (i : Fin 3) : MeasureTheory.Integrable (fun (x : NavierStokes.ProblemStatement.Space) => ‖NavierStokes.SolutionDifference.spatialPartial i (fun (y : NavierStokes.ProblemStatement.Space) => u (t, y)) x‖ ^ 2) MeasureTheory.volume

theorem NavierStokesR3.CompactEnergy.hasDerivAt_energy_balance {a b t : ℝ} {u f : NavierStokes.ProblemStatement.VelocityField} {p : NavierStokes.ProblemStatement.PressureField} {K : Set NavierStokes.ProblemStatement.Space} (hK : IsCompact K) (hu : ContDiffOn ℝ (↑⊤) u (NavierStokes.SolutionDifference.slab a b)) (hp : ContDiffOn ℝ (↑⊤) p (NavierStokes.SolutionDifference.slab a b)) (hf : Continuous fun (x : NavierStokes.ProblemStatement.Space) => f (t, x)) (hsupp : ∀ r ∈ Set.Icc a b, (tsupport fun (x : NavierStokes.ProblemStatement.Space) => u (r, x)) ⊆ K) (ht : t ∈ Set.Ioo a b) (hdiv : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hNS : ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = f (t, x)) : HasDerivAt (l2Sq u) (-2 * dissipation u t + 2 * ∫ (x : NavierStokes.ProblemStatement.Space), inner ℝ (u (t, x)) (f (t, x))) t

The exact energy identity, with the derivative justified and all spatial integrals taken against ordinary Lebesgue volume on R³.

theorem NavierStokesR3.CompactEnergy.uniform_finite_energy {u f : NavierStokes.ProblemStatement.VelocityField} {p : NavierStokes.ProblemStatement.PressureField} {K : Set NavierStokes.ProblemStatement.Space} (hK : IsCompact K) (hu : ContDiffOn ℝ (↑⊤) u NavierStokes.ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p NavierStokes.ProblemStatement.preSingularDomain) (hsupp : ∀ t ∈ Set.Ico 0 1, (tsupport fun (x : NavierStokes.ProblemStatement.Space) => u (t, x)) ⊆ K) (hf : ContDiff ℝ (↑⊤) f) (hcf : HasCompactSupport f) (hinitial : ∀ (x : NavierStokes.ProblemStatement.Space), u (0, x) = 0) (hdiv : ∀ t ∈ Set.Ioo 0 1, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0) (hNS : ∀ t ∈ Set.Ioo 0 1, ∀ (x : NavierStokes.ProblemStatement.Space), NavierStokes.ProblemStatement.navierStokesResidual u p t x = f (t, x)) : ProblemStatement.UniformFiniteEnergy (Set.Ico 0 1) u

A smooth compact force yields one uniform bound for the kinetic energy before time one. The proof includes square integrability at every time, then uses the PDE-derived energy inequality and a scalar integrating factor.