Time translation of a strong solution

Translating a space-time field in time by t₀ preserves the slab measure, the space-time test-function class, and the spatial and time partial derivatives of the translated tests (prop:lps-local-strong).

def ESS.LPS.lpsShift (t₀ : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.ParabolicPoint

The translation of the time variable by t₀.

Equations

• ESS.LPS.lpsShift t₀ z = (z.1, t₀ + z.2)

theorem ESS.LPS.lps_shift_measurePreserving (t₀ a b : ℝ) : MeasureTheory.MeasurePreserving (lpsShift t₀) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (t₀ + a) (t₀ + b))))

The time translation carries the slab over (a, b) measure preservingly onto the slab over (t₀ + a, t₀ + b).

theorem ESS.LPS.lps_shift_spatialPartial (t₀ : ℝ) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => g (y.1, y.2 - t₀)) j (lpsShift t₀ z) = CKN.spatialPartial g j z

The spatial partial derivative of a time-translated function.

theorem ESS.LPS.lps_shift_timePartial (t₀ : ℝ) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => g (y.1, y.2 - t₀)) (lpsShift t₀ z) = CKN.timePartial g z

The time partial derivative of a time-translated function.

theorem ESS.LPS.lps_shift_testFunction {a b : ℝ} (t₀ : ℝ) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)) : (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ (y.1, y.2 - t₀)) ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo (t₀ + a) (t₀ + b))

A vector-valued space-time test field, translated in time.

theorem ESS.LPS.lps_shift_measurableEmbedding (t₀ : ℝ) : MeasurableEmbedding (lpsShift t₀)