Time increments of solenoidal pairings for the forced regularized solutions

The forced regularized solutions of lem:regularised-forced are only continuous L² mild solutions, so the time regularity of a spatial pairing comes from the weak momentum identity eq:reg-momentum-forced, as in lem:forced-equicontinuity. For a smooth, compactly supported, divergence-free spatial field w, testing the identity with η(t) w(x) shows that t ↦ ∫ u(t)·w has the weak time derivative ∫ ((J u)_j u_i ∂_j w_i - (Du)_{ij} ∂_j w_i + f·w): the pressure drops out. Continuity of the pairing then identifies each increment from time 0 with the space-time integral of this flux.

noncomputable def CKN.Leray.forcedHopfPairingFlux (J U f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (wc : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The flux density of the forced momentum identity against a spatial test field wc: transport, viscous and force contributions.

Equations

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

theorem CKN.Leray.forcedHopf_transport_integrable {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {V W : α → Foundation.Parabolic.Vec3} {φ : Fin 3 → Fin 3 → α → ℝ} (hV : MeasureTheory.MemLp V 3 μ) (hW : MeasureTheory.MemLp W 3 μ) (hφ : ∀ (i j : Fin 3), MeasureTheory.MemLp (φ i j) ⊤ μ) : MeasureTheory.Integrable (fun (x : α) => ∑ i : Fin 3, ∑ j : Fin 3, V x j * W x i * φ i j x) μ

The transport term of two L³ fields against bounded coefficients is integrable on a finite measure space.

theorem CKN.Leray.forcedHopf_memLp_top_spatial {μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint} {g : Foundation.Parabolic.Vec3 → ℝ} (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => g z.1) ⊤ μ

A continuous compactly supported spatial function is bounded on space-time.

theorem CKN.Leray.forcedHopf_slab_isFiniteMeasure {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (T : ℝ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (spaceTimeSet K (Set.Ioo 0 T)))

The slab K × (0,T) over a compact spatial set has finite measure.

theorem CKN.Leray.forcedHopf_spatialDeriv_memLp_top {μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint} {g : Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (j : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialDeriv g j z.1) ⊤ μ

The spatial derivatives of a smooth compactly supported spatial function are bounded on space-time.

theorem CKN.Leray.forcedHopf_pairingFlux_integrable {T : ℝ} {J U f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {wc : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (wc i)) {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hwK : ∀ (i : Fin 3), tsupport (wc i) ⊆ K) (hJ : MeasureTheory.MemLp J 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hU : MeasureTheory.MemLp U 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hD : MeasureTheory.MemLp D 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) : MeasureTheory.Integrable (forcedHopfPairingFlux J U f D wc) (MeasureTheory.volume.restrict (spaceTimeSet K (Set.Ioo 0 T)))

The flux density is integrable on the slab over a compact spatial set carrying the test field.

theorem CKN.Leray.forcedHopf_regPairing_sub_eq {T : ℝ} (hT : 0 < T) {U J f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {P : Foundation.Parabolic.ParabolicPoint → ℝ} {wc : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (wc i)) {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hwK : ∀ (i : Fin 3), tsupport (wc i) ⊆ K) (hdivw : ∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, spatialDeriv (wc i) i x = 0) (hU : MeasureTheory.MemLp U 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hJ : MeasureTheory.MemLp J 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hD : MeasureTheory.MemLp D 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hcont : ContinuousOn (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * wc i x) (Set.Ici 0)) (hmom : ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, U z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, J z j * U z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, D z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - P z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, f z i * φ z i = 0) (t : ℝ) : t ∈ Set.Ioo 0 T → (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * wc i x) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, 0) i * wc i x = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet K (Set.Ioo 0 t), forcedHopfPairingFlux J U f D wc z

The increment of a solenoidal pairing of a forced regularized solution from time 0 is the space-time integral of the flux, by the weak momentum identity eq:reg-momentum-forced tested with η(t) w(x) and the continuity of the pairing.