Conditions for regularized solutions and their compactness limits

The regularity, energy and convergence assumptions shared by the Leray compactness and solution assembly theorems.

def CKN.lerayAssemblyRegularisedConditions (ρ : 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 → ℝ) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε) : Prop

Regularity, equation, pressure, and energy conditions for one regularized solution.

Equations

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

def CKN.lerayAssemblyLocalLimitData (ρ : Leray.RegMollifierProfile) (uε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) (σ : ℕ → ℕ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (T : ℝ) : Prop

The local convergence, integrability and weak-gradient data of a Leray limit.

Equations

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

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

Compactness and convergence data produced by the Leray limit argument.

Equations

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