English
There is a linear map construction between Schwartz spaces parameterized by a bilinear map A, preserving linearity and Schwartz seminorms.
Русский
Существует линейное отображение между пространствами Шварца, задаваемое билинейной картой A, сохраняющее линейность и семинормы Шварца.
LaTeX
$$$mkLM\\; (A, hadd, hsmul, hsmooth, hbound): 𝓢(D,E) → 𝓢(F,G)$ with linearity and growth control.$$
Lean4
/-- Create a continuous semilinear map between Schwartz spaces.
For an example of using this definition, see `fderivCLM`. -/
def mkCLM [RingHomIsometric σ] (A : 𝓢(D, E) → F → G) (hadd : ∀ (f g : 𝓢(D, E)) (x), A (f + g) x = A f x + A g x)
(hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)) (x), A (a • f) x = σ a • A f x) (hsmooth : ∀ f : 𝓢(D, E), ContDiff ℝ ∞ (A f))
(hbound :
∀ n : ℕ × ℕ,
∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
0 ≤ C ∧
∀ (f : 𝓢(D, E)) (x : F),
‖x‖ ^ n.fst * ‖iteratedFDeriv ℝ n.snd (A f) x‖ ≤ C * s.sup (schwartzSeminormFamily 𝕜 D E) f) :
𝓢(D, E) →SL[σ] 𝓢(F, G)
where
cont := by
change Continuous (mkLM A hadd hsmul hsmooth hbound : 𝓢(D, E) →ₛₗ[σ] 𝓢(F, G))
refine Seminorm.continuous_from_bounded (schwartz_withSeminorms 𝕜 D E) (schwartz_withSeminorms 𝕜' F G) _ fun n => ?_
rcases hbound n with ⟨s, C, hC, h⟩
refine ⟨s, ⟨C, hC⟩, fun f => ?_⟩
exact (mkLM A hadd hsmul hsmooth hbound f).seminorm_le_bound 𝕜' n.1 n.2 (by positivity) (h f)
toLinearMap := mkLM A hadd hsmul hsmooth hbound
