Integrated scalar Carleman commutator estimate

Compact support eliminates the space-time fluxes in eq:carleman-commutator; the remaining two squares give the lower bound.

@[instance_reducible]

def ESS.carlemanCoreCommutatorIntegralNormedAddCommGroup : NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

The product norm on parabolic space-time used in this identity.

Equations

• ESS.carlemanCoreCommutatorIntegralNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

noncomputable def ESS.carlemanCoreCommutatorIntegralNormedSpace : NormedSpace ℝ CKN.Foundation.Parabolic.ParabolicPoint

The real scalar action compatible with the product norm on parabolic space-time.

Equations

• ESS.carlemanCoreCommutatorIntegralNormedSpace = CKN.carlemanProductNormedSpace

@[instance_reducible]

noncomputable def ESS.carlemanCoreCommutatorIntegralMeasureSpace : MeasureTheory.MeasureSpace CKN.Foundation.Parabolic.ParabolicPoint

Product Lebesgue measure on parabolic space-time.

Equations

• ESS.carlemanCoreCommutatorIntegralMeasureSpace = MeasureTheory.Measure.prod.measureSpace

theorem ESS.contDiff_of_local_and_tsupport {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hFU : tsupport f ⊆ U) : ContDiff ℝ (↑⊤) f

A function smooth on an open set containing its support is smooth.

theorem ESS.integrable_sq_smooth_compact {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f z ^ 2) MeasureTheory.volume

The square of a smooth compactly supported scalar field is integrable.

theorem ESS.carleman_commutator_le {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ U) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.carlemanCommutatorDensity φ v z ≤ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * CKN.carlemanConj φ v z ^ 2

The commutator density is bounded by the square of the conjugated heat operator, as used in eq:carleman-commutator-energy.