Theorems · Theorem · real analysis

LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {C : NNReal} [FiniteDimensional ℝ E] {f : E → F},
  LipschitzWith C f →
    ∀ {s : Set E},
      Metric.sphere 0 1 ⊆ closure s →
        ∀ {L : E →L[ℝ] F} {x : E}, (∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v) → HasFDerivAt f L x

If a Lipschitz functions has line derivatives in a dense set of directions, all of them given by a single continuous linear map L, then it admits L as Fréchet derivative.

Defined in

Mathlib.Analysis.Calculus.Rademacher

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceFiniteDimensional