SegmentIncrementDerivative.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Closed increment constraints pass to one-sided derivatives

theorem OAI.PolycyclicRecognition.derivative_mem_of_short_increments line 14

Source documentation

Only positive short segments are needed to constrain the derivative. The derivative limit itself supplies all required convergence.

theorem derivative_mem_of_short_increments
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (f : ℝ → W) (w : W) (hderiv : HasDerivAt f w 0)
    (S : Set W) (hS : IsClosed S) {T₀ : ℝ} (hT₀ : 0 < T₀)
    (hinc : ∀ t : ℝ, 0 < t → t < T₀ → t⁻¹ • (f t - f 0) ∈ S) : w ∈ S := by
…