Removing the mollification and cutoff from space-time pairings #
On the slab ℝ³ × (0, t), pairings of slice-wise mollified fields weighted by
the cutoffs converge to the pairings of the fields, and those weighted by
cutoff gradients tend to zero. These are the limit terms of the cross-testing
identity in lem:pv-serrin-uniqueness.
theorem
ESS.serrinSM_tendsto_restrict
{t T : ℝ}
(ht : t ≤ T)
{f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{p : ENNReal}
(hp : 1 ≤ p)
(hptop : p ≠ ⊤)
(hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
Filter.Tendsto
(fun (n : ℕ) =>
MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinSM f n z - f z) p
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t))))
Filter.atTop (nhds 0)
Slice-wise mollification converges in L^p on every shorter slab.
theorem
ESS.serrin_cutoff_pairing_limit
{t T : ℝ}
(ht : t ≤ T)
{p q : ENNReal}
[p.HolderTriple q 1]
(hp : 1 ≤ p)
(hptop : p ≠ ⊤)
(hq : 1 ≤ q)
(hqtop : q ≠ ⊤)
{f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hg : MeasureTheory.MemLp g q (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCutoff n z.1 * serrinSM f n z * serrinSM g n z)
Filter.atTop
(nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), f z * g z))
Cutoff-weighted pairings of mollified fields converge to the pairing of the fields.
theorem
ESS.serrin_cutoff_deriv_pairing_limit
{t T : ℝ}
(ht : t ≤ T)
{p q : ENNReal}
[p.HolderTriple q 1]
(hp : 1 ≤ p)
(hptop : p ≠ ⊤)
(hq : 1 ≤ q)
(hqtop : q ≠ ⊤)
{f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hg : MeasureTheory.MemLp g q (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(j : Fin 3)
:
Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), CKN.spatialDeriv (serrinCutoff n) j z.1 * serrinSM f n z * serrinSM g n z)
Filter.atTop (nhds 0)
Pairings of mollified fields weighted by a cutoff gradient tend to zero.
theorem
ESS.serrinSM_memLp_eventually
{t T : ℝ}
(ht : t ≤ T)
{f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{p : ENNReal}
(hp : 1 ≤ p)
(hptop : p ≠ ⊤)
(hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.MemLp (serrinSM f n) p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))
Slice-wise mollifications of an L^p field are eventually in L^p on
every shorter slab.
theorem
ESS.serrin_weighted_term_integrable
{t T : ℝ}
(ht : t ≤ T)
{p q : ENNReal}
[p.HolderTriple q 1]
(hp : 1 ≤ p)
(hptop : p ≠ ⊤)
(hq : 1 ≤ q)
(hqtop : q ≠ ⊤)
{f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hg : MeasureTheory.MemLp g q (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
{c : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hc : ∀ (n : ℕ), Continuous (c n))
(hcb : ∀ (n : ℕ), ∃ (C : ℝ), ∀ (y : CKN.Foundation.Parabolic.Vec3), |c n y| ≤ C)
:
∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => c n z.1 * serrinSM f n z * serrinSM g n z)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))
A bounded continuous weight times two slice-wise mollified fields in conjugate spaces is eventually integrable on the shorter slab.