Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.FourierHeatDivergence

The heat multiplier and Fourier divergence #

Scalar heat multiplication preserves Fourier orthogonality to the spatial frequency, the Fourier-side ingredient for the divergence assertion in lem:reg-multiplier-bounds.

source
theorem CKN.Leray.heatSemigroup_preserves_fourierOrthogonal (t : ℝ) (ht : 0 ≤ t) (v : ↥ComplexVectorL2) (hv : ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), inner ℂ (complexifyFrequency ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) ξ) = 0) :
∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), inner ℂ (complexifyFrequency ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (heatSemigroup t ht v)) ξ) = 0

The heat semigroup preserves frequency orthogonality to the divergence direction.

source
theorem CKN.Leray.realHeatOperator_isInJ_of_fourierOrthogonal (t : ℝ) (ht : 0 ≤ t) (f : ↥RealVectorL2) (hf : ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), inner ℂ (complexifyFrequency ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 f)) ξ) = 0) :
IsInJ (realVectorL2Representative (realHeatOperator t ht f))

The real heat operator has weakly divergence-free range whenever its complex Fourier input is orthogonal to frequency.