The kernel formula for rough tensors

For a tensor in L² vanishing at nonpositive times, the kernel integrals defining the forced heat response converge absolutely at almost every point of the slab ℝ³ × (0,τ), the response is measurable, and responses of approximating tensors converge to it in the weighted L¹ sense and hence, along a subsequence, almost everywhere on the slab. This identifies the rough response of lem:pv-stokes with limits of smooth responses.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume_3 : MeasureTheory.volume.IsAddHaarMeasure

noncomputable def ESS.kernelResponse (g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.Foundation.Parabolic.Vec3

The kernel formula of the forced heat response for a tensor on Vec3 × ℝ.

Equations

• ESS.kernelResponse g z i = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ j : Fin 3, CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * g i j (z - p)

theorem ESS.forcedHeat_eq_kernelResponse (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : forcedHeat G z = kernelResponse (fun (i j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) z

The forced heat response is the kernel formula of its tensor.

theorem ESS.kernelResponse_component_aestronglyMeasurable {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), MeasureTheory.AEStronglyMeasurable (g i j) MeasureTheory.volume) (i : Fin 3) : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => kernelResponse g z i) MeasureTheory.volume

The kernel response of a measurable tensor is measurable.

theorem ESS.kernel_integrable_ae_slab {τ : ℝ} (hτ : 0 < τ) (j : Fin 3) {H : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hH : MeasureTheory.MemLp H 2 MeasureTheory.volume) (hsupp : ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), H z ≠ 0 → 0 < z.2) : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo 0 τ), MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * H (z - p)) MeasureTheory.volume

For a source in L² vanishing at nonpositive times, the kernel integral is absolutely convergent at almost every point of the slab.

theorem ESS.kernel_weighted_aemeasurable (j : Fin 3) {H : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hH : MeasureTheory.AEStronglyMeasurable H MeasureTheory.volume) (μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)) (hμ : μ.AbsolutelyContinuous MeasureTheory.volume) : AEMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ENNReal.ofReal (forcedHeatWeight z.1) * ∫⁻ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ‖CKN.Foundation.Heat.heatKernelSpaceDerivative p.1 p.2 j * H (z - p)‖ₑ) μ

The weighted kernel lintegral is measurable in the base point.

theorem ESS.kernelResponse_weighted_tendsto {τ : ℝ} (hτ : 0 < τ) {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {gn : ℕ → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (g i j) 2 MeasureTheory.volume) (hgsupp : ∀ (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), g i j z ≠ 0 → 0 < z.2) (hgn : ∀ (n : ℕ) (i j : Fin 3), ContDiff ℝ (↑⊤) (gn n i j)) (hgnc : ∀ (n : ℕ) (i j : Fin 3), HasCompactSupport (gn n i j)) (hgnpos : ∀ (n : ℕ) (i j : Fin 3), tsupport (gn n i j) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) (hconv : ∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (gn n i j - g i j) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo 0 τ, ENNReal.ofReal (forcedHeatWeight z.1) * ‖kernelResponse (gn n) z - kernelResponse g z‖ₑ) Filter.atTop (nhds 0)

Responses of smooth tensors converging in L² to a rough tensor converge to the rough response in the weighted L¹ sense on the slab.

theorem ESS.kernelResponse_ae_subseq {τ : ℝ} (hτ : 0 < τ) {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {gn : ℕ → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (g i j) 2 MeasureTheory.volume) (hgsupp : ∀ (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), g i j z ≠ 0 → 0 < z.2) (hgn : ∀ (n : ℕ) (i j : Fin 3), ContDiff ℝ (↑⊤) (gn n i j)) (hgnc : ∀ (n : ℕ) (i j : Fin 3), HasCompactSupport (gn n i j)) (hgnpos : ∀ (n : ℕ) (i j : Fin 3), tsupport (gn n i j) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) (hconv : ∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (gn n i j - g i j) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo 0 τ), Filter.Tendsto (fun (k : ℕ) => kernelResponse (gn (ns k)) z) Filter.atTop (nhds (kernelResponse g z))

Along a subsequence, responses of smooth approximants converge almost everywhere on the slab to the rough response.