Integrability of the scalar commutator density

The compact-support property needed to compare the pointwise half-space commutator bound with the integrated identity in eq:carleman-commutator.

@[instance_reducible]

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

The product norm on parabolic space-time used for classical differentiation.

Equations

• ESS.carlemanCoreIntegrabilityNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

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

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

Equations

• ESS.carlemanCoreIntegrabilityNormedSpace = CKN.carlemanProductNormedSpace

theorem ESS.carlemanCommutatorDensity_tsupport_subset (φ v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : tsupport (CKN.carlemanCommutatorDensity φ v) ⊆ tsupport v

The commutator density vanishes off the support of the field.

theorem ESS.integrable_carlemanCommutatorDensity {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) : MeasureTheory.Integrable (CKN.carlemanCommutatorDensity φ v) MeasureTheory.volume

The scalar commutator density is integrable for a smooth, compactly supported field and a phase smooth near its support.