Lower bounds that saturate a limit of the sum are limits

Let f i be a finite family of functions into a linearly ordered field. If every f i is eventually above each value below c i, so that c i is a lower bound for its lower limit, and the sum ∑ i, f i is eventually below each value above ∑ i, c i, then every f i tends to c i: the lower bounds of the other members leave room for no more than c i in the sum.

The two hypotheses are the two halves of tendsto_order, the lower half for each member and the upper half for the sum. No boundedness is assumed, so the statement avoids the side conditions of Filter.liminf and Filter.limsup.

This is how a one-sided estimate becomes an asymptotic: an argument that exhibits enough mass in each member of a finite partition, and cannot see that there is no more, still determines every member once the total is known.

The analogous Dirichlet-density squeeze is NumberField.Set.hasDirichletDensity_of_squeeze.

Main results

• TauCeti.tendsto_of_forall_eventually_lt_of_eventually_sum_lt: lower bounds on the members of a finite family whose sum is bounded above by the sum of the bounds are limits.

theorem TauCeti.tendsto_of_forall_eventually_lt_of_eventually_sum_lt {ι : Type u_1} {α : Type u_2} {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {s : Finset ι} {f : ι → α → 𝕜} {c : ι → 𝕜} (hlow : ∀ i ∈ s, ∀ b < c i, ∀ᶠ (x : α) in l, b < f i x) (hsum : ∀ b > ∑ i ∈ s, c i, ∀ᶠ (x : α) in l, ∑ i ∈ s, f i x < b) {i₀ : ι} (hi₀ : i₀ ∈ s) : Filter.Tendsto (f i₀) l (nhds (c i₀))

Lower bounds that saturate the sum are limits. Let f i, for i ∈ s, be functions into a linearly ordered field with the order topology. If for every i ∈ s each value below c i is eventually exceeded by f i, and each value above ∑ i ∈ s, c i eventually exceeds ∑ i ∈ s, f i, then f i₀ tends to c i₀ for every i₀ ∈ s.

The hypotheses are the lower half of tendsto_order for each member and the upper half for the sum; the upper half for a member is manufactured from the other members' lower bounds.