Blowup Pressure Two Radius #
Pressure bounds and convergence estimates for the rescaled sequence.
theorem
ESS.blowup_pressure_two_radius_convergence
{E : Type u_1}
[NormedAddCommGroup E]
(p : ℕ → E)
(q : E)
(near : ℕ → ℕ → E)
(nearLimit : ℕ → E)
(far : ℕ → ℕ → E)
(farLimit : ℕ → E)
(hsplit : ∀ (L k : ℕ), p k = near L k + far L k)
(hlimitSplit : ∀ (L : ℕ), q = nearLimit L + farLimit L)
(hnear : ∀ (L : ℕ), Filter.Tendsto (near L) Filter.atTop (nhds (nearLimit L)))
(hfar : ∀ (ε : ℝ), 0 < ε → ∃ (L : ℕ), (∀ (k : ℕ), ‖far L k‖ < ε) ∧ ‖farLimit L‖ < ε)
:
Filter.Tendsto p Filter.atTop (nhds q)
Convergent near pressures and uniformly small far pressures identify the limit of the full pressure through the two-radius argument.