Compactness Gradient Representative

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.Leray.compactnessGradientLocalRepresentative (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (D : (j : ℕ) → ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))) (j : ℕ) : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber

A measurable representative of a local matrix-gradient L² class.

Equations

• CKN.Leray.compactnessGradientLocalRepresentative K J D j = AEMeasurable.mk ↑↑(D j) ⋯

theorem CKN.Leray.measurable_compactnessGradientLocalRepresentative (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (D : (j : ℕ) → ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))) (j : ℕ) : Measurable (compactnessGradientLocalRepresentative K J D j)

The chosen representative of a local gradient class is measurable.

theorem CKN.Leray.compactnessGradientLocalRepresentative_ae_eq (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (D : (j : ℕ) → ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))) (j : ℕ) : (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ↑↑(D j) z) =ᵐ[(MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))] compactnessGradientLocalRepresentative K J D j

The local measurable representative agrees with its L² class almost everywhere on the extraction rectangle.

theorem CKN.Leray.compactnessGradientLocalRepresentative_weak_partial {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (K : ℕ → Set Foundation.Parabolic.Vec3) (J : ℕ → Set ℝ) (hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U) (hJ : ∀ (j : ℕ), IsCompact (J j) ∧ J j ⊆ I) (hweakGrad : ∀ (n : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u n (x, t) i) fun (x : Vec 3) => Du n (x, t) i) (D : (j : ℕ) → ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))) (hDweak : ∀ (j : ℕ), ∃ (hgrad : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))), ∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) ⋯) w) Filter.atTop (nhds (inner ℝ (D j) w))) (hstrong : ∀ (j : ℕ), ∃ (_ : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm ((fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) - fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (v z)) 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))) Filter.atTop (nhds 0)) (j : ℕ) (i m : Fin 3) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (J j), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => ((compactnessGradientLocalRepresentative K J D j (x, t)).ofLp i).ofLp m) (interior (K j)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (interior (K j)) m (fun (x : Vec 3) => v (x, t) i) fun (x : Vec 3) => ((compactnessGradientLocalRepresentative K J D j (x, t)).ofLp i).ofLp m

On each open inner rectangle, the measurable local matrix limit is an almost-every-time weak spatial gradient of the strong velocity limit.