The gradient clauses of prop:forced-limit

For the forced regularized gradients along the subsequence of the forced local compactness theorem (forcedLerayLimit_local_compactness), and every finite slab ℝ³ × (0,T): the weak limit Du, read off from the compactness gradient limit, is square integrable on the slab and every coordinate of the gradients converges to it weakly against every square-integrable test on the slab. The local weak limits come from the compactness step on an exhaustion of the slab by compact cylinders, and the uniform bound on the slab is the dissipation bound of lem:forced-energy-bounds.

def CKN.Leray.forcedLerayLimitGradientCylinder (T : ℝ) (m : ℕ) : Set (Foundation.Parabolic.Vec3 × ℝ)

The compact cylinders exhausting the slab ℝ³ × (0,T).

Equations

• CKN.Leray.forcedLerayLimitGradientCylinder T m = Metric.closedBall 0 ↑m ×ˢ Set.Icc (T / (↑m + 2)) (T - T / (↑m + 2))

theorem CKN.Leray.forcedLerayLimit_gradient_clauses (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) (σ : ℕ → ℕ) (g : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber) (hgrad : ∀ (Q : Set (Foundation.Parabolic.Vec3 × ℝ)), IsCompact Q → Q ⊆ Set.univ ×ˢ Set.Ioi 0 → ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => toCompactnessGradientFiber (forcedRegGradient ρ a ha f hf (εseq (σ k)) z)) 2 (MeasureTheory.volume.restrict Q)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict Q)), ∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 (MeasureTheory.volume.restrict Q))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.ParabolicPoint) => toCompactnessGradientFiber (forcedRegGradient ρ a ha f hf (εseq (σ k)) z)) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp g hg) w))) (T : ℝ) (hT : 0 < T) : have μ := MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)); have Dseq := fun (n : ℕ) => forcedRegGradient ρ a ha f hf (εseq (σ n)); have Du := fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => ((g (Foundation.Parabolic.parabolicHomeomorph z)).ofLp i).ofLp j; MeasureTheory.AEStronglyMeasurable Du μ ∧ MeasureTheory.MemLp Du 2 μ ∧ ∀ (i j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp w 2 μ → 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), Du z i j * w z))

The gradient clauses of prop:forced-limit on every finite slab: for the subsequence σ and the gradient limit g of the forced local compactness theorem (forcedLerayLimit_local_compactness) (its third output is the hypothesis hgrad), the field Du z i j = g z i j is strongly measurable and square integrable on ℝ³ × (0,T), and each coordinate of the forced regularized gradients converges to it weakly against every square-integrable test on the slab.