Limits of ℝ≥0∞-valued functions #
This file collects squeeze arguments for functions valued in ℝ≥0∞, where the usual
subtraction-based estimates are unavailable.
Main declarations #
TauCeti.tendsto_nhds_zero_of_le_enorm_mul: a quantity dominated by‖h‖ₑtimes a finite constant vanishes ash → 0.
theorem
TauCeti.tendsto_nhds_zero_of_le_enorm_mul
{E : Type u_1}
[TopologicalSpace E]
[ESeminormedAddMonoid E]
{G : E → ENNReal}
{C : ENNReal}
(hC : C ≠ ⊤)
(hG : ∀ (h : E), G h ≤ ‖h‖ₑ * C)
:
Filter.Tendsto G (nhds 0) (nhds 0)
A quantity dominated by ‖h‖ₑ times a finite constant vanishes as h → 0. This is the form
in which a linear modulus of continuity yields the qualitative limit.