English
Under suitable conditions, there exists a neighborhood where HasFDerivWithinAt holds for the family f.
Русский
При подходящих условиях существует окрестность, где выполняется HasFDerivWithinAt для семейства f.
LaTeX
$$$\exists v \in \mathcal{N}[insert x_0 s] x_0,\; v \subset insert x_0 s \land\; \exists f' : E → F →L[\mathbb{K}] G,\; (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x))$$$
Lean4
/-- The most general lemma stating that `x ↦ fderivWithin 𝕜 (f x) t (g x)` is `C^n`
at a point within a set.
To show that `x ↦ D_yf(x,y)g(x)` (taken within `t`) is `C^m` at `x₀` within `s`, we require that
* `f` is `C^n` at `(x₀, g(x₀))` within `(s ∪ {x₀}) × t` for `n ≥ m+1`.
* `g` is `C^m` at `x₀` within `s`;
* Derivatives are unique at `g(x)` within `t` for `x` sufficiently close to `x₀` within `s ∪ {x₀}`;
* `t` is a neighborhood of `g(x₀)` within `g '' s`; -/
theorem fderivWithin'' {f : E → F → G} {g : E → F} {t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g s x₀)
(ht : ∀ᶠ x in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)) (hmn : m + 1 ≤ n) (hgt : t ∈ 𝓝[g '' s] g x₀) :
ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀ :=
by
have : ∀ k : ℕ, k ≤ m → ContDiffWithinAt 𝕜 k (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀ :=
by
intro k hkm
obtain ⟨v, hv, -, f', hvf', hf'⟩ :=
(hf.of_le <| (add_le_add_right hkm 1).trans hmn).hasFDerivWithinAt_nhds (by simp) (hg.of_le hkm) hgt
refine hf'.congr_of_eventuallyEq_insert ?_
filter_upwards [hv, ht]
exact fun y hy h2y => (hvf' y hy).fderivWithin h2y
match m with
| ω =>
obtain rfl : n = ω := by simpa using hmn
obtain ⟨v, hv, -, f', hvf', hf'⟩ := hf.hasFDerivWithinAt_nhds (by simp) hg hgt
refine hf'.congr_of_eventuallyEq_insert ?_
filter_upwards [hv, ht]
exact fun y hy h2y => (hvf' y hy).fderivWithin h2y
| ∞ =>
rw [contDiffWithinAt_infty]
exact fun k ↦ this k (by exact_mod_cast le_top)
| (m : ℕ) => exact this _ le_rfl
