Blowup Pressure Cauchy

Pressure bounds and convergence estimates for the rescaled sequence.

theorem ESS.blowup_pressure_limit_of_near_far {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] (p : ℕ → E) (near far : ℕ → ℕ → E) (hsplit : ∀ (L k : ℕ), p k = near L k + far L k) (hnear : ∀ (L : ℕ), CauchySeq (near L)) (hfar : ∀ (ε : ℝ), 0 < ε → ∃ (L : ℕ), ∀ (k : ℕ), ‖far L k‖ < ε) : ∃ (q : E), Filter.Tendsto p Filter.atTop (nhds q)

Convergent near pressures and uniformly vanishing far pressures give a strong local pressure limit. This is the two-radius argument in prop:blowup-limit.