The mollifier limit of the space-time energy identity

For each velocity component of the forced regularized solution, the space-time energy identity of the mollified velocity passes to the limit as the mollifier radius tends to zero: on almost every time slice the mollified pairing converges to the unmollified pairing, dominated by an integrable product of slice L² norms. The result is ∫∫ u_k² ∂ₜψ = 2 ∫ L_k, where L_k is the limiting slice pairing. This is the limit step of eq:reg-local-energy-forced.

theorem CKN.Leray.memLp_toReal_of_lintegral_sq {N : ℝ → ENNReal} (hm : Measurable N) {T : ℝ} (hfin : ∫⁻ (t : ℝ) in Set.Ioo 0 T, N t ^ 2 ≠ ⊤) : MeasureTheory.MemLp (fun (t : ℝ) => (N t).toReal) 2 (MeasureTheory.volume.restrict (Set.Ioo 0 T))

theorem CKN.Leray.memLp_eLpNorm_slice_two {X : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hX : MeasureTheory.StronglyMeasurable X) {T : ℝ} (h2 : MeasureTheory.MemLp X 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))) : MeasureTheory.MemLp (fun (t : ℝ) => (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => X (x, t)) 2 MeasureTheory.volume).toReal) 2 (MeasureTheory.volume.restrict (Set.Ioo 0 T))

theorem CKN.Leray.memLp_eLpNorm_vector_slice_two {X : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hX : MeasureTheory.StronglyMeasurable X) {T : ℝ} (h2 : MeasureTheory.MemLp X 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))) : MeasureTheory.MemLp (fun (t : ℝ) => (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => X (x, t)) 2 MeasureTheory.volume).toReal) 2 (MeasureTheory.volume.restrict (Set.Ioo 0 T))

theorem CKN.Leray.fderiv_scalar_slice {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (x : Foundation.Parabolic.Vec3) (t : ℝ) (v : Foundation.Parabolic.Vec3) : (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => ψ (y, t)) x) v = (fderiv ℝ ψ (x, t)) (v, 0)

theorem CKN.Leray.fderiv_eq_zero_of_notMem_tsupport_scalar {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) : fderiv ℝ ψ z = 0

theorem CKN.Leray.exists_weight_bound {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∃ (M : ℝ), 0 ≤ M ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), |ψ z| ≤ M) ∧ ∀ (j : Fin 3) (x : Foundation.Parabolic.Vec3) (t : ℝ), |(fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => ψ (y, t)) x) (basisVec j)| ≤ M

A smooth compactly supported space-time weight and its spatial partial derivatives are uniformly bounded.

theorem CKN.Leray.hasCompactSupport_scalar_slice {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgc : HasCompactSupport g) (t : ℝ) : HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => g (x, t)

noncomputable def CKN.Leray.leDeltaT (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (n : ℕ) (k : Fin 3) (t : ℝ) : ℝ

The mollified energy pairing of one component on a time slice.

Equations

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

noncomputable def CKN.Leray.leLimitT (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (k : Fin 3) (t : ℝ) : ℝ

The limiting energy pairing of one component on a time slice.

Equations

• CKN.Leray.leLimitT ρ ε hε ha hf ψ k t = Filter.atTop.limUnder fun (n : ℕ) => CKN.Leray.leDeltaT ρ ε hε ha hf ψ n k t

noncomputable def CKN.Leray.leTimeBound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (M : ℝ) (k : Fin 3) (t : ℝ) : ℝ

The dominating function of the mollified energy pairings.

Equations

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

theorem CKN.Leray.integrableOn_leTimeBound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (M : ℝ) (k : Fin 3) {T : ℝ} (hT : 0 < T) : MeasureTheory.IntegrableOn (leTimeBound ρ ε hε ha hf M k) (Set.Ioo 0 T) MeasureTheory.volume

theorem CKN.Leray.memLp_leTensor_slice (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {T t : ℝ} (ht : t ∈ Set.Icc 0 T) (k : Fin 3) (hDu : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) (x, t) i j) 2 MeasureTheory.volume) (j : Fin 3) : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => leTensor ρ ε hε ha hf j k (y, t)) 2 MeasureTheory.volume

theorem CKN.Leray.ae_leDelta (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {T : ℝ} (hT : 0 < T) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {M : ℝ} (hMψ : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), |ψ z| ≤ M) (hMd : ∀ (j : Fin 3) (x : Foundation.Parabolic.Vec3) (t : ℝ), |(fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => ψ (y, t)) x) (basisVec j)| ≤ M) (k : Fin 3) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∀ (n : ℕ), |leDeltaT ρ ε hε ha hf ψ n k t| ≤ leTimeBound ρ ε hε ha hf M k t) ∧ Filter.Tendsto (fun (n : ℕ) => leDeltaT ρ ε hε ha hf ψ n k t) Filter.atTop (nhds (leLimitT ρ ε hε ha hf ψ k t)) ∧ ∀ (hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume), leLimitT ρ ε hε ha hf ψ k t = leLimit (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) (fun (j : Fin 3) (y : Foundation.Parabolic.Vec3) => forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) (y, t) k j) (fun (j : Fin 3) (y : Foundation.Parabolic.Vec3) => leTensor ρ ε hε ha hf j k (y, t)) (fun (y : Foundation.Parabolic.Vec3) => forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) (y, t)) (fun (y : Foundation.Parabolic.Vec3) => forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft y k) (fun (y : Foundation.Parabolic.Vec3) => forcedForceMod f hf (y, t) k) (fun (y : Foundation.Parabolic.Vec3) => ψ (y, t)) k

On almost every time slice the mollified energy pairings are bounded by the dominating function and converge to the limiting pairing, which is the slice pairing of the unmollified fields.

theorem CKN.Leray.aestronglyMeasurable_leDeltaSlice (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : Continuous ψ) (n : ℕ) (k : Fin 3) (ν : MeasureTheory.Measure ℝ) : MeasureTheory.AEStronglyMeasurable (leDeltaT ρ ε hε ha hf ψ n k) ν

theorem CKN.Leray.integrableOn_leLimitT (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {T : ℝ} (hT : 0 < T) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (k : Fin 3) : MeasureTheory.IntegrableOn (leLimitT ρ ε hε ha hf ψ k) (Set.Ioo 0 T) MeasureTheory.volume

theorem CKN.Leray.integral_sq_timePartial_eq (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (k : Fin 3) {T : ℝ} (hT : 0 < T) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {c d : ℝ} (hc : 0 < c) (hcd : c < d) (hdT : d < T) (hψs : ∀ z ∈ tsupport ψ, z.2 ∈ Set.Ioo c d) : ∫ (t : ℝ) in Set.Ioo 0 T, ∫ (x : Foundation.Parabolic.Vec3), forcedRegRep ρ ε hε ha hf (x, t) k * (forcedRegRep ρ ε hε ha hf (x, t) k * timePartial ψ (x, t)) = 2 * ∫ (t : ℝ) in Set.Ioo 0 T, leLimitT ρ ε hε ha hf ψ k t

The mollifier limit of the space-time energy identity of one component.