Leray Assembly Energy

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayAssembly_weightedGradient_matrix (μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint) [MeasureTheory.IsFiniteMeasure μ] (D : ℕ → Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (d : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hD : ∀ (n : ℕ), MeasureTheory.MemLp (D n) 2 μ) (hd : MeasureTheory.MemLp d 2 μ) (hweak : ∀ (i j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp w 2 μ → Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint), D n z i j * w z ∂μ) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint), d z i j * w z ∂μ))) (ψ : Foundation.Parabolic.ParabolicPoint → ℝ) (hψ : MeasureTheory.MemLp ψ ⊤ μ) (hψpos : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂μ, 0 ≤ ψ z) : Filter.Tendsto (fun (n : ℕ) => ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint), D n z i j * d z i j * ψ z ∂μ) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint), spatialGradientSq (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) d z * ψ z ∂μ)) ∧ ∀ (n : ℕ), 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint), D n z i j * d z i j * ψ z ∂μ ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint), spatialGradientSq (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) (D n) z * ψ z ∂μ + ∫ (z : Foundation.Parabolic.ParabolicPoint), spatialGradientSq (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) d z * ψ z ∂μ

Weak convergence of the regularized gradient gives the weighted mixed energy limit and the polarization bound used in (S4).

theorem CKN.Leray.lerayAssembly_quadraticTerm_tendsto (μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint) [MeasureTheory.IsFiniteMeasure μ] (U : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) (hu : MeasureTheory.MemLp u 3 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 μ) Filter.atTop (nhds 0)) (T : Foundation.Parabolic.ParabolicPoint → ℝ) (hT : MeasureTheory.MemLp T ⊤ μ) : (∀ (n : ℕ), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, U n z i * U n z i * T z) μ) ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * u z i * T z) μ ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, U n z i * U n z i * T z ∂μ) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, u z i * u z i * T z ∂μ))

Strong local L³ convergence passes the quadratic energy term against a bounded test derivative.

theorem CKN.Leray.lerayAssembly_flux_integrable {μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint} (F G φ : Foundation.Parabolic.ParabolicPoint → ℝ) (hF : MeasureTheory.MemLp F (3 / 2) μ) (hG : MeasureTheory.MemLp G 3 μ) (hφ : MeasureTheory.MemLp φ ⊤ μ) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => F z * G z * φ z) μ

An L^{3/2} field times an L³ field can be paired with a bounded energy test derivative.

theorem CKN.Leray.lerayAssembly_cubicTerm_tendsto (μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint) (U J : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) (hJ : ∀ (n : ℕ), MeasureTheory.MemLp (J n) 3 μ) (hu : MeasureTheory.MemLp u 3 μ) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 μ) Filter.atTop (nhds 0)) (hJconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n - u) 3 μ) Filter.atTop (nhds 0)) (φ : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (hφ : ∀ (j : Fin 3), MeasureTheory.MemLp (φ j) ⊤ μ) : (∀ (n : ℕ), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, U n z i * U n z i * J n z j * φ j z) μ) ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z i * u z j * φ j z) μ ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, ∑ j : Fin 3, U n z i * U n z i * J n z j * φ j z ∂μ) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z i * u z j * φ j z ∂μ))

Strong L³ convergence of velocity and mollified transport velocity passes the regularized cubic energy flux to its limit.

theorem CKN.Leray.lerayAssembly_pressureFlux_tendsto (μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint) (P : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (U : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hP : ∀ (n : ℕ), MeasureTheory.MemLp (P n) (3 / 2) μ) (hp : MeasureTheory.MemLp p (3 / 2) μ) (hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) (hu : MeasureTheory.MemLp u 3 μ) (hPconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (P n - p) (3 / 2) μ) Filter.atTop (nhds 0)) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 μ) Filter.atTop (nhds 0)) (φ : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (hφ : ∀ (j : Fin 3), MeasureTheory.MemLp (φ j) ⊤ μ) : (∀ (n : ℕ), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, P n z * U n z j * φ j z) μ) ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, p z * u z j * φ j z) μ ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ j : Fin 3, P n z * U n z j * φ j z ∂μ) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ j : Fin 3, p z * u z j * φ j z ∂μ))

Strong local pressure and velocity convergence passes the pressure energy flux to its limit.

theorem CKN.Leray.lerayAssembly_energyRhs_decompose (μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint) (U J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p T : Foundation.Parabolic.ParabolicPoint → ℝ) (φ : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (hA : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, U z i * U z i * T z) μ) (hB : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, U z i * U z i * J z j * φ j z) μ) (hC : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, p z * U z j * φ j z) μ) : ∫ (z : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.vec3EuclideanNorm (U z) ^ 2 * T z + ∑ j : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (U z) ^ 2 * J z j + 2 * p z * U z j) * φ j z ∂μ = ∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, U z i * U z i * T z ∂μ + ∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, ∑ j : Fin 3, U z i * U z i * J z j * φ j z ∂μ + 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ j : Fin 3, p z * U z j * φ j z ∂μ

The regularized local-energy right side splits into quadratic energy, transport flux, and pressure flux.

theorem CKN.Leray.lerayAssembly_energyRhs_tendsto (μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint) [MeasureTheory.IsFiniteMeasure μ] (U J : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (P : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) (hJ : ∀ (n : ℕ), MeasureTheory.MemLp (J n) 3 μ) (hu : MeasureTheory.MemLp u 3 μ) (hP : ∀ (n : ℕ), MeasureTheory.MemLp (P n) (3 / 2) μ) (hp : MeasureTheory.MemLp p (3 / 2) μ) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 μ) Filter.atTop (nhds 0)) (hJconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n - u) 3 μ) Filter.atTop (nhds 0)) (hPconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (P n - p) (3 / 2) μ) Filter.atTop (nhds 0)) (T : Foundation.Parabolic.ParabolicPoint → ℝ) (hT : MeasureTheory.MemLp T ⊤ μ) (φ : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (hφ : ∀ (j : Fin 3), MeasureTheory.MemLp (φ j) ⊤ μ) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.vec3EuclideanNorm (U n z) ^ 2 * T z + ∑ j : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (U n z) ^ 2 * J n z j + 2 * P n z * U n z j) * φ j z ∂μ) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * T z + ∑ j : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * u z j + 2 * p z * u z j) * φ j z ∂μ))

The regularized local-energy right side converges to the unregularized right side under the strong velocity, transport, and pressure limits.

theorem CKN.Leray.lerayAssembly_regEnergyRhs_localBox {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)) (hKbox : tsupport (have this := ψ; this) ⊆ spaceTimeSet Ω' J) (U Jv : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), Foundation.Parabolic.vec3EuclideanNorm (U z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (U z) ^ 2 * Jv z i + 2 * p z * U z i) * spatialPartial ψ i z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, Foundation.Parabolic.vec3EuclideanNorm (U z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (U z) ^ 2 * Jv z i + 2 * p z * U z i) * spatialPartial ψ i z

The regularized local-energy flux is supported in the test function's compact support.

theorem CKN.Leray.lerayAssembly_localEnergy_limit {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Set.univ (Set.Ioi 0) Ω' J) (U Jv : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Dseq : ℕ → Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (Pseq : ℕ → Foundation.Parabolic.ParabolicPoint → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p ψ : Foundation.Parabolic.ParabolicPoint → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)) (hKbox : tsupport (have this := ψ; this) ⊆ spaceTimeSet Ω' J) (hψpos : ∀ (z : Foundation.Parabolic.ParabolicPoint), 0 ≤ ψ z) (hULocal : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hJLocal : ∀ (n : ℕ), MeasureTheory.MemLp (Jv n) 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (huLocal : MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (hJconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Jv n - u) 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (hDseqLocal : ∀ (n : ℕ), MeasureTheory.MemLp (Dseq n) 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hDuLocal : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hweak : ∀ (i j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, Dseq n z i j * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, Du z i j * w z))) (hPseqLocal : ∀ (n : ℕ), MeasureTheory.MemLp (Pseq n) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hpLocal : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hPconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Pseq n - p) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) (hreg : ∀ (n : ℕ), 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), spatialGradientSq (U n) (Dseq n) z * ψ z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), Foundation.Parabolic.vec3EuclideanNorm (U n z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (U n z) ^ 2 * Jv n z i + 2 * Pseq n z * U n z i) * spatialPartial ψ i z) : 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, spatialGradientSq u Du z * ψ z ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * u z i + 2 * p z * u z i) * spatialPartial ψ i z

The regularized local-energy equality passes directly to the limit on a local box by weighted gradient lower semicontinuity and strong flux convergence ((S4) of thm:leray).