English
The natural identification (E × F) × G ≃ E × (F × G) is a smooth isomorphism.
Русский
Естественное биективное отображение (E × F) × G ≃ E × (F × G) гладко отображает пространства на уровне гладкости.
LaTeX
$$$\operatorname{ContDiff}_{\mathbb{K}} n (\mathrm{prodAssoc}\; E\; F\; G)$$$
Lean4
/-- Application of a `ContinuousLinearMap` to a constant commutes with `iteratedFDerivWithin`. -/
theorem iteratedFDerivWithin_clm_apply_const_apply {s : Set E} (hs : UniqueDiffOn 𝕜 s) {c : E → F →L[𝕜] G}
(hc : ContDiffOn 𝕜 n c s) {i : ℕ} (hi : i ≤ n) {x : E} (hx : x ∈ s) {u : F} {m : Fin i → E} :
(iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = (iteratedFDerivWithin 𝕜 i c s x) m u := by
induction i generalizing x with
| zero => simp
| succ i ih =>
replace hi : (i : WithTop ℕ∞) < n := lt_of_lt_of_le (by norm_cast; simp) hi
have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
(hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s := hc.differentiableOn_iteratedFDerivWithin hi hs
simp only [iteratedFDerivWithin_succ_apply_left]
rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]
rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
(differentiableWithinAt_const u)]
rw [fderivWithin_const_apply]
simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]
rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]
