The classical dissipation of the regularized solution

For a time slice that is continuously differentiable in space and agrees with the real part of a complex L² field whose transform is conjugation symmetric, the classical dissipation ∫ |∇u|² equals the frequency dissipation ∫ 4π²|ξ|² |v̂|². Integrating in time identifies the dissipation term of the energy equality in thm:regularised.

theorem CKN.Leray.norm_sq_eq_sum_sq_re_of_conj (T : ComplexTensor3) (hT : complexTensorConj T = T) : ‖T‖ ^ 2 = ∑ i : Fin 3, ∑ j : Fin 3, ((T.ofLp j).ofLp i).re ^ 2

A tensor fixed by coordinatewise conjugation has squared norm equal to the sum of the squares of the real parts of its entries.

theorem CKN.Leray.lintegral_spatialGradientSq_slice_eq {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (hreal : (conjReflectLp complexVecConj) ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) = (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) (hrep : (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) =ᵐ[MeasureTheory.volume] realPartVectorL2Representative v) (hC1 : ∀ (i : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => u (x, s) i) : ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (x, s)) = ENNReal.ofReal (forcedFourierDissipation v)

The classical squared gradient of a spatially C¹ slice equals the frequency dissipation of a conjugation-symmetric complex field representing it.

theorem CKN.Leray.regUniformDissipation_eq_ofReal_integral {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {t T : ℝ} (htT : t ≤ T) (hDcont : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (Set.univ ×ˢ Set.Ioc 0 T)) (d : ℝ → ℝ) (hd : MeasureTheory.IntegrableOn d (Set.Ioc 0 t) MeasureTheory.volume) (hd0 : ∀ (s : ℝ), 0 ≤ d s) (hslice : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (x, s)) = ENNReal.ofReal (d s)) : regUniformDissipation u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) t = ENNReal.ofReal (∫ (s : ℝ) in Set.Ioc 0 t, d s)

The dissipation of a velocity whose spatial derivatives are continuous on positive times up to T is the time integral of its slice dissipations.