The small heat orbit #
This file proves lem:pv-small-heat: for a ∈ L² ∩ L³ the norms of the heat
orbit in L⁵(Q_τ) and L⁴(Q_τ) tend to zero as τ ↓ 0. By
lem:pv-heat-critical the orbit lies in both spaces on the slab Q_1, and the
slabs Q_τ decrease to the empty set, so the claim is the absolute continuity
of the integral.
theorem
ESS.tendsto_eLpNorm_spaceTimeSet_zero
{E : Type u_1}
[NormedAddCommGroup E]
{F : CKN.Foundation.Parabolic.ParabolicPoint → E}
{r : ENNReal}
(hr0 : r ≠ 0)
(hrtop : r ≠ ⊤)
(hF :
∀ (τ : ℝ), 0 < τ → MeasureTheory.MemLp F r (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))))
:
Filter.Tendsto
(fun (τ : ℝ) => MeasureTheory.eLpNorm F r (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))))
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
A function lying in Lʳ of every slab ℝ³ × (0, τ) has Lʳ norms on
these slabs tending to zero as τ ↓ 0.
theorem
ESS.pvSmallHeat
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(ha2 : MeasureTheory.MemLp a 2 MeasureTheory.volume)
(ha3 : MeasureTheory.MemLp a 3 MeasureTheory.volume)
:
Filter.Tendsto
(fun (τ : ℝ) =>
MeasureTheory.eLpNorm (heatOrbit a) 5 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) + MeasureTheory.eLpNorm (heatOrbit a) 4 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))))
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
lem:pv-small-heat: for a ∈ L² ∩ L³,
‖S(·)a‖_{L⁵(Q_τ)} + ‖S(·)a‖_{L⁴(Q_τ)} → 0 as τ ↓ 0.