Breakdown Criterion

theorem EulerBreakdownCriterion.no_escape_near_compact_trajectory {E : Type u_1} [NormedAddCommGroup E] (reference : ℝ → E) (samples : ℕ → E) (times errors : ℕ → ℝ) (S : ℝ) (hc : ContinuousOn reference (Set.Icc 0 S)) (ht : ∀ (n : ℕ), times n ∈ Set.Icc 0 S) (he : Filter.Tendsto errors Filter.atTop (nhds 0)) (hd : ∀ᶠ (n : ℕ) in Filter.atTop, ‖samples n - reference (times n)‖ ≤ errors n) : ¬Filter.Tendsto (fun (n : ℕ) => ‖samples n‖) Filter.atTop Filter.atTop

theorem EulerBreakdownCriterion.no_gradient_escape_under_C1_comparison (u : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (U : ℕ → ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (times errors : ℕ → ℝ) (S : ℝ) (hc : ContinuousOn (fun (t : ℝ) => fderiv ℝ (u t) 0) (Set.Icc 0 S)) (ht : ∀ (n : ℕ), times n ∈ Set.Icc 0 S) (he : Filter.Tendsto errors Filter.atTop (nhds 0)) (hd : ∀ (n : ℕ), ‖fderiv ℝ (U n (times n)) 0 - fderiv ℝ (u (times n)) 0‖ ≤ errors n) : ¬Filter.Tendsto (fun (n : ℕ) => ‖fderiv ℝ (U n (times n)) 0‖) Filter.atTop Filter.atTop

The final gradient contradiction, expressed with actual Fréchet derivatives at the origin.