Time translation of strong solutions #

A strong solution on [0, τ] translated in time is a strong solution on [a, a + τ] (prop:lps-local-strong). The weak-derivative and equation clauses transfer by the measure-preserving time translation of the space-time slab.

source

def ESS.LPS.lpsTimeShift (a : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

CKN.Foundation.Parabolic.ParabolicPoint

The time translation (x, s) ↦ (x, s - a) of space-time.

Equations

ESS.LPS.lpsTimeShift a z = (z.1, z.2 - a)

Instances For

source

theorem ESS.LPS.lps_timeShift_measurePreserving (a : ℝ) :

MeasureTheory.MeasurePreserving (lpsTimeShift a) MeasureTheory.volume MeasureTheory.volume

The time translation preserves Lebesgue measure on space-time.

source

theorem ESS.LPS.lps_timeShift_measurableEmbedding (a : ℝ) :

MeasurableEmbedding (lpsTimeShift a)

The time translation is a measurable embedding.

source

theorem ESS.LPS.lps_preimage_Ioo_shift (a τ : ℝ) :

(fun (s : ℝ) => s - a) ⁻¹' Set.Ioo 0 τ = Set.Ioo a (a + τ)

The preimage of a time interval under the time translation.

source

theorem ESS.LPS.lps_memLp_timeShift {E : Type} [NormedAddCommGroup E] (a τ : ℝ) {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))) :

MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f (lpsTimeShift a z)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a (a + τ))))

Square integrability on a slab is preserved by the time translation.

source

def ESS.LPS.lpsTimeTranslate (a : ℝ) :

CKN.Foundation.Parabolic.Vec3 × ℝ ≃ₜ CKN.Foundation.Parabolic.Vec3 × ℝ

The time-translation homeomorphism (x, s) ↦ (x, s + a).

Equations

ESS.LPS.lpsTimeTranslate a = (Homeomorph.refl CKN.Foundation.Parabolic.Vec3).prodCongr (Homeomorph.addRight a)

Instances For

source

theorem ESS.LPS.lps_testFunction_shift {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a τ : ℝ) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → V} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a (a + τ))) :

(fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 + a)) ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 τ)

A translated space-time test function is a test function on the translated slab.

source

theorem ESS.LPS.lps_spatialPartial_timeTranslate (a : ℝ) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g (w.1, w.2 + a)) j z = CKN.spatialPartial g j (z.1, z.2 + a)

Spatial partial derivatives commute with time translation.

source

theorem ESS.LPS.lps_timePartial_timeTranslate (a : ℝ) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g (w.1, w.2 + a)) z = CKN.timePartial g (z.1, z.2 + a)

The time partial derivative commutes with time translation.

source

theorem ESS.LPS.lps_shift_integral (a τ : ℝ) (g G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hG : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), G z = g (lpsTimeShift a z)) :

∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a (a + τ)), G z = ∫ (w : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), g w

Change of variables for the time translation on a slab.

source

theorem ESS.LPS.lps_locallyIntegrableOn_of_memLp {E : Type} [NormedAddCommGroup E] {f : CKN.Foundation.Parabolic.ParabolicPoint → E} {I : Set ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))) :

MeasureTheory.LocallyIntegrableOn f (CKN.spaceTimeSet Set.univ I) MeasureTheory.volume

A field in L² of a slab is locally integrable on it.

source

theorem ESS.LPS.lps_phiShift_spatial (a : ℝ) (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 + a)) j (lpsTimeShift a z) = CKN.spatialPartial φ j z

Spatial derivative of a translated test function.

source

theorem ESS.LPS.lps_phiShift_time (a : ℝ) (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 + a)) (lpsTimeShift a z) = CKN.timePartial φ z

Time derivative of a translated test function.

source

theorem ESS.LPS.lps_phiShift_value (a : ℝ) (φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

(fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ (w.1, w.2 + a)) (lpsTimeShift a z) = φ z

Value of a translated test function.

source

CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo a (a + τ)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u (lpsTimeShift a z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Du (lpsTimeShift a z) i) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => D2u (lpsTimeShift a z) i j) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Dtu (lpsTimeShift a z)

Space-time weak derivatives transfer under time translation.

source

theorem ESS.LPS.lps_isLpsStrongSolution_shift {a τ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (h : IsLpsStrongSolution 0 τ u Du p) :

IsLpsStrongSolution a (a + τ) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u (lpsTimeShift a z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Du (lpsTimeShift a z) i) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => p (lpsTimeShift a z)

A strong solution on [0, τ] translated by a is a strong solution on [a, a + τ] (prop:lps-local-strong).

Documentation

LeanPool.EscauriazaSereginSverak.LPS.LocalStrongShift

Time translation of strong solutions #