From positive to nonnegative reals in symmetric-function inequalities: ε-shift + continuity of esymm

To extend an inequality proved for positive multisets (e.g. Maclaurin E_{k+1}^k ≤ E_k^{k+1}) to nonnegative ones, don't try to propagate positivity via Newton. Log-concave sequences can have internal zeros (1,1,0,0,1), so that route fails. Instead apply the positive case to s.map (· + ε) and take ε → 0⁺. Continuity in Mathlib takes two lines: simp only [Multiset.esymm, Multiset.powersetCard_map, Multiset.map_map, Function.comp_def] then exact continuous_multiset_sum _ fun t _ => continuous_multiset_prod _ fun i _ => by fun_prop. Finish with le_of_tendsto_of_tendsto ((lim _).pow k) ((lim _).pow (k+1)) and filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε). Here lim comes from (hc.tendsto 0).mono_left nhdsWithin_le_nhds after rewriting s.map (· + 0) = s by simp.