The flux of the time-difference quotients is square integrable

prop:lps-smoothing: let u be a strong solution, h > 0, v = (u(·, · + h) - u)/h and Hᵢⱼ = ((uᵢuⱼ)(·, · + h) - uᵢuⱼ)/h = vᵢ uⱼ(·, · + h) + uᵢ vⱼ. If uᵢ(x, t)² ≤ K M(t) for almost every (x, t) with M integrable in time, then at almost every time ∑ᵢⱼ Hᵢⱼ² ≤ 6K (M(t) + M(t + h)) |v|² pointwise, and H is square integrable on the slab over (t₀, T - h), since the energy ∫ |v(x, t)|² dx is continuous on [t₀, T - h].

theorem ESS.lps_flux_sum_sq_le {v w u : Fin 3 → ℝ} {A B : ℝ} (hw : ∀ (j : Fin 3), w j ^ 2 ≤ A) (hu : ∀ (j : Fin 3), u j ^ 2 ≤ B) : ∑ i : Fin 3, ∑ j : Fin 3, (v i * w j + u i * v j) ^ 2 ≤ 6 * (A + B) * ∑ i : Fin 3, v i ^ 2

The flux vᵢwⱼ + uᵢvⱼ is bounded by the pointwise bounds of the components of w and u (prop:lps-smoothing).

theorem ESS.lps_ae_restrict_Ioo_shift {a b h : ℝ} (hh : 0 ≤ h) {P : ℝ → Prop} (hP : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), P t) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a (b - h)), P (t + h)

A property holding at almost every time of (a, b) holds at t + h for almost every time t of (a, b - h), when h ≥ 0.

theorem ESS.lps_curve_energy_continuousOn {S : Set ℝ} {f : ℝ → CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hf : ∀ t ∈ S, MeasureTheory.MemLp (f t) 2 MeasureTheory.volume) (hcont : ∀ t ∈ S, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f s x - f t x) 2 MeasureTheory.volume) (nhdsWithin t S) (nhds 0)) : ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f t x i ^ 2) S

The kinetic energy of an L²-continuous curve of square-integrable vector fields is continuous.

theorem ESS.lps_diffQuotient_slice_continuous {t₀ T h : ℝ} (hh : 0 < h) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc t₀ T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ T)) (nhds 0)) : (∀ t ∈ Set.Icc t₀ (T - h), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => (1 / h) • (u (x, t + h) - u (x, t))) 2 MeasureTheory.volume) ∧ ∀ t ∈ Set.Icc t₀ (T - h), Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => (1 / h) • (u (x, s + h) - u (x, s)) - (1 / h) • (u (x, t + h) - u (x, t))) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ (T - h))) (nhds 0)

The time-difference quotients of an L²-continuous curve of square-integrable slices form an L²-continuous curve of square-integrable slices on [t₀, T - h].

theorem ESS.lps_diffQuotient_energy_continuousOn {t₀ T h : ℝ} (hh : 0 < h) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc t₀ T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ T)) (nhds 0)) : ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (1 / h * (u (x, t + h) i - u (x, t) i)) ^ 2) (Set.Icc t₀ (T - h))

The energy ∫ |v(x, t)|² dx of the time-difference quotient v = (u(·, · + h) - u)/h is continuous on [t₀, T - h] (prop:lps-smoothing).

theorem ESS.lps_flux_slice_bound {t₀ T h K : ℝ} {M : ℝ → ℝ} (hh : 0 < h) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hK : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∀ (i : Fin 3), u (x, t) i ^ 2 ≤ K * M t) : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ (T - h)), (∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => 1 / h * (u (x, τ + h) i * u (x, τ + h) j - u (x, τ) i * u (x, τ) j)) 2 MeasureTheory.volume) ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (1 / h * (u (x, τ + h) i * u (x, τ + h) j - u (x, τ) i * u (x, τ) j)) ^ 2 ≤ 6 * K * (M τ + M (τ + h)) * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (1 / h * (u (x, τ + h) i - u (x, τ) i)) ^ 2

At almost every time of (t₀, T - h), the difference quotient of the convective flux is square integrable in space and ∫ ∑ᵢⱼ Hᵢⱼ² ≤ 6K (M(t) + M(t + h)) ∫ |v|², given the pointwise bound uᵢ(x, t)² ≤ K M(t) (prop:lps-smoothing).

theorem ESS.lps_flux_memLp {t₀ T h K : ℝ} {M : ℝ → ℝ} (hh : 0 < h) (hhT : h < T - t₀) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc t₀ T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ T)) (nhds 0)) (hK0 : 0 ≤ K) (hM0 : ∀ (t : ℝ), 0 ≤ M t) (hM : MeasureTheory.Integrable M (MeasureTheory.volume.restrict (Set.Ioo t₀ T))) (hK : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∀ (i : Fin 3), u (x, t) i ^ 2 ≤ K * M t) (i j : Fin 3) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => 1 / h * (u (z.1, z.2 + h) i * u (z.1, z.2 + h) j - u z i * u z j)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h))))

The difference quotient of the convective flux is square integrable on the slab over (t₀, T - h), given the pointwise bound uᵢ(x, t)² ≤ K M(t) with M integrable in time (prop:lps-smoothing).