Compactness Strong Field

Supporting estimates for the Navier–Stokes development.

theorem instFactLeENNRealOfNat_leanPool : Fact (1 ≤ 2)

theorem instFactNeENNRealOfNatTop_leanPool : Fact (2 ≠ ⊤)

theorem CKN.Leray.memLp_two_vec3_on_rectangle_of_slice_bound {K Kc : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hKKc : K ⊆ Kc) (hJ : MeasurableSet J) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)] (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hu : Measurable u) (M : ENNReal) (hM : M < ⊤) (hbound : ∀ t ∈ J, ∫⁻ (x : Foundation.Parabolic.Vec3) in Kc, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 2 ≤ M) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u z)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))

A uniform spatial slice bound puts the field in space-time L² on a smaller spatial rectangle.

theorem CKN.Leray.lintegral_withLp_vec3_error_eq_rectangle {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (u v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ), ‖WithLp.toLp 2 (u z) - WithLp.toLp 2 (v z)‖ₑ ^ 2 ∂(MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J) = ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z - v z) ^ 2)

Squared L² distance on a restricted product is the squared Euclidean field error on the corresponding space-time rectangle.

theorem CKN.Leray.exists_strong_l2_limit_on_compact_rectangle {K W Kc : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hK : IsCompact K) (hW : IsOpen W) (hKW : K ⊆ W) (hWKc : W ⊆ Kc) (hJ : IsCompact J) (hJI : J ⊆ I) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (hDuMeas : ∀ (n : ℕ), Measurable (Du n)) (hweakW : ∀ (n : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn W (fun (y : Vec 3) => u n (y, t) i) fun (y : Vec 3) => Du n (y, t) i) (M G : ENNReal) (hM : M < ⊤) (hG : G < ⊤) (huBound : ∀ (n : ℕ), ∀ t ∈ J, ∫⁻ (x : Foundation.Parabolic.Vec3) in Kc, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M) (hDuBound : ∀ (n : ℕ), ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in Kc, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ x ∈ W, χ x = 1) (hmem : ∀ (n : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u n (x, ↑t))) 2 MeasureTheory.volume) (V : ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (t : ↑I) (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)), Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, ↑t))) ⋯) x) Filter.atTop (nhds (inner ℝ (V t) x))) (hVcont : ∀ (x : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)), Continuous fun (t : ↑I) => inner ℝ (V t) x) (huniform : ∀ (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : ℝ) (ht : t ∈ J), dist (inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, t))) ⋯) x) (inner ℝ (V ⟨t, ⋯⟩) x) < ε) (C : ℝ) (hC : 0 ≤ C) (hcutBound : ∀ (n : ℕ) (t : ℝ) (ht : t ∈ J), ‖MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, t))) ⋯‖ ≤ C) : ∃ (hf : ∀ (n : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u n z)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) (g : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)))), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u n z)) ⋯) Filter.atTop (nhds g)

The ball-average error and fixed-rank convergence give strong L² convergence on one compact space-time rectangle.