English
One can partition the domain into countably many disjoint measurable pieces on each of which f is well approximated by some linear map A_n with a uniform radius; these pieces cover the domain.
Русский
Можно разбить область на счетное число парно-дискретных непересекающихся измеримых частей, на каждой из которых f хорошо приближается к некоторой линейной карте A_n при фиксированном радиусе; части покрывают область.
LaTeX
$$$$ \exists (t_n)_{n\in\mathbb{N}}, (A_n)_{n\in\mathbb{N}}:\quad \text{PairwiseDisjoint on } t_n \land \forall n, \text{Measurable}(t_n) \land s \subseteq \bigcup_n t_n \land \forall n, ApproximatesLinearOn(f,A_n,s\cap t_n,\delta_n). $$$$
Lean4
/-- Assume that a function `f` has a derivative at every point of a set `s`. Then one may
partition `s` into countably many disjoint relatively measurable sets (i.e., intersections
of `s` with measurable sets `t n`) on which `f` is well approximated by linear maps `A n`. -/
theorem exists_partition_approximatesLinearOn_of_hasFDerivWithinAt [SecondCountableTopology F] (f : E → F) (s : Set E)
(f' : E → E →L[ℝ] F) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (r : (E →L[ℝ] F) → ℝ≥0) (rpos : ∀ A, r A ≠ 0) :
∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
Pairwise (Disjoint on t) ∧
(∀ n, MeasurableSet (t n)) ∧
(s ⊆ ⋃ n, t n) ∧
(∀ n, ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
by
rcases exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' r rpos with
⟨t, A, t_closed, st, t_approx, ht⟩
refine
⟨disjointed t, A, disjoint_disjointed _, MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩
· rw [iUnion_disjointed]; exact st
· intro n; exact (t_approx n).mono_set (inter_subset_inter_right _ (disjointed_subset _ _))
