Reg Equicontinuity Inputs Data

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regEquicontinuity_data_of_regularised_contract (ρ : 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ε) (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

Extracts the regularized sequence data used by the equicontinuity estimate.

theorem CKN.Leray.regEquicontinuity_regularized_velocity_tenThirds_bound (ρ : 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 < ε), have u := uε a ha ε; have p := pε a ha ε; have D := fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z; have DD := fun (z : Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k z; have Dt := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z; have Dp := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z; (∃ (hSlice : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume), (Continuous fun (t : ↑(Set.Ici 0)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) ∧ (fun (x : Foundation.Parabolic.Vec3) => u (x, 0)) =ᵐ[MeasureTheory.volume] regUniformMollifiedInitial ρ ε hε a ∧ ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => D (x, z.2) i j) z.1) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ), 0 < δ → δ < T → ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ C ∧ |p z| ≤ C ∧ (∀ (i j : Fin 3), |D z i j| ≤ C) ∧ (∀ (i j k : Fin 3), |DD z i j k| ≤ C) ∧ (∀ (i : Fin 3), |Dt z i| ≤ C) ∧ ∀ (i : Fin 3), |Dp z i| ≤ C) ∧ (∀ (δ T : ℝ), 0 < δ → δ < T → (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j k : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (z : Foundation.Parabolic.ParabolicPoint), 0 < z.2 → ∀ (i : Fin 3), Dt z i - ∑ j : Fin 3, DD z i j j + ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * D z i j + Dp z i = 0) ∧ (∀ (t : ℝ), 0 < t → ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) (ENNReal.ofReal 2) MeasureTheory.volume), ((fun (x : Foundation.Parabolic.Vec3) => p (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 regEquicontinuity_regularized_velocity_tenThirds_bound._proof_55 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) ⋯) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), p (x, t) * spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j * mixedSecond ψ i j x) ∧ ∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u D t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (n : ℕ) (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) z i) (ENNReal.ofReal (10 / 3)) regUniformPositiveTimeMeasure ∧ MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) z i) (ENNReal.ofReal (10 / 3)) regUniformPositiveTimeMeasure ≤ ENNReal.ofReal B

Obtains a uniform positive-time ten-thirds bound from the regularized energy identity.

theorem CKN.Leray.regEquicontinuity_mollified_velocity_tenThirds_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hSlice : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hUc : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hC1 : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hU : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) (ENNReal.ofReal (10 / 3)) regUniformPositiveTimeMeasure) (BU : ℝ) (hBU : 0 ≤ BU) (hUbound : ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) (ENNReal.ofReal (10 / 3)) regUniformPositiveTimeMeasure ≤ ENNReal.ofReal BU) (i : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u z i) (ENNReal.ofReal (10 / 3)) regUniformPositiveTimeMeasure ∧ MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u z i) (ENNReal.ofReal (10 / 3)) regUniformPositiveTimeMeasure ≤ ENNReal.ofReal (3 * BU)

Transfers a positive-time ten-thirds bound through spatial mollification.