Weak multiplication on the short-time half-space cylinder

Smooth scalar factors obey the spatial, second spatial, and time weak product identities on the cylinder used in lem:bu-small-time.

@[reducible, inline]

abbrev ESS.buShortΩ : Set CKN.Foundation.Parabolic.Vec3

The positive spatial half-space for the short-time backward uniqueness argument.

Equations

• ESS.buShortΩ = {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}

@[reducible, inline]

abbrev ESS.buShortI : Set ℝ

The terminal half of the normalized short time interval.

Equations

• ESS.buShortI = Set.Ioo (1 / 2) 1

def ESS.buCutScalar (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

A smooth scalar factor evaluated in parabolic coordinates.

Equations

• ESS.buCutScalar κ z = κ (CKN.Foundation.Parabolic.parabolicHomeomorph z)

def ESS.buCutField (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The cut-off vector field.

Equations

• ESS.buCutField κ w z = ESS.buCutScalar κ z • w z

noncomputable def ESS.buCutDw (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : Fin 3 → CKN.Foundation.Parabolic.Vec3

First spatial weak derivative data for the cut-off field.

Equations

• ESS.buCutDw κ w Dw z i j = ESS.buCutScalar κ z * Dw z i j + w z i * CKN.spatialPartial (ESS.buCutScalar κ) j z

noncomputable def ESS.buCutD2 (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3

Second spatial weak derivative data for the cut-off field.

Equations

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

noncomputable def ESS.buCutDt (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (w Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.Vec3

Weak time derivative data for the cut-off field.

Equations

• ESS.buCutDt κ w Dtw z i = ESS.buCutScalar κ z * Dtw z i + w z i * CKN.timePartial (ESS.buCutScalar κ) z

theorem ESS.buCut_hasSpaceTimeWeakDerivs (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hξ : ContDiff ℝ (↑⊤) κ) {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hw : CKN.HasSpaceTimeWeakDerivs buShortΩ buShortI w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs buShortΩ buShortI (buCutField κ w) (buCutDw κ w Dw) (buCutD2 κ w Dw D2w) (buCutDt κ w Dtw)

Smooth scalar multiplication preserves weak spatial and time derivatives on the shifted half-space cylinder.