H³ stability on varying initial horizons. The comparison constant uses only the original reference Euler solution and its full horizon.
theorem
EulerOrdinarySobolev.Evolution.restricted_exponential_le
{T : ℝ}
{hT : 0 ≤ T}
(U : Evolution T hT)
(durations : ℕ → ℝ)
(hDT : ∀ (n : ℕ), durations n ≤ T)
(n : ℕ)
:
Real.exp (3 * stabilityConstant U.referenceSize * durations n) ≤ Real.exp (3 * stabilityConstant U.referenceSize * T)
theorem
EulerOrdinarySobolev.Evolution.eventually_h3_bound_varying
{T : ℝ}
{hT : 0 ≤ T}
(U : Evolution T hT)
(durations : ℕ → ℝ)
(hD : ∀ (n : ℕ), 0 ≤ durations n)
(hDT : ∀ (n : ℕ), durations n ≤ T)
(V : (n : ℕ) → Evolution (durations n) ⋯)
(ε : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hlim : Filter.Tendsto ε Filter.atTop (nhds 0))
(hinit : ∀ (n : ℕ), tensorNorm 3 (((fun (n : ℕ) => U.restrictTime (durations n) ⋯ ⋯) n).difference (V n) ⟨0, ⋯⟩) ≤ ε n)
:
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : ↑(Set.Icc 0 (durations n))),
tensorNorm 3 (((fun (n : ℕ) => U.restrictTime (durations n) ⋯ ⋯) n).difference (V n) t) ≤ 640 * ε n * Real.exp (3 * stabilityConstant U.referenceSize * T)
theorem
EulerOrdinarySobolev.Evolution.sampled_h3_tendsto_zero_varying
{T : ℝ}
{hT : 0 ≤ T}
(U : Evolution T hT)
(durations : ℕ → ℝ)
(hD : ∀ (n : ℕ), 0 ≤ durations n)
(hDT : ∀ (n : ℕ), durations n ≤ T)
(V : (n : ℕ) → Evolution (durations n) ⋯)
(ε : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hlim : Filter.Tendsto ε Filter.atTop (nhds 0))
(hinit : ∀ (n : ℕ), tensorNorm 3 (((fun (n : ℕ) => U.restrictTime (durations n) ⋯ ⋯) n).difference (V n) ⟨0, ⋯⟩) ≤ ε n)
(times : (n : ℕ) → ↑(Set.Icc 0 (durations n)))
:
Filter.Tendsto
(fun (n : ℕ) => tensorNorm 3 (((fun (n : ℕ) => U.restrictTime (durations n) ⋯ ⋯) n).difference (V n) (times n)))
Filter.atTop (nhds 0)
theorem
EulerOrdinarySobolev.Evolution.no_gradient_escape_varying
{T : ℝ}
{hT : 0 ≤ T}
(U : Evolution T hT)
(durations : ℕ → ℝ)
(hD : ∀ (n : ℕ), 0 ≤ durations n)
(hDT : ∀ (n : ℕ), durations n ≤ T)
(V : (n : ℕ) → Evolution (durations n) ⋯)
(ε : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hlim : Filter.Tendsto ε Filter.atTop (nhds 0))
(hinit : ∀ (n : ℕ), tensorNorm 3 (((fun (n : ℕ) => U.restrictTime (durations n) ⋯ ⋯) n).difference (V n) ⟨0, ⋯⟩) ≤ ε n)
(times : (n : ℕ) → ↑(Set.Icc 0 (durations n)))
:
¬Filter.Tendsto (fun (n : ℕ) => ‖fderiv ℝ ((V n).velocity (times n)).field 0‖) Filter.atTop Filter.atTop
theorem
EulerOrdinarySobolev.Evolution.no_gradient_escape_of_initial_tendsto_varying
{T : ℝ}
{hT : 0 ≤ T}
(U : Evolution T hT)
(durations : ℕ → ℝ)
(hD : ∀ (n : ℕ), 0 ≤ durations n)
(hDT : ∀ (n : ℕ), durations n ≤ T)
(V : (n : ℕ) → Evolution (durations n) ⋯)
(hinit :
Filter.Tendsto
(fun (n : ℕ) => tensorNorm 3 (((fun (n : ℕ) => U.restrictTime (durations n) ⋯ ⋯) n).difference (V n) ⟨0, ⋯⟩))
Filter.atTop (nhds 0))
(times : (n : ℕ) → ↑(Set.Icc 0 (durations n)))
:
¬Filter.Tendsto (fun (n : ℕ) => ‖fderiv ℝ ((V n).velocity (times n)).field 0‖) Filter.atTop Filter.atTop