Compact Gaussian data after the positive-time translation

The cutoff is translated together with the rescaled field. Its support then lies strictly inside the positive-time cylinder used by the Gaussian weight.

noncomputable def ESS.buGaussianShiftedFinalCutoff (s : ℝ) : ℝ

The terminal cutoff translated from the initial cutoff of the reflected field.

Equations

• ESS.buGaussianShiftedFinalCutoff s = ESS.ucFinalTimeCutoff (s - 1 / 6)

noncomputable def ESS.buGaussianShiftedInitialCutoff (ε s : ℝ) : ℝ

The initial cutoff translated from the terminal cutoff of the reflected field.

Equations

• ESS.buGaussianShiftedInitialCutoff ε s = ESS.ucInitialTimeCutoff ε (s - 1 / 6)

noncomputable def ESS.buGaussianShiftedCutoffField (ρ : ℝ) (hρ : 0 < ρ) (ε : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The Gaussian cutoff field after translation by 1/6.

Equations

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

noncomputable def ESS.buGaussianShiftedCutoffDw (ρ : ℝ) (hρ : 0 < ρ) (ε : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3

The first weak derivative data of the translated cutoff field.

Equations

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

noncomputable def ESS.buGaussianShiftedCutoffD2w (ρ : ℝ) (hρ : 0 < ρ) (ε : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3

The second weak derivative data of the translated cutoff field.

Equations

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

noncomputable def ESS.buGaussianShiftedCutoffDtw (ρ : ℝ) (hρ : 0 < ρ) (ε : ℝ) (v Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The time derivative data of the translated cutoff field.

Equations

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

theorem ESS.buGaussian_shifted_cutoff_admissible {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 (2 - 1 / 6)) v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), ‖buGaussianShiftedField (1 / 6) v z‖ₑ ^ 2 + ‖buGaussianShiftedDw (1 / 6) Dv z‖ₑ ^ 2 + ‖buGaussianShiftedD2w (1 / 6) D2v z‖ₑ ^ 2 + ‖buGaussianShiftedDtw (1 / 6) Dtv z‖ₑ ^ 2 < ⊤) : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo 0 2) (buGaussianShiftedCutoffField ρ hρ ε v) (buGaussianShiftedCutoffDw ρ hρ ε v Dv) (buGaussianShiftedCutoffD2w ρ hρ ε v Dv D2v) (buGaussianShiftedCutoffDtw ρ hρ ε v Dtv) ∧ HasCompactSupport (buGaussianShiftedCutoffField ρ hρ ε v) ∧ tsupport (buGaussianShiftedCutoffField ρ hρ ε v) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2) ∧ MeasureTheory.MemLp (buGaussianShiftedCutoffField ρ hρ ε v) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (buGaussianShiftedCutoffDw ρ hρ ε v Dv) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (buGaussianShiftedCutoffD2w ρ hρ ε v Dv D2v) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (buGaussianShiftedCutoffDtw ρ hρ ε v Dtv) 2 MeasureTheory.volume

A smooth cutoff supported in a compact subset of the source cylinder extends the translated field and its weak derivatives to the Gaussian Carleman cylinder.