The fixed point of the Duhamel map

For a datum in L² ∩ L³ the Duhamel map of prop:pv-local-solution has a fixed point in L⁵ ∩ L⁴ of a short slab: the heat orbit is small there (lem:pv-small-heat), and the map is quadratically Lipschitz with a constant independent of the length of the slab. The fixed point is then normalized so that the fixed-point identity holds at every positive time and the datum is its value at time zero.

theorem ESS.rieszPressureSpaceTime_ae_zero (r : ℝ) (hr : 1 < r) (F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume) (h0 : ∀ (i j : Fin 3), F i j =ᵐ[MeasureTheory.volume] 0) : CKN.Leray.rieszPressureSpaceTime r hr F hF =ᵐ[MeasureTheory.volume] 0

The canonical Riesz pressure of a tensor vanishing almost everywhere vanishes almost everywhere.

theorem ESS.pvLocalMap_zero (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (σ : ℝ) : pvLocalMap a σ 0 = heatOrbit a

The forcing of the zero velocity vanishes, so the Duhamel map sends zero to the heat orbit.

theorem ESS.pvLocalMap_congr {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {σ : ℝ} {U V : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hUV : U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))] V) : pvLocalMap a σ U = pvLocalMap a σ V

The Duhamel map only sees the velocity almost everywhere on the slab.

theorem ESS.pvLocalMap_memLp {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha2 : MeasureTheory.MemLp a 2 MeasureTheory.volume) (ha3 : MeasureTheory.MemLp a 3 MeasureTheory.volume) {σ : ℝ} (hσ : 0 < σ) {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hU5 : MeasureTheory.MemLp U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) (hU4 : MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) : MeasureTheory.MemLp (pvLocalMap a σ U) (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) ∧ MeasureTheory.MemLp (pvLocalMap a σ U) (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))

The Duhamel map sends L⁵ ∩ L⁴ of the slab to itself.

theorem ESS.pvLocal_fixedPoint {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha2 : MeasureTheory.MemLp a 2 MeasureTheory.volume) (ha3 : MeasureTheory.MemLp a 3 MeasureTheory.volume) : ∃ (σ : ℝ), 0 < σ ∧ ∃ (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), MeasureTheory.MemLp U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) ∧ MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) ∧ (∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≠ 0 → U z = pvLocalMap a σ U z) ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), U (x, 0) = a x

The Duhamel map has a fixed point in L⁵ ∩ L⁴ of a short slab, which satisfies the fixed-point identity at every nonzero time and equals the datum at time zero.