Semigroup identities for the regularized mild equation

These identities express restarting the Fourier heat evolution and its projected divergence term at an intermediate time.

theorem CKN.Leray.lpMultiplier_add (m : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f g : ↥ComplexVectorL2) : m • (f + g) = m • f + m • g

theorem CKN.Leray.lpMultiplier_smul (m : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (c : ℂ) (f : ↥ComplexVectorL2) : m • c • f = c • m • f

noncomputable def CKN.Leray.complexSchwartzToL2 (g : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : ↥ComplexVectorL2

The spatial L² class of a Schwartz vector field.

Equations

• CKN.Leray.complexSchwartzToL2 g = g.toLp 2 MeasureTheory.volume

noncomputable def CKN.Leray.heatSemigroupCLM (t : ℝ) (ht : 0 ≤ t) : ↥ComplexVectorL2 →L[ℂ] ↥ComplexVectorL2

The complex heat evolution as a bounded linear operator on spatial L².

Equations

• CKN.Leray.heatSemigroupCLM t ht = { toFun := CKN.Leray.heatSemigroup t ht, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem CKN.Leray.heatSemigroupCLM_apply (t : ℝ) (ht : 0 ≤ t) (f : ↥ComplexVectorL2) : (heatSemigroupCLM t ht) f = heatSemigroup t ht f