English
One direction of differentiability implies a differentiable variation within a neighborhood provided a neighborhood for the derivative.
Русский
Одна часть условия дифференцируемости приводит к гладкости вариаций внутри окрестности.
LaTeX
$$$\exists v \in \mathcal{N}[insert x_0 s] x_0 \text{ with appropriate properties }$$$
Lean4
/-- One direction of `contDiffWithinAt_succ_iff_hasFDerivWithinAt`, but where all derivatives are
taken within the same set. Version for partial derivatives / functions with parameters. If `f x` is
a `C^n+1` family of functions and `g x` is a `C^n` family of points, then the derivative of `f x` at
`g x` depends in a `C^n` way on `x`. We give a general version of this fact relative to sets which
may not have unique derivatives, in the following form. If `f : E × F → G` is `C^n+1` at
`(x₀, g(x₀))` in `(s ∪ {x₀}) × t ⊆ E × F` and `g : E → F` is `C^n` at `x₀` within some set `s ⊆ E`,
then there is a function `f' : E → F →L[𝕜] G` that is `C^n` at `x₀` within `s` such that for all `x`
sufficiently close to `x₀` within `s ∪ {x₀}` the function `y ↦ f x y` has derivative `f' x` at `g x`
within `t ⊆ F`. For convenience, we return an explicit set of `x`'s where this holds that is a
subset of `s ∪ {x₀}`. We need one additional condition, namely that `t` is a neighborhood of
`g(x₀)` within `g '' s`. -/
theorem hasFDerivWithinAt_nhds {f : E → F → G} {g : E → F} {t : Set F} (hn : n ≠ ∞) {x₀ : E}
(hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 n g s x₀)
(hgt : t ∈ 𝓝[g '' s] g x₀) :
∃ v ∈ 𝓝[insert x₀ s] x₀,
v ⊆ insert x₀ s ∧
∃ f' : E → F →L[𝕜] G,
(∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 n (fun x => f' x) s x₀ :=
by
have hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀) :=
by
refine nhdsWithin_mono _ ?_ (nhdsWithin_prod self_mem_nhdsWithin hgt)
simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert, true_and,
subset_preimage_image]
obtain ⟨v, hv, hvs, f_an, f', hvf', hf'⟩ := (contDiffWithinAt_succ_iff_hasFDerivWithinAt' hn).mp hf
refine
⟨(fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s, ?_, inter_subset_right, fun z =>
(f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F), ?_, ?_⟩
· refine inter_mem ?_ self_mem_nhdsWithin
have := mem_of_mem_nhdsWithin (mem_insert _ _) hv
refine mem_nhdsWithin_insert.mpr ⟨this, ?_⟩
refine (continuousWithinAt_id.prodMk hg.continuousWithinAt).preimage_mem_nhdsWithin' ?_
rw [← nhdsWithin_le_iff] at hst hv ⊢
exact (hst.trans <| nhdsWithin_mono _ <| subset_insert _ _).trans hv
· intro z hz
have := hvf' (z, g z) hz.1
refine this.comp _ (hasFDerivAt_prodMk_right _ _).hasFDerivWithinAt ?_
exact mapsTo_iff_image_subset.mpr (image_prodMk_subset_prod_right hz.2)
·
exact
(hf'.continuousLinearMap_comp <|
(ContinuousLinearMap.compL 𝕜 F (E × F) G).flip (ContinuousLinearMap.inr 𝕜 E F)).comp_of_mem_nhdsWithin_image
x₀ (contDiffWithinAt_id.prodMk hg) hst
