English
If a Lipschitz function has differentiable behavior on a countable set of directions, then there exists a common Frechet derivative operator L that explains all those derivatives almost everywhere.
Русский
Если для множества счетных направлений существует линейная производная, то существует общий линейный оператор Фреше, объясняющий все производные почти везде.
LaTeX
$$$\exists L:\, E \to L(E)\quad \text{such that for a.e. } x, \forall v\in s, HasLineDerivAt( f, L v, x, v).$$$
Lean4
theorem ae_exists_fderiv_of_countable (hf : LipschitzWith C f) {s : Set E} (hs : s.Countable) :
∀ᵐ x ∂μ, ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v :=
by
have B := Basis.ofVectorSpace ℝ E
have I1 :
∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v i) • B i) = ∑ i, B.repr v i • lineDeriv ℝ f x (B i) :=
(ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDeriv_sum_eq _ _ _)
have I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v :=
(ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDifferentiableAt v)
filter_upwards [I1, I2] with x hx h'x
let L : StrongDual ℝ E := LinearMap.toContinuousLinearMap (B.constr ℝ (fun i ↦ lineDeriv ℝ f x (B i)))
refine ⟨L, fun v hv ↦ ?_⟩
have J : L v = lineDeriv ℝ f x v := by convert (hx v hv).symm <;> simp [L, B.sum_repr v]
simpa [J] using (h'x v hv).hasLineDerivAt
