Leray Assembly Contracts

Supporting estimates for the Navier–Stokes development.

def CKN.lerayAssemblyPressureSlabData (pε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ) (σ : ℕ → ℕ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (T : ℝ) : Prop

Identification and strong pressure convergence on one finite time slab.

Equations

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

def CKN.lerayAssemblyPressureLimitContract (ρ : Leray.RegMollifierProfile) (uε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (pε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ) : Prop

Pressure identification and convergence data for a Leray subsequence.

Equations

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

def CKN.lerayAssemblyHopfLimitContract (ρ : Leray.RegMollifierProfile) (uε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hlerayLimit : lerayAssemblyCompactnessLimitContract ρ uε) : Prop

Named proposition contract for the limiting Hopf property.

Equations

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

theorem CKN.lerayExistence_of_limits (ρ : Leray.RegMollifierProfile) (uε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (pε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ) (hregularised : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε), lerayAssemblyRegularisedConditions ρ uε pε a ha ε hε) (hregMomentum : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε), ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, uε a ha ε z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, Leray.regUniformMollifiedVelocity ρ ε hε (uε a ha ε) z j * uε a ha ε z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha ε y i) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - pε a ha ε z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) (hregLocalEnergy : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε), ∀ ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), spatialGradientSq (uε a ha ε) (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha ε y i) j z) z * ψ z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), Foundation.Parabolic.vec3EuclideanNorm (uε a ha ε z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (uε a ha ε z) ^ 2 * Leray.regUniformMollifiedVelocity ρ ε hε (uε a ha ε) z i + 2 * pε a ha ε z * uε a ha ε z i) * spatialPartial ψ i z) (hlerayLimit : lerayAssemblyCompactnessLimitContract ρ uε) (hpressureLimit : lerayAssemblyPressureLimitContract ρ uε pε) (hhopfLimit : lerayAssemblyHopfLimitContract ρ uε hlerayLimit) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : IsInJ a → ∃ (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ), IsGlobalLerayHopfSolution a u Du ∧ ∀ (q : ℝ), 5 / 2 < q → IsSuitableWeakSolution Set.univ (Set.Ioi 0) q u Du p 0

The direct limiting argument for thm:leray, with the regularized identities and convergence statements as explicit inputs.