Derivatives of the Carleman phase quantities

The coordinate rules here expand the squared gradient and spatial Laplacian in the commutator identity eq:carleman-commutator.

@[instance_reducible]

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

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

Equations

• ESS.carlemanCoreCommDerivativesNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

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

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

Equations

• ESS.carlemanCoreCommDerivativesNormedSpace = CKN.carlemanProductNormedSpace

theorem ESS.spatialPartial_time_pow_mul_at (m : ℕ) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hf : DifferentiableAt ℝ f z) (i : Fin 3) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => y.2 ^ m * f y) i z = z.2 ^ m * CKN.spatialPartial f i z

Spatial differentiation ignores a factor depending only on time.

theorem ESS.spatialPartial_const_mul_at (c : ℝ) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hf : DifferentiableAt ℝ f z) (i : Fin 3) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => c * f y) i z = c * CKN.spatialPartial f i z

A real constant factors out of a spatial coordinate derivative.

theorem ESS.spatialPartial_const_time_pow_mul_at (c : ℝ) (m : ℕ) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hf : DifferentiableAt ℝ f z) (i : Fin 3) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => c * (y.2 ^ m * f y)) i z = c * z.2 ^ m * CKN.spatialPartial f i z

A constant times an integral time power factors out of a spatial coordinate derivative.

theorem ESS.timePartial_scalarGradSq_on {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) : CKN.timePartial (CKN.scalarGradSq f) z = 2 * ∑ i : Fin 3, CKN.spatialPartial f i z * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial f i y) z

The time derivative of a squared spatial gradient.

theorem ESS.spatialPartial_scalarGradSq_on {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (j : Fin 3) : CKN.spatialPartial (CKN.scalarGradSq f) j z = 2 * ∑ i : Fin 3, CKN.spatialPartial f i z * CKN.spatialSecondPartial f i j z

A spatial derivative of a squared spatial gradient.

theorem ESS.timePartial_carlemanPotential_on {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) : CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.scalarGradSq f y - CKN.timePartial f y) z = 2 * ∑ i : Fin 3, CKN.spatialPartial f i z * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial f i y) z - CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial f y) z

The time derivative of the zeroth-order conjugation potential.

theorem ESS.spatialPartial_carlemanPotential_on {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.scalarGradSq f y - CKN.timePartial f y) i z = 2 * ∑ j : Fin 3, CKN.spatialPartial f j z * CKN.spatialSecondPartial f j i z - CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial f i y) z

A spatial derivative of the zeroth-order conjugation potential.

theorem ESS.spatialPartial_gradientDot_on {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, CKN.spatialPartial f j y * CKN.spatialPartial g j y) i z = ∑ j : Fin 3, (CKN.spatialSecondPartial f j i z * CKN.spatialPartial g j z + CKN.spatialPartial f j z * CKN.spatialSecondPartial g j i z)

Product rule for the spatial dot product of two gradients.

theorem ESS.spatialPartial_scalarLaplacian_on {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) : CKN.spatialPartial (CKN.scalarLaplacian f) i z = ∑ j : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialSecondPartial f j j y) i z

A spatial derivative distributes over the scalar Laplacian.

theorem ESS.scalarLaplacian_second_diagonal_on {U : Set CKN.Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) : ∑ i : Fin 3, CKN.spatialSecondPartial (CKN.scalarLaplacian f) i i z = ∑ j : Fin 3, ∑ i : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialSecondPartial f j j y) i i z

The spatial bi-Laplacian is the double sum of fourth coordinate derivatives.