English
The evaluation of bilinLeftCLM on f reduces to the pointwise application B(f(x),g(x)).
Русский
Оценка bilinLeftCLM на f сводится к точечному применению B(f(x),g(x)).
LaTeX
$$$bilinLeftCLM\\; B\\; hg\\; f = (x \\mapsto B(f(x),g(x))).$$$
Lean4
/-- The map applying a vector to Hom-valued Schwartz function as a continuous linear map. -/
protected def evalCLM (m : E) : 𝓢(E, E →L[ℝ] F) →L[𝕜] 𝓢(E, F) :=
mkCLM (fun f x => f x m) (fun _ _ _ => rfl) (fun _ _ _ => rfl) (fun f => ContDiff.clm_apply f.2 contDiff_const) <|
by
rintro ⟨k, n⟩
use {(k, n)}, ‖m‖, norm_nonneg _
intro f x
simp only [Finset.sup_singleton, schwartzSeminormFamily_apply]
calc
‖x‖ ^ k * ‖iteratedFDeriv ℝ n (f · m) x‖ ≤ ‖x‖ ^ k * (‖m‖ * ‖iteratedFDeriv ℝ n f x‖) :=
by
gcongr
exact norm_iteratedFDeriv_clm_apply_const (f.smooth _).contDiffAt le_rfl
_ ≤ ‖m‖ * SchwartzMap.seminorm 𝕜 k n f := by
move_mul [‖m‖]
gcongr
apply le_seminorm
