Weighted bounds and integrability of Schwartz functions #
A Schwartz function is bounded and decays faster than any power. Pointwise, it absorbs any
polynomial weight ⟨c x⟩ ^ m = (1 + ‖c x‖²) ^ (m / 2) and still decays like (1 + ‖x‖) ^ (-k).
Consequently ‖x‖ ^ k ‖f x‖² is
integrable against any measure of temperate growth. This is the integrability input for weighted
L² estimates such as the weighted Plancherel identity. Likewise the pointwise inner product of two
Schwartz functions is integrable, which justifies splitting L² pairings of Schwartz functions.
Main declarations #
SchwartzMap.one_add_norm_smul_sq_rpow_mul_norm_le:⟨c x⟩ ^ m ‖f x‖is bounded by a finite supremum of Schwartz seminorms offtimes(1 + ‖x‖) ^ (-k).SchwartzMap.integrable_norm_pow_mul_norm_sq:‖x‖ ^ k ‖f x‖²is integrable.SchwartzMap.integrable_inner:⟪f x, g x⟫is integrable.SchwartzMap.integrable_one_add_norm_sq_rpow_mul_norm:(1 + ‖x‖ ^ 2) ^ r ‖f x‖is integrable for every realr.SchwartzMap.integrable_one_add_norm_smul_sq_rpow_mul_norm:⟨c x⟩ ^ m ‖f x‖is integrable against any measure of temperate growth.SchwartzMap.integrable_norm_iteratedFDeriv:‖D^k f x‖is integrable.SchwartzMap.integrable_iteratedFDeriv_comp_left,SchwartzMap.integral_norm_iteratedFDeriv_comp_left_le: for a continuous linear mapL, the derivatives ofL ∘ fare integrable, with∫ ‖D^k (L ∘ f)‖ ≤ ‖L‖ ∫ ‖D^k f‖.SchwartzMap.integral_norm_sq_eq_zero_iff: a Schwartz function vanishes exactly when the integral of its squared norm does, for a measure charging every nonempty open set.TauCeti.eq_zero_of_forall_integral_apply_eq_zero: a continuous operator-valued function that integrates to zero against every Schwartz function vanishes.HasCompactSupport.toSchwartzMap_toLp: theLᵖclass of a smooth compactly supported function is the same whether built throughHasCompactSupport.toSchwartzMapor fromMemLp.
A Schwartz function absorbs the polynomial weight ⟨c x⟩ ^ m = (1 + ‖c x‖²) ^ (m / 2) and
still decays like (1 + ‖x‖) ^ (-k), with a constant given by a finite supremum of Schwartz
seminorms.
For a Schwartz function f, the function ‖x‖ ^ k * ‖D^n f x‖ is integrable. Unlike
SchwartzMap.integrable_pow_mul_iteratedFDeriv, this needs no second countability of E: the
function is real-valued and continuous.
For a Schwartz function f, the function ‖x‖ ^ k ‖f x‖² is integrable.
A Schwartz function vanishes if and only if the integral of its squared norm does, against a measure of temperate growth that charges every nonempty open set.
For Schwartz functions f and g with values in a real inner product space, the pointwise
inner product ⟪f x, g x⟫ is integrable.
For a Schwartz function f and every real r, the function (1 + ‖x‖ ^ 2) ^ r ‖f x‖ is
integrable. With r = s / 2 this is the Japanese bracket weight ⟨x⟩ ^ s ‖f x‖.
For a Schwartz function f and real c, m, the function
⟨c x⟩ ^ m ‖f x‖ = (1 + ‖c x‖ ^ 2) ^ (m / 2) ‖f x‖ is integrable.
The norms of the derivatives of a Schwartz function are integrable.
For a Schwartz function f and a continuous linear map L, the derivatives of L ∘ f are
integrable.
For a Schwartz function f and a continuous linear map L,
∫ ‖D^k (L ∘ f)‖ ≤ ‖L‖ ∫ ‖D^k f‖.
A continuous function g : E → V →L[ℂ] W such that ∫ g ζ (f ζ) ∂μ = 0 for every Schwartz
function f, against a locally finite measure charging every nonempty open set, vanishes.
The Lᵖ class of a smooth compactly supported function does not depend on whether it is
built through HasCompactSupport.toSchwartzMap or from any proof of Lᵖ membership.