Limits of weighted extended-real sums #
Weighted sums s a + t b - r with nonnegative real weights and a real correction preserve
limits when both endpoint limits are different from ⊤. This allows convexity inequalities
for extended-real energies to pass to pointwise limits, including endpoint energies ⊥.
theorem
EReal.tendsto_coe_mul_add_coe_mul_sub
{ι : Type u_1}
{l : Filter ι}
{u v : ι → EReal}
{a b : EReal}
(hu : Filter.Tendsto u l (nhds a))
(hv : Filter.Tendsto v l (nhds b))
(ha : a ≠ ⊤)
(hb : b ≠ ⊤)
{s t : ℝ}
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(r : ℝ)
:
Weighted sums with nonnegative real weights and a real subtrahend preserve limits when
both endpoint limits are different from ⊤. Endpoint limits equal to ⊥ are allowed.