Limits of the mollified weak heat solution

The uniform limit Z of the mollified curves is continuous on [a, τ], starts at w₀, and agrees with the time slices of w for almost every time. The mollified gradients converge in L² of the slab to the weak gradient of w (lem:localized-vorticity-energy).

theorem ESS.vl_integral_mul_eq_inner {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g ψ : α → ℝ} (hg : MeasureTheory.MemLp g 2 μ) (hψ : MeasureTheory.MemLp ψ 2 μ) : ∫ (x : α), g x * ψ x ∂μ = inner ℝ (MeasureTheory.MemLp.toLp g hg) (MeasureTheory.MemLp.toLp ψ hψ)

An integral of a product of square-integrable functions is an L² inner product.

noncomputable def ESS.vlLimit {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (t : ↑(Set.Icc a τ)) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The limit curve.

Equations

• ESS.vlLimit sol t = Filter.atTop.limUnder fun (n : ℕ) => ESS.vlCurve sol n t

theorem ESS.vlLimit_tendsto {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (t : ↑(Set.Icc a τ)) : Filter.Tendsto (fun (n : ℕ) => vlCurve sol n t) Filter.atTop (nhds (vlLimit sol t))

theorem ESS.vlLimit_continuous {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) : Continuous (vlLimit sol)

theorem ESS.vlLimit_initial {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) : vlLimit sol ⟨a, ⋯⟩ = MeasureTheory.MemLp.toLp w₀ ⋯

At the initial time the limit is the initial datum.

noncomputable def ESS.vlPrimM (a : ℝ) (k w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

A jointly measurable version of the time primitive.

Equations

• ESS.vlPrimM a k w₀ w H f p = CKN.vlConv k w₀ p.1 + ∫ (s : ℝ), (Set.Ioc a p.2).indicator (fun (s : ℝ) => CKN.vlSource k w H f p.1 s) s

theorem ESS.vlPrimM_eq (a : ℝ) (k w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (x : CKN.Foundation.Parabolic.Vec3) {t : ℝ} (ht : a ≤ t) : vlPrimM a k w₀ w H f (x, t) = CKN.vlPrim a k w₀ w H f x t

theorem ESS.vlPrimM_stronglyMeasurable {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) : MeasureTheory.StronglyMeasurable (vlPrimM a k w₀ w H f)

theorem ESS.vlPrim_slice_ae {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (n : ℕ) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlPrim a (CKN.vlMoll n) w₀ w H f x t = CKN.vlConvT (CKN.vlMoll n) w x t

For almost every time, each mollified primitive is the mollification of the time slice.

theorem ESS.vlLimit_slice_ae {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), ∀ (ht : t ∈ Set.Icc a τ), ↑↑(vlLimit sol ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, t)

For almost every time, the limit curve is the time slice of w.