The heat multiplier on spatial L²

The heat operator is the inverse Fourier transform of multiplication by its Gaussian symbol, as in sec:regularised.

noncomputable def CKN.Leray.heatSymbol (t : ℝ) (ξ : Foundation.Parabolic.L2Vec3) : ℂ

The heat symbol in the Fourier convention of sec:regularised.

Equations

• CKN.Leray.heatSymbol t ξ = ↑(Real.exp (-4 * Real.pi ^ 2 * t * ‖ξ‖ ^ 2))

theorem CKN.Leray.heatSymbol_norm_le_one {t : ℝ} (ht : 0 ≤ t) (ξ : Foundation.Parabolic.L2Vec3) : ‖heatSymbol t ξ‖ ≤ 1

The heat symbol is bounded by one for nonnegative time.

noncomputable def CKN.Leray.heatMultiplier (t : ℝ) (ht : 0 ≤ t) : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)

The heat multiplier as a bounded multiplier on frequency-space L².

Equations

• CKN.Leray.heatMultiplier t ht = MeasureTheory.MemLp.toLp (CKN.Leray.heatSymbol t) ⋯

theorem CKN.Leray.heatMultiplier_norm_le_one (t : ℝ) (ht : 0 ≤ t) : ‖heatMultiplier t ht‖ ≤ 1

The Gaussian multiplier has essential-supremum norm at most one.

noncomputable def CKN.Leray.heatSemigroup (t : ℝ) (ht : 0 ≤ t) (v : ↥(MeasureTheory.Lp ComplexVec3 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ComplexVec3 2 MeasureTheory.volume)

The heat semigroup on complex velocity L², defined by its Fourier multiplier.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.heatSemigroup_norm_le (t : ℝ) (ht : 0 ≤ t) (v : ↥(MeasureTheory.Lp ComplexVec3 2 MeasureTheory.volume)) : ‖heatSemigroup t ht v‖ ≤ ‖v‖

The heat semigroup is an L² contraction, by Plancherel and the Gaussian symbol bound in lem:reg-multiplier-bounds.