Global weak convergence of the gradients in prop:forced-limit

The compactness step of prop:forced-limit gives weak L² convergence of the forced regularized gradients on the compact sets of an exhaustion of the slab ℝ³ × (0,T). With the uniform dissipation bound of lem:forced-energy-bounds on the slab, the weak limit is square integrable on the whole slab, and each coordinate converges weakly against every square-integrable test on the slab.

noncomputable def CKN.Leray.forcedLerayLimitGradientCoord (i j : Fin 3) : CompactnessGradientFiber →L[ℝ] ℝ

The coordinate (i, j) of the gradient carrier, as a continuous linear functional.

Equations

• CKN.Leray.forcedLerayLimitGradientCoord i j = PiLp.proj 2 (fun (x : Fin 3) => ℝ) j ∘SL PiLp.proj 2 (fun (x : Fin 3) => CKN.Foundation.Parabolic.L2Vec3) i

theorem CKN.Leray.forcedLerayLimit_globalGradient_outputs (T : ℝ) (Dseq : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (G : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber) (K : ℕ → Set (Foundation.Parabolic.Vec3 × ℝ)) (hKsubset : ∀ (m : ℕ), K m ⊆ spaceTimeSet Set.univ (Set.Ioo 0 T)) (hKcover : MeasureTheory.AECover (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) Filter.atTop K) (B : ENNReal) (hB : B < ⊤) (hDenergy : ∀ (n : ℕ), ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ‖toCompactnessGradientFiber (Dseq n z)‖ₑ ^ 2 ≤ B) (hlocal : ∀ (m : ℕ), ∃ (hD : ∀ (n : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Dseq n z)) 2 (MeasureTheory.volume.restrict (K m))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (K m))), ∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 (MeasureTheory.volume.restrict (K m)))), Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Dseq n z)) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp G hG) w))) : MeasureTheory.AEStronglyMeasurable (fun (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => ((G z).ofLp i).ofLp j) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) => ((G z).ofLp i).ofLp j) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∀ (i j : Fin 3) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ), MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), Dseq n z i j * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ((G z).ofLp i).ofLp j * w z))

The global gradient clause of prop:forced-limit on one slab ℝ³ × (0,T): weak L² convergence of the gradients on the members of an exhaustion of the slab, with a uniform bound on the slab, gives a square-integrable limit on the slab and weak convergence of every coordinate against every square-integrable test on the slab. The limit is the matrix field of the local weak limit G.