Two-scale limits

This file packages the ε → 0 first, truncation order B → ∞ second argument used in paper (3.39).

theorem Anderson4D.tendsto_of_two_scale_approximation {ι : Type u_1} {E : Type u_2} [PseudoMetricSpace E] {l : Filter ι} (f : ι → E) (g : ℕ → ι → E) (zB : ℕ → E) (z : E) (error : ℕ → ℝ) (hg : ∀ (B : ℕ), Filter.Tendsto (g B) l (nhds (zB B))) (hz : Filter.Tendsto zB Filter.atTop (nhds z)) (herror : Filter.Tendsto error Filter.atTop (nhds 0)) (hclose : ∀ (B : ℕ), ∀ᶠ (i : ι) in l, dist (f i) (g B i) ≤ error B) : Filter.Tendsto f l (nhds z)

A family converges if it is uniformly approximated, at every fixed truncation order, by families with known limits; the approximation error and those limits then converge as the truncation order tends to infinity.

No countability or nontriviality assumption on the primary filter is needed.