Time translation between slabs

For h : ℝ the translation (x, t) ↦ (x, t + h) maps the slab over (c, d) onto the slab over (c + h, d + h) and preserves Lebesgue measure. A space-time weak derivative identity on a slab over (a, b) therefore passes to the translated fields on every slab over (c, d) with a ≤ c + h and d + h ≤ b. These are the time-translation steps of the difference-quotient argument in prop:lps-smoothing.

theorem ESS.LPS.lps_forwardShift_measurePreserving (h : ℝ) : MeasureTheory.MeasurePreserving (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (z.1, z.2 + h)) MeasureTheory.volume MeasureTheory.volume

The forward time translation (x, t) ↦ (x, t + h) preserves Lebesgue measure.

theorem ESS.LPS.lps_forwardShift_measurableEmbedding (h : ℝ) : MeasurableEmbedding fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (z.1, z.2 + h)

The forward time translation is a measurable embedding.

theorem ESS.LPS.lps_forwardShift_preimage_slab (c d h : ℝ) : (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (z.1, z.2 + h)) ⁻¹' CKN.spaceTimeSet Set.univ (Set.Ioo (c + h) (d + h)) = CKN.spaceTimeSet Set.univ (Set.Ioo c d)

The preimage of a translated slab under the forward time translation.

theorem ESS.LPS.lps_slab_subset {a b c d : ℝ} (hac : a ≤ c) (hdb : d ≤ b) : CKN.spaceTimeSet Set.univ (Set.Ioo c d) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo a b)

A slab over a subinterval is contained in the slab over the interval.

theorem ESS.LPS.lps_measurableSet_slab (a b : ℝ) : MeasurableSet (CKN.spaceTimeSet Set.univ (Set.Ioo a b))

The slab over an open interval is measurable.

theorem ESS.LPS.lps_setIntegral_forwardShift (c d h : ℝ) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo c d), g (z.1, z.2 + h) = ∫ (w : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo (c + h) (d + h)), g w

Change of variables for the forward time translation between slabs.

theorem ESS.LPS.lps_memLp_forwardShift {E : Type} [NormedAddCommGroup E] {p : ENNReal} {a b c d h : ℝ} (hac : a ≤ c + h) (hdb : d + h ≤ b) {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f (z.1, z.2 + h)) p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))

Integrability of a field on a slab passes to the translated field on every slab whose translate lies inside.

theorem ESS.LPS.lps_memLp_slab_mono {E : Type} [NormedAddCommGroup E] {p : ENNReal} {a b c d : ℝ} (hac : a ≤ c) (hdb : d ≤ b) {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))

Integrability on a slab passes to every slab over a subinterval.

theorem ESS.LPS.lps_ae_forwardShift {a b c d h : ℝ} (hac : a ≤ c + h) (hdb : d + h ≤ b) {P : CKN.Foundation.Parabolic.ParabolicPoint → Prop} (hP : ∀ᵐ (w : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)), P w) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)), P (z.1, z.2 + h)

An almost-everywhere property on a slab passes to the translated points of every slab whose translate lies inside.

theorem ESS.LPS.lps_ae_slab_mono {a b c d : ℝ} (hac : a ≤ c) (hdb : d ≤ b) {P : CKN.Foundation.Parabolic.ParabolicPoint → Prop} (hP : ∀ᵐ (w : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)), P w) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)), P z

An almost-everywhere property on a slab holds on every slab over a subinterval.

theorem ESS.LPS.lps_testFunction_backShift {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {c d : ℝ} (h : ℝ) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → V} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo c d)) : (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 - h)) ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo (c + h) (d + h))

A test function on the slab over (c, d), translated backward by h, is a test function on the slab over (c + h, d + h).

theorem ESS.LPS.lps_testFunction_slab_mono {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b c d : ℝ} (hac : a ≤ c) (hdb : d ≤ b) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → V} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo c d)) : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)

A test function on a slab is a test function on every larger slab.

theorem ESS.LPS.lps_setIntegral_slab_eq_of_vanish {a b c d : ℝ} (hac : a ≤ c) (hdb : d ≤ b) {K : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hK : ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo c d), K z = 0) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), K z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo c d), K z

The integral over a slab of a function vanishing outside a smaller slab is its integral over the smaller slab.

theorem ESS.LPS.lps_test_vanish {c d : ℝ} {φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo c d)) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo c d)) : φ z = 0 ∧ (∀ (j : Fin 3), CKN.spatialPartial φ j z = 0) ∧ CKN.timePartial φ z = 0

Values and first derivatives of a scalar test vanish outside its slab.

theorem ESS.LPS.lps_backShift_spatialPartial (h : ℝ) (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 - h)) j (z.1, z.2 + h) = CKN.spatialPartial φ j z

Spatial derivatives of a backward-translated test, at a forward-translated point.

theorem ESS.LPS.lps_backShift_timePartial (h : ℝ) (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 - h)) (z.1, z.2 + h) = CKN.timePartial φ z

Time derivative of a backward-translated test, at a forward-translated point.

theorem ESS.LPS.lps_backShift_value {V : Type} (h : ℝ) (φ : CKN.Foundation.Parabolic.ParabolicPoint → V) (z : CKN.Foundation.Parabolic.ParabolicPoint) : (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 - h)) (z.1, z.2 + h) = φ z

Value of a backward-translated test at a forward-translated point.

theorem ESS.LPS.lps_setIntegral_slab_forwardShift {a b c d h : ℝ} (hac : a ≤ c + h) (hdb : d + h ≤ b) (K : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hK : ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo (c + h) (d + h)), K z = 0) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), K z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo c d), K (z.1, z.2 + h)

The integral over a slab of a function vanishing outside a translated subslab, written as an integral over the untranslated subslab.

theorem ESS.LPS.lps_hasSpaceTimeWeakDerivs_forwardShift {a b c d h : ℝ} (hac : a ≤ c + h) (hdb : d + h ≤ b) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hw : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo a b) u Du D2u Dtu) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo c d) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u (z.1, z.2 + h)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Du (z.1, z.2 + h)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => D2u (z.1, z.2 + h)) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Dtu (z.1, z.2 + h)

Space-time weak derivatives on a slab pass to the time-translated fields on every slab whose translate lies inside (prop:lps-smoothing).

theorem ESS.LPS.lps_weakEquation_forwardShift {a b c d h : ℝ} (hac : a ≤ c + h) (hdb : d + h ≤ b) {A : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {F : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → ℝ} {G : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (heq : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), ∑ i : Fin 3, A z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, F z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, G z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - q z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo c d) → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo c d), ∑ i : Fin 3, A (z.1, z.2 + h) i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, F (z.1, z.2 + h) i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, G (z.1, z.2 + h) i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - q (z.1, z.2 + h) * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The weak momentum equation with a time-derivative field, on a slab, passes to the time-translated fields on every slab whose translate lies inside (prop:lps-smoothing).

theorem ESS.LPS.lps_hasSpaceTimeWeakDerivs_slab_mono {a b c d : ℝ} (hac : a ≤ c) (hdb : d ≤ b) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hw : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo a b) u Du D2u Dtu) : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo c d) u Du D2u Dtu

Space-time weak derivatives on a slab restrict to every slab over a subinterval.

theorem ESS.LPS.lps_weakEquation_slab_mono {a b c d : ℝ} (hac : a ≤ c) (hdb : d ≤ b) {A : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {F : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → ℝ} {G : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (heq : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), ∑ i : Fin 3, A z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, F z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, G z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - q z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo c d) → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo c d), ∑ i : Fin 3, A z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, F z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, G z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - q z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

The weak momentum equation with a time-derivative field, on a slab, restricts to every slab over a subinterval.