Infinite extended right derivative is equivalent to ordinary right derivative divergence
ProvedAvramDividend.Classical.derivZeroPlus_top_iff_deriv_tendsto_atTopavram-dividendextended-derivativelimit-equivalenceroot-prerequisitezero-cap
The canonical extended-real right liminf of the ordinary scale derivative equals +∞ if and only if the ordinary derivative tends to +∞ as its argument decreases to zero through positive values. Combines two separately Proved directions, allowing zero-barrier fluctuation arguments to choose whichever representation is convenient.
Preamble
import Theorems.Thm_AvramDividend_Classical_deriv_tendsto_atTop_of_derivZeroPlus_top import Theorems.Thm_AvramDividend_Classical_derivZeroPlus_eq_top_of_right_tendsto_atTop open AvramDividend.Classical Filter Set
Formal statement
theorem AvramDividend.Classical.derivZeroPlus_top_iff_deriv_tendsto_atTop
(W : ℝ → ℝ) :
derivZeroPlus W = ⊤ ↔
Tendsto (fun y : ℝ => deriv W y)
(nhdsWithin (0 : ℝ) (Ioi 0)) atTop := by sorrySource
Canonical Proved forward and reverse derivative-divergence theorems in pinned Mathlib environment.