English
Let g be a continuous linear equivalence; then SchwartMap.compCLMOfContinuousLinearEquiv 𝕜 g acts by composition with g on Schwartz(E, F).
Русский
Пусть g — непрерывная линейная эквивалентность; тогда SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g действует посредством композиции с g на Schwartz(E, F).
LaTeX
$$$compCLMOfContinuousLinearEquiv 𝕜 g f = f \circ g$$$
Lean4
/-- The Fréchet derivative on Schwartz space as a continuous `𝕜`-linear map. -/
def fderivCLM : 𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F) :=
mkCLM (fderiv ℝ ·) (fun f g _ => fderiv_add f.differentiableAt g.differentiableAt)
(fun a f _ => fderiv_const_smul f.differentiableAt a) (fun f => (contDiff_succ_iff_fderiv.mp (f.smooth ⊤)).2.2)
fun ⟨k, n⟩ =>
⟨{⟨k, n + 1⟩}, 1, zero_le_one, fun f x => by
simpa only [schwartzSeminormFamily_apply, Seminorm.comp_apply, Finset.sup_singleton, one_smul,
norm_iteratedFDeriv_fderiv, one_mul] using f.le_seminorm 𝕜 k (n + 1) x⟩
