English
For any Schwartz map f, the function x ↦ ‖x‖^k · ‖f x‖ is integrable with respect to μ when μ has temperate growth.
Русский
Для любой Schwartz‑карты f функция x ↦ ‖x‖^k · ‖f(x)‖ интегрируема по μ при условии темпериатного роста μ.
LaTeX
$$$\text{Integrable}(x \mapsto \|x\|^{k} \cdot \|f(x)\|)\, μ$$$
Lean4
/-- The integral as a continuous linear map from Schwartz space to the codomain. -/
def integralCLM : 𝓢(D, V) →L[𝕜] V :=
by
refine mkCLMtoNormedSpace (∫ x, · x ∂μ) (fun f g ↦ integral_add f.integrable g.integrable) (integral_smul · ·) ?_
rcases hμ.exists_integrable with ⟨n, h⟩
let m := (n, 0)
use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (-(n : ℝ)) ∂μ
refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩
have h' :
∀ x,
‖f x‖ ≤ (1 + ‖x‖) ^ (-(n : ℝ)) * (2 ^ n * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) :=
by
intro x
rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff₀' (by positivity), rpow_natCast]
simpa using one_add_le_sup_seminorm_apply (m := m) (k := n) (n := 0) le_rfl le_rfl f x
apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans
· unfold schwartzSeminormFamily
rw [integral_mul_const, ← mul_assoc, mul_comm (2 ^ n)]
apply h.mul_const
