Real heat evolution as a continuous linear operator

The real Fourier heat map is bounded and therefore commutes with Bochner integration on finite intervals.

noncomputable def CKN.Leray.realHeatOperatorCLM (t : ℝ) (ht : 0 ≤ t) : ↥RealVectorL2 →L[ℝ] ↥RealVectorL2

The real heat operator as a bounded real-linear map on spatial L².

Equations

• CKN.Leray.realHeatOperatorCLM t ht = CKN.Leray.realPartVectorL2 ∘SL ContinuousLinearMap.restrictScalars ℝ (CKN.Leray.heatSemigroupCLM t ht) ∘SL CKN.Leray.complexifyVectorL2

theorem CKN.Leray.realHeatOperatorCLM_apply (t : ℝ) (ht : 0 ≤ t) (b : ↥RealVectorL2) : (realHeatOperatorCLM t ht) b = realHeatOperator t ht b

The bounded real-linear heat map agrees with the Fourier definition.