The gradient and dissipation of the forced regularized solution

Where the frequency dissipation of the complex solution is finite, the real solution has a square-integrable weak gradient given by the inverse transform of its frequency gradient. The mollified-gradient field represents it, and its squared norm is bounded by the frequency dissipation; this is the gradient data of lem:regularised-forced.

theorem CKN.Leray.forcedFourierGrad_hasWeakGradientOn (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (i : Fin 3) : HasWeakGradientOn Set.univ (fun (x : Vec 3) => realPartVectorL2Representative v x i) fun (x : Vec 3) (j : Fin 3) => (((↑↑(forcedFourierGrad v hv) (WithLp.toLp 2 x)).ofLp j).ofLp i).re

The real part of a complex field with square-integrable frequency gradient has a weak gradient in every component.

theorem CKN.Leray.forcedMollifiedGrad_of_fourier {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (hrep : (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) =ᵐ[MeasureTheory.volume] realPartVectorL2Representative v) : (∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) => forcedMollifiedGrad u (x, s) i) ∧ ∀ (i j : Fin 3), (fun (x : Foundation.Parabolic.Vec3) => forcedMollifiedGrad u (x, s) i j) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => (((↑↑(forcedFourierGrad v hv) (WithLp.toLp 2 x)).ofLp j).ofLp i).re

The slices of the mollified-gradient field of a representative of the real part represent the weak gradient, and their squared norms are bounded by the frequency dissipation.

theorem CKN.Leray.sum_sq_re_le_norm_sq (T : ComplexTensor3) : ∑ i : Fin 3, ∑ j : Fin 3, ((T.ofLp j).ofLp i).re ^ 2 ≤ ‖T‖ ^ 2

The squared entries of the real parts of a complex tensor are bounded by its squared norm.

theorem CKN.Leray.lintegral_spatialGradientSq_le {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (hrep : (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) =ᵐ[MeasureTheory.volume] realPartVectorL2Representative v) : ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u (forcedMollifiedGrad u) (x, s)) ≤ ENNReal.ofReal (forcedFourierDissipation v)

The squared gradient of a slice is bounded by the frequency dissipation.

theorem CKN.Leray.restrict_spaceTimeSet_eq_prod (I : Set ℝ) : MeasureTheory.volume.restrict (spaceTimeSet Set.univ I) = MeasureTheory.volume.prod (MeasureTheory.volume.restrict I)

theorem CKN.Leray.regUniformDissipation_eq_slab (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (t : ℝ) : regUniformDissipation u Du t = ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t), ENNReal.ofReal (spatialGradientSq u Du z)

The positive-time dissipation up to time t as a slab integral.