Second spatial derivatives on an open domain

The local second derivative product rule used in prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript.

@[instance_reducible]

def CKN.carlemanCoreSecondNormedAddCommGroup : NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure used for second-derivative identities.

Equations

• CKN.carlemanCoreSecondNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

noncomputable def CKN.carlemanCoreSecondNormedSpace : NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

The real product normed-space structure used for second-derivative identities.

Equations

• CKN.carlemanCoreSecondNormedSpace = CKN.carlemanProductNormedSpace

theorem CKN.differentiableAt_spatialPartial_slice {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) : DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => spatialPartial f i (x, z.2)) z.1

A spatial derivative of a smooth function is differentiable along each spatial slice.

theorem CKN.spatialSecondPartial_mul_at {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {a b : Foundation.Parabolic.ParabolicPoint → ℝ} (ha : ContDiffOn ℝ (↑⊤) a U) (hb : ContDiffOn ℝ (↑⊤) b U) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i j : Fin 3) : spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => a y * b y) i j z = spatialSecondPartial a i j z * b z + spatialPartial a i z * spatialPartial b j z + spatialPartial a j z * spatialPartial b i z + a z * spatialSecondPartial b i j z

Local product rule for an iterated spatial derivative.

theorem CKN.spatialSecondPartial_exp_at {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i j : Fin 3) : spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y)) i j z = Real.exp (φ z) * (spatialSecondPartial φ i j z + spatialPartial φ i z * spatialPartial φ j z)

The second spatial derivative of an exponential phase.

theorem CKN.spatialSecondPartial_exp_mul_at {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ w : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hw : ContDiff ℝ (↑⊤) w) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i j : Fin 3) : spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y) * w y) i j z = Real.exp (φ z) * (spatialSecondPartial w i j z + spatialPartial φ i z * spatialPartial w j z + spatialPartial φ j z * spatialPartial w i z + w z * (spatialSecondPartial φ i j z + spatialPartial φ i z * spatialPartial φ j z))

The second spatial derivative under exponential conjugation.