Theorems · Theorem · real analysis

derivWithin.lhopital_zero_nhdsWithin_convex

∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ} {s : Set ℝ},
  Convex ℝ s →
    (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), DifferentiableWithinAt ℝ f (s \ {a}) x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), derivWithin g (s \ {a}) x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a (s \ {a})) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a (s \ {a})) (nhds 0) →
            Filter.Tendsto (fun x => derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) (nhdsWithin a (s \ {a})) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (s \ {a})) l

L'Hôpital's rule for approaching a real from within a convex set, derivWithin version

Defined in

Mathlib.Analysis.Calculus.LHopital

Cited by

1 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound