Compactness Gradient Local

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.weak_partial_of_strong_velocity_and_weak_matrix_on_inner_rectangle {K Ω : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hK : IsCompact K) (hΩ : IsOpen Ω) (hΩK : Ω ⊆ K) (hJ : IsCompact J) (f : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3) (g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3) (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (D : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)))) (hf : ∀ (k : ℕ), MeasureTheory.MemLp (f k) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) (hstrong : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (f k - g) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) Filter.atTop (nhds 0)) (hDmem : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du k z)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) (hDweak : ∀ (v : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du k z)) ⋯) v) Filter.atTop (nhds (inner ℝ D v))) (i j : Fin 3) (hpartial : ∀ (k : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakPartialDerivOn Ω j (fun (x : Vec 3) => (f k (x, t)).ofLp i) fun (x : Vec 3) => Du k (x, t) i j) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakPartialDerivOn Ω j (fun (x : Vec 3) => (g (x, t)).ofLp i) fun (x : Vec 3) => (gradientCoordinateCLM i j) (↑↑D (x, t))

A weak local matrix limit is the almost-every-time spatial gradient of the strong local velocity limit on an open inner rectangle.