English
Composition with a right-hand continuous linear equivalence acts as a continuous linear map on Schwartz space, given by compCLMOfContinuousLinearEquiv 𝕜 g = compCLMOfAntilipschitz 𝕜 (g.toContinuousLinearMap.hasTemperateGrowth) g.antilipschitz.
Русский
Композиция справа по непрерывной линейной эквивалентности задаёт непрерывно линейное отображение на пространстве Шварца: compCLMOfContinuousLinearEquiv 𝕜 g = compCLMOfAntilipschitz 𝕜 (g.toContinuousLinearMap.hasTemperateGrowth) g.antilipschitz.
LaTeX
$$$compCLMOfContinuousLinearEquiv 𝕜 g = compCLMOfAntilipschitz 𝕜 (g.toContinuousLinearMap.hasTemperateGrowth) g.antilipschitz$$$
Lean4
/-- Composition with a continuous linear equiv on the right is a continuous linear map on
Schwartz space. -/
def compCLMOfContinuousLinearEquiv (g : D ≃L[ℝ] E) : 𝓢(E, F) →L[𝕜] 𝓢(D, F) :=
compCLMOfAntilipschitz 𝕜 (g.toContinuousLinearMap.hasTemperateGrowth) g.antilipschitz
