Exact transfer of relative propagation to physical time and its actual profile.

noncomputable def EulerPacketMovingFrame.scaledTime (t₀ a ε t : ℝ) : ℝ

Scaled time, given by (a/ε)*(t-t₀).

Equations

• EulerPacketMovingFrame.scaledTime t₀ a ε t = a / ε * (t - t₀)

noncomputable def EulerPacketMovingFrame.physicalProfile (Z : ℝ → ℝ) (t₀ a ε t : ℝ) : ℝ

Physical profile, given by Z (scaledTime t₀ a ε t).

Equations

• EulerPacketMovingFrame.physicalProfile Z t₀ a ε t = Z (EulerPacketMovingFrame.scaledTime t₀ a ε t)

theorem EulerPacketMovingFrame.physicalTime_scaledTime {t₀ a ε t : ℝ} (ha : a ≠ 0) (hε : ε ≠ 0) : physicalTime t₀ a ε (scaledTime t₀ a ε t) = t

theorem EulerPacketMovingFrame.scaledTime_physicalTime {t₀ a ε τ : ℝ} (ha : a ≠ 0) (hε : ε ≠ 0) : scaledTime t₀ a ε (physicalTime t₀ a ε τ) = τ

theorem EulerPacketMovingFrame.scaledTime_strictMono {t₀ a ε : ℝ} (ha : 0 < a) (hε : 0 < ε) : StrictMono (scaledTime t₀ a ε)

theorem EulerPacketMovingFrame.scaledTime_mem {t₀ a ε T t : ℝ} (ha : 0 < a) (hε : 0 < ε) (ht : t ∈ Set.Icc t₀ (physicalTime t₀ a ε T)) : scaledTime t₀ a ε t ∈ Set.Icc 0 T

theorem EulerPacketMovingFrame.physicalProfile_continuousOn {Z : ℝ → ℝ} {t₀ a ε T : ℝ} (ha : 0 < a) (hε : 0 < ε) (hZ : ContinuousOn Z (Set.Icc 0 T)) : ContinuousOn (physicalProfile Z t₀ a ε) (Set.Icc t₀ (physicalTime t₀ a ε T))

theorem EulerPacketMovingFrame.physicalProfile_positive {Z : ℝ → ℝ} {t₀ a ε T : ℝ} (ha : 0 < a) (hε : 0 < ε) (hZ : ∀ t ∈ Set.Icc 0 T, 0 < Z t) (t : ℝ) : t ∈ Set.Icc t₀ (physicalTime t₀ a ε T) → 0 < physicalProfile Z t₀ a ε t

theorem EulerPacketMovingFrame.physical_propagation_of_scaled {E : Type u_1} [NormedAddCommGroup E] (w : ℝ → E) (Z : ℝ → ℝ) {t₀ a ε T C : ℝ} (ha : 0 < a) (hε : 0 < ε) (hbound : ∀ (s t : ℝ), 0 ≤ s → s ≤ t → t ≤ T → ‖w (physicalTime t₀ a ε t)‖ ≤ C * (Z t / Z s) * ‖w (physicalTime t₀ a ε s)‖) (s t : ℝ) : s ∈ Set.Icc t₀ (physicalTime t₀ a ε T) → t ∈ Set.Icc t₀ (physicalTime t₀ a ε T) → s ≤ t → ‖w t‖ ≤ C * (physicalProfile Z t₀ a ε t / physicalProfile Z t₀ a ε s) * ‖w s‖

This is only the exact change of the time variable in an already proved propagator estimate; its profile ratio is preserved.