Reg Equicontinuity Main

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regEquicontinuity_modulus (ρ : 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 → ℝ) (hregData : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ) (_hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1), (∀ (n : ℕ) (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => uε a ha (εseq n) (x, t)) 2 MeasureTheory.volume) ∧ (∀ (n : ℕ) (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => uε a ha (εseq n) (x, t)) ∧ (∀ (n : ℕ) (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (n : ℕ) (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y i) j z) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (n : ℕ) (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) x i) j y) k z) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (n : ℕ) (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y i) z) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (n : ℕ), ContinuousOn (pε a ha (εseq n)) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (n : ℕ) (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => pε a ha (εseq n) y) i z) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (n : ℕ) (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (n : ℕ), ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y i) j (x, z.2)) z.1) ∧ (∀ (n : ℕ), ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => pε a ha (εseq n) (x, z.2)) z.1) ∧ (∀ (n : ℕ) (δ T : ℝ), 0 < δ → δ < T → ∃ (M : ℝ), 0 ≤ M ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), ∀ (i : Fin 3), |timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y i) z| ≤ M) ∧ (∀ (n : ℕ) (z : Foundation.Parabolic.ParabolicPoint), 0 < z.2 → ∀ (i : Fin 3), timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y i) z - ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) x i) j y) j z + ∑ j : Fin 3, regUniformMollifiedVelocity ρ (εseq n) ⋯ (uε a ha (εseq n)) z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y i) j z + spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => pε a ha (εseq n) y) i z = 0) ∧ ∀ (n : ℕ) (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice (uε a ha (εseq n)) t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation (uε a ha (εseq n)) (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y i) j z) t = MeasureTheory.eLpNorm (regMollifyVector ρ (εseq n) ⋯ (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2) (hregPressureBound : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ), (∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) → ∃ (P : ℝ), 0 ≤ P ∧ ∀ (n : ℕ), MeasureTheory.MemLp (pε a ha (εseq n)) (ENNReal.ofReal (5 / 3)) regUniformPositiveTimeMeasure ∧ MeasureTheory.eLpNorm (pε a ha (εseq n)) (ENNReal.ofReal (5 / 3)) regUniformPositiveTimeMeasure ≤ ENNReal.ofReal P) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ) (_hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) (C : Set Foundation.Parabolic.Vec3) (_hC : IsCompact C) (_hCU : C ⊆ Set.univ) (s₀ s₁ : ℝ) (_hs₀s₁ : Set.Icc s₀ s₁ ⊆ Set.Ioi 0) (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3) (_hw : ContDiff ℝ (↑⊤) w) (_hwc : HasCompactSupport w) (_hws : tsupport w ⊆ C) : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), s ∈ Set.Icc s₀ s₁ → t ∈ Set.Icc s₀ s₁ → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, uε a ha (εseq n) (x, t) i * (w x).ofLp i) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, uε a ha (εseq n) (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ

The regularized momentum and pressure bounds give the time-pairing modulus required by lem:compactness.