Limit passages for the rough forced heat response #
Two convergence mechanisms pass the weak identities of smooth forced heat
responses to the rough response of lem:pv-stokes: L² convergence against
square-integrable tests, and weighted L¹ convergence of the responses
against continuous compactly supported tests.
theorem
ESS.tendsto_integral_mul_of_eLpNorm_two
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : ℕ → α → ℝ}
{F ψ : α → ℝ}
(hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ)
(hF : MeasureTheory.MemLp F 2 μ)
(hψ : MeasureTheory.MemLp ψ 2 μ)
(hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - F) 2 μ) Filter.atTop (nhds 0))
:
Integrals against a fixed square-integrable function converge along an L²
convergent sequence.
theorem
ESS.abs_le_mul_forcedHeatWeight
{ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hψ : Continuous ψ)
(hψc : HasCompactSupport ψ)
:
A continuous compactly supported function is dominated by a multiple of the
weight forcedHeatWeight.
theorem
ESS.kernelResponse_integral_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))
{ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hψ : Continuous ψ)
(hψc : HasCompactSupport ψ)
(i : Fin 3)
:
MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => kernelResponse g z i * ψ z)
(MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo 0 τ)) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo 0 τ, kernelResponse (gn n) z i * ψ z)
Filter.atTop
(nhds (∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo 0 τ, kernelResponse g z i * ψ z))
Integrals of the responses against a continuous compactly supported test
converge on the slab along an L² convergent smooth approximation.