Localized energy identities for regularized Leray solutions

Compact spatial tests in lem:reg-local-energy yield an interval energy identity for every compact spatial cutoff.

theorem CKN.Leray.regTails_laplacian_ibp (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (q : Foundation.Parabolic.Vec3 → ℝ) (η : ℝ → ℝ) (i j : Fin 3) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηI : tsupport η ⊆ Set.Ioi 0) (hUcont : ∀ (k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) k) (Set.univ ×ˢ Set.Ioi 0)) (hDcont : ∀ (k j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y k) j z) (Set.univ ×ˢ Set.Ioi 0)) (hUdiff : ∀ (k : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) k) (Set.univ ×ˢ Set.Ioi 0)) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioi 0, u (z.1, z.2) i ^ 2 * spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => q y.1) j j z * η z.2 = -2 * ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioi 0, u (z.1, z.2) i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => q y.1) j z * η z.2

Spatial integration by parts transfers the compact cutoff Laplacian onto the regularized velocity in the positive time region. This is the localized form of the calculation in lem:reg-tails.

theorem CKN.Leray.regTails_intervalIntegral_eq_sub_of_weak_identity (F g : ℝ → ℝ) (hFcont : ContinuousOn F (Set.Ioi 0)) (hGcont : ContinuousOn g (Set.Ioi 0)) (hweak : ∀ (η : ℝ → ℝ), ContDiff ℝ (↑⊤) η → HasCompactSupport η → tsupport η ⊆ Set.Ioi 0 → ∫ (x : ℝ), F x * deriv η x = -∫ (x : ℝ), g x * η x) {s t : ℝ} (hs : 0 < s) (hst : s < t) : F t - F s = ∫ (x : ℝ) in s..t, g x

A continuous scalar weak time identity gives the corresponding interval identity on every positive time interval.

theorem CKN.Leray.regTails_timeFactor_integral (A : Foundation.Parabolic.Vec3 × ℝ → ℝ) (η : ℝ → ℝ) (hInt : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => A z * η z.2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioi 0, A z * η z.2 = ∫ (t : ℝ) in Set.Ioi 0, (∫ (x : Foundation.Parabolic.Vec3), A (x, t)) * η t

Fubini separates a compact positive time factor from a locally continuous space-time coefficient.

noncomputable def CKN.Leray.regTailsEnergyWeight (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (q : Foundation.Parabolic.Vec3 → ℝ) (t : ℝ) : ℝ

The localized kinetic energy associated with a compact spatial weight.

Equations

• CKN.Leray.regTailsEnergyWeight u q t = ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ^ 2 * q x

noncomputable def CKN.Leray.regTailsLocalizedSource (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (q : Foundation.Parabolic.Vec3 → ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The flux form of the localized kinetic energy derivative in lem:reg-tails.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regTails_localized_profiles_continuous (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (q : Foundation.Parabolic.Vec3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) (hUcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) (hDcont : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => D (z.1, z.2) i j) (Set.univ ×ˢ Set.Ioi 0)) (hPcont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2)) (Set.univ ×ˢ Set.Ioi 0)) (hJcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => J (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) : ContinuousOn (regTailsEnergyWeight u q) (Set.Ioi 0) ∧ ContinuousOn (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), regTailsLocalizedSource u D p J q (x, t)) (Set.Ioi 0)

Compact spatial weights make the localized energy and its flux source continuous functions of positive time.