Algebra of the scalar Carleman commutator

This is the finite-dimensional polynomial identity underlying eq:carleman-commutator. Its variables stand for the coordinate derivatives of a scalar field and a smooth phase.

@[instance_reducible]

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

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

Equations

• ESS.carlemanCoreCommutatorAlgebraNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

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

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

Equations

• ESS.carlemanCoreCommutatorAlgebraNormedSpace = CKN.carlemanProductNormedSpace

noncomputable def ESS.commutatorSymmetric (φ v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The symmetric part of the time-weighted conjugated heat operator in eq:carleman-S.

Equations

• ESS.commutatorSymmetric φ v z = z.2 * CKN.scalarLaplacian v z + z.2 * (CKN.scalarGradSq φ z - CKN.timePartial φ z) * v z - v z / 2

noncomputable def ESS.commutatorSkew (φ v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The skew part of the time-weighted conjugated heat operator in eq:carleman-A.

Equations

• ESS.commutatorSkew φ v z = z.2 * CKN.timePartial v z + v z / 2 - z.2 * (2 * ∑ i : Fin 3, CKN.spatialPartial φ i z * CKN.spatialPartial v i z + CKN.scalarLaplacian φ z * v z)

noncomputable def ESS.commutatorTimeFlux (φ v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The time flux whose derivative appears in the scalar commutator identity eq:carleman-commutator.

Equations

• ESS.commutatorTimeFlux φ v z = (CKN.scalarGradSq φ z - CKN.timePartial φ z) * (z.2 ^ 2 * v z ^ 2) - z.2 ^ 2 * CKN.scalarGradSq v z - 1 / 2 * (z.2 * v z ^ 2)

noncomputable def ESS.commutatorSpaceFlux (φ v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The spatial flux whose divergence appears in the scalar commutator identity eq:carleman-commutator.

Equations

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

theorem ESS.commutator_pointwise_divergence {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) : 2 * commutatorSymmetric φ v z * commutatorSkew φ v z = CKN.carlemanCommutatorDensity φ v z + CKN.timePartial (commutatorTimeFlux φ v) z + ∑ i : Fin 3, CKN.spatialPartial (commutatorSpaceFlux φ v i) i z

The scalar commutator pairing equals its density plus the derivatives of compactly supported space-time fluxes.