OAI/GroupTheory/PolycyclicRecognition/Geometry/SegmentVolumeDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.SupportDatum.le_segmentSupport_derivative line 23

   Source documentation

   Differentiability controls the whole short one-sided segment, so the segment-volume lower bound passes to its derivative without any extra Hausdorff-convergence hypothesis.

   theorem le_segmentSupport_derivative
       (f : ℝ → W) (hf : Continuous f) (w : W) (hderiv : HasDerivAt f w 0)
       (p : ℝ) {T₀ : ℝ} (hT₀ : 0 < T₀)
       (hvolume : ∀ T : ℝ, 0 < T → T < T₀ → T * p ≤ D.templateSupport (f '' Icc 0 T)) :
       p ≤ D.segmentSupport w := by
   …