English
If ContDiffWithinAt 𝕜 n f s x holds, m < n, and hs : UniqueDiffOn 𝕜 (insert x s), then differentiability of iteratedFDerivWithin 𝕜 m f s at x within s holds.
Русский
Если ContDiffWithinAt 𝕜 n f s x, m < n и hs : UniqueDiffOn 𝕜 (insert x s), то f имеет дифференцируемость внутри s для итеративной производной.
LaTeX
$$$ContDiffWithinAt\\ 𝕜\\ n\\ f\\ s\\ x \\rightarrow m < n \\rightarrow UniqueDiffOn\\ 𝕜\\ (Set.insert\\ x\\ s) \\rightarrow DifferentiableWithinAt\\ 𝕜\\ (iteratedFDerivWithin\\ 𝕜\\ m\\ f\\ s)\\ s\\ x$$$
Lean4
theorem differentiableWithinAt_iteratedFDerivWithin {m : ℕ} (h : ContDiffWithinAt 𝕜 n f s x) (hmn : m < n)
(hs : UniqueDiffOn 𝕜 (insert x s)) : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x :=
by
have : (m + 1 : WithTop ℕ∞) ≠ ∞ := Ne.symm (ne_of_beq_false rfl)
rcases h.contDiffOn' (ENat.add_one_natCast_le_withTop_of_lt hmn) (by simp [this]) with ⟨u, uo, xu, hu⟩
set t := insert x s ∩ u
have A : t =ᶠ[𝓝[≠] x] s :=
by
simp only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter']
rw [← inter_assoc, nhdsWithin_inter_of_mem', ← diff_eq_compl_inter, insert_diff_of_mem, diff_eq_compl_inter]
exacts [rfl, mem_nhdsWithin_of_mem_nhds (uo.mem_nhds xu)]
have B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t :=
iteratedFDerivWithin_eventually_congr_set' _ A.symm _
have C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) t x :=
hu.differentiableOn_iteratedFDerivWithin (Nat.cast_lt.2 m.lt_succ_self) (hs.inter uo) x ⟨mem_insert _ _, xu⟩
rw [differentiableWithinAt_congr_set' _ A] at C
exact C.congr_of_eventuallyEq (B.filter_mono inf_le_left) B.self_of_nhds
