English
The derivative within domains preserves ContDiff on product spaces.
Русский
Производная внутри доменов сохраняет ContDiff на произведениях пространств.
LaTeX
$$$ContDiffOn\ 𝕜\ n f\ s \to ContDiffOn\ 𝕜\ n (derivWithin\ 𝕜\ f\ s)\ s$$$
Lean4
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` within a set in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear. This lemma is an auxiliary version
assuming all spaces live in the same universe, to enable an induction. Use instead
`ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear` that removes this assumption. -/
theorem norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu Fu Gu : Type u} [NormedAddCommGroup Du] [NormedSpace 𝕜 Du]
[NormedAddCommGroup Eu] [NormedSpace 𝕜 Eu] [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu]
[NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} {n : ℕ} {s : Set Du} {x : Du}
(hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
‖iteratedFDerivWithin 𝕜 n (fun y => B (f y) (g y)) s x‖ ≤
‖B‖ *
∑ i ∈ Finset.range (n + 1),
(n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
by
/- We argue by induction on `n`. The bound is trivial for `n = 0`. For `n + 1`, we write
the `(n+1)`-th derivative as the `n`-th derivative of the derivative `B f g' + B f' g`,
and apply the inductive assumption to each of those two terms. For this induction to make sense,
the spaces of linear maps that appear in the induction should be in the same universe as the
original spaces, which explains why we assume in the lemma that all spaces live in the same
universe. -/
induction n generalizing Eu Fu Gu with
|
zero =>
simp only [norm_iteratedFDerivWithin_zero, zero_add, Finset.range_one, Finset.sum_singleton, Nat.choose_self,
Nat.cast_one, one_mul, Nat.sub_zero, ← mul_assoc]
apply B.le_opNorm₂
| succ n IH =>
have In : (n : WithTop ℕ∞) + 1 ≤ n.succ := by simp only [Nat.cast_succ, le_refl]
have I1 :
‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompR Du (f y) (fderivWithin 𝕜 g s y)) s x‖ ≤
‖B‖ *
∑ i ∈ Finset.range (n + 1),
n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖ :=
by
calc
‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompR Du (f y) (fderivWithin 𝕜 g s y)) s x‖ ≤
‖B.precompR Du‖ *
∑ i ∈ Finset.range (n + 1),
n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
IH _ (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)
_ ≤
‖B‖ *
∑ i ∈ Finset.range (n + 1),
n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
by gcongr; exact B.norm_precompR_le Du
_ = _ := by
congr 1
apply Finset.sum_congr rfl fun i hi => ?_
rw [Nat.succ_sub (Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)), ← norm_iteratedFDerivWithin_fderivWithin hs hx]
have I2 :
‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s x‖ ≤
‖B‖ *
∑ i ∈ Finset.range (n + 1),
n.choose i * ‖iteratedFDerivWithin 𝕜 (i + 1) f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
calc
‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s x‖ ≤
‖B.precompL Du‖ *
∑ i ∈ Finset.range (n + 1),
n.choose i * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ *
‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
IH _ (hf.fderivWithin hs In) (hg.of_le (Nat.cast_le.2 (Nat.le_succ n)))
_ ≤
‖B‖ *
∑ i ∈ Finset.range (n + 1),
n.choose i * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ *
‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
by gcongr; exact B.norm_precompL_le Du
_ = _ := by
congr 1
apply Finset.sum_congr rfl fun i _ => ?_
rw [← norm_iteratedFDerivWithin_fderivWithin hs hx]
have J :
iteratedFDerivWithin 𝕜 n (fun y : Du => fderivWithin 𝕜 (fun y : Du => B (f y) (g y)) s y) s x =
iteratedFDerivWithin 𝕜 n
(fun y => B.precompR Du (f y) (fderivWithin 𝕜 g s y) + B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s x :=
by
apply iteratedFDerivWithin_congr (fun y hy => ?_) hx
have L : (1 : WithTop ℕ∞) ≤ n.succ := by simpa only [ENat.coe_one, Nat.one_le_cast] using Nat.succ_pos n
exact B.fderivWithin_of_bilinear (hf.differentiableOn L y hy) (hg.differentiableOn L y hy) (hs y hy)
rw [← norm_iteratedFDerivWithin_fderivWithin hs hx, J]
have A : ContDiffOn 𝕜 n (fun y => B.precompR Du (f y) (fderivWithin 𝕜 g s y)) s :=
(B.precompR Du).isBoundedBilinearMap.contDiff.comp₂_contDiffOn (hf.of_le (Nat.cast_le.2 (Nat.le_succ n)))
(hg.fderivWithin hs In)
have A' : ContDiffOn 𝕜 n (fun y => B.precompL Du (fderivWithin 𝕜 f s y) (g y)) s :=
(B.precompL Du).isBoundedBilinearMap.contDiff.comp₂_contDiffOn (hf.fderivWithin hs In)
(hg.of_le (Nat.cast_le.2 (Nat.le_succ n)))
rw [iteratedFDerivWithin_add_apply' (A.contDiffWithinAt hx) (A'.contDiffWithinAt hx) hs hx]
apply (norm_add_le _ _).trans ((add_le_add I1 I2).trans (le_of_eq ?_))
simp_rw [← mul_add, mul_assoc]
congr 1
exact
(Finset.sum_choose_succ_mul (fun i j => ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 j g s x‖)
n).symm
