mkCLMtoNormedSpace — Mathlib

English

Given a bilinear left map B and a temperate growth g, one defines a SchwartzMap bilinearLeftCLM that acts by (f ↦ B(f,g)) pointwise.

Русский

С заданием билинейной левой карты B и темперированного роста g определяется SchwartzMap bilinearLeftCLM, действующий по формуле (f↦B(f,g)).

LaTeX

$$$bilinLeftCLM(B,g) : 𝓢(D,E) → 𝓢(D,G)$ with $(B,g)$-action.$$

Lean4

/-- Define a continuous semilinear map from Schwartz space to a normed space. -/
def mkCLMtoNormedSpace [RingHomIsometric σ] (A : 𝓢(D, E) → G) (hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g)
    (hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = σ a • A f)
    (hbound :
      ∃ (s : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ C * s.sup (schwartzSeminormFamily 𝕜 D E) f) :
    𝓢(D, E) →SL[σ] G :=
  letI f : 𝓢(D, E) →ₛₗ[σ] G :=
    { toFun := (A ·)
      map_add' := hadd
      map_smul' := hsmul }
  { toLinearMap := f
    cont := by
      change Continuous (LinearMap.mk _ _)
      apply Seminorm.cont_withSeminorms_normedSpace G (schwartz_withSeminorms 𝕜 D E)
      rcases hbound with ⟨s, C, hC, h⟩
      exact ⟨s, ⟨C, hC⟩, h⟩ }

Похожие утверждения