Physlib.SpaceAndTime.Space.IsDistBounded
64 declarations
is distribution-bounded
#IsDistBoundedLet be a function from a -dimensional Euclidean space to a normed space . The predicate `IsDistBounded f` holds if is almost everywhere strongly measurable with respect to the volume measure and there exists a finite natural number such that the norm of is bounded by a sum of the form: \[ \|f(x)\| \le \sum_{i=1}^n c_i \|x + g_i\|^{p_i} \] where for each , the coefficient is a non-negative real number (), is a vector in , and the exponent is an integer satisfying .
implies is almost everywhere strongly measurable
#aestronglyMeasurableLet be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (satisfies ), then is almost everywhere strongly measurable with respect to the volume measure on .
If is distribution-bounded, then is almost everywhere strongly measurable
#aeStronglyMeasurable_schwartzMap_smulLet be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (satisfies `IsDistBounded f`), then for any Schwartz map , the function mapping to the scalar product is almost everywhere strongly measurable with respect to the volume measure.
AE Strong Measurability of for Distribution-Bounded
#aeStronglyMeasurable_fderiv_schwartzMap_smulLet be a natural number and be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (satisfies `IsDistBounded f`), then for any Schwartz map and any vector , the function is almost everywhere strongly measurable with respect to the volume measure, where denotes the Fréchet derivative of at evaluated in the direction .
If is distribution-bounded, then is almost everywhere strongly measurable
#aeStronglyMeasurable_inv_powLet and be natural numbers. Let be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (meaning it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form ), then the function is almost everywhere strongly measurable with respect to the volume measure on .
A distribution-bounded function scaled by a space-time Schwartz map is AE strongly measurable
#aeStronglyMeasurable_time_schwartzMap_smulLet be a natural number and be a distribution-bounded function mapping into a normed space . For any Schwartz map , the function is almost everywhere strongly measurable with respect to the volume measure on .
Distribution-bounded functions are integrable against Schwartz maps
#integrable_spaceLet be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (satisfies `IsDistBounded f`), then for any Schwartz map , the function is integrable on with respect to the volume measure.
The product of a distribution-bounded function and a Schwartz map is integrable
#integrable_space_mulLet be a real-valued function on a -dimensional Euclidean space. If is distribution-bounded (satisfies `IsDistBounded f`), then for any Schwartz map , the product function is integrable with respect to the volume measure.
Distribution-bounded functions are integrable against the derivatives of Schwartz maps
#integrable_space_fderivLet be a natural number and let be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (satisfies `IsDistBounded f`), then for any Schwartz map and any vector , the function is integrable with respect to the volume measure, where denotes the Fréchet derivative of at applied to the vector .
Product of a distribution-bounded function and the derivative of a Schwartz map is integrable
#integrable_space_fderiv_mulLet be a distribution-bounded function on a -dimensional Euclidean space. For any Schwartz map and any vector , the function is integrable with respect to the volume measure on , where denotes the Fréchet derivative of at applied to the vector .
Temperate growth of and implies temperate growth of
#instHasTemperateGrowthProdProdOfOpensMeasurableSpaceLet and be normed additive commutative groups equipped with measurable structures. If and are measures on and respectively that both have temperate growth, then the product measure on the product space also has temperate growth, provided that the product space is an opens-measurable space (i.e., its -algebra is generated by its open sets).
Integrability of distribution-bounded functions against space-time Schwartz maps
#integrable_time_spaceLet be a natural number and be a distribution-bounded function mapping into a normed space . For any Schwartz map in the space , the function is integrable over with respect to the volume measure.
If is distribution-bounded, then is integrable for some
#integrable_mul_inv_powLet be a natural number and be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (i.e., it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form where ), then there exists a natural number such that the function \[ x \mapsto \frac{1}{(1 + \|x\|)^r} f(x) \] is integrable with respect to the volume measure on .
Integral of a distribution-bounded function is bounded by Schwartz seminorms
#integral_mul_schwartzMap_boundedLet be a distribution-bounded function from a -dimensional Euclidean space to a normed space . Then there exist a finite set of indices and a non-negative real constant such that for any Schwartz map , the norm of the integral of against is bounded by the supremum of a finite family of Schwartz seminorms: \[ \left\| \int_{\text{Space } d} \eta(x) f(x) \, dx \right\| \le C \cdot \max_{(k, \ell) \in s} p_{k, \ell}(\eta) \] where denotes the -th seminorm in the standard family of seminorms for the Schwartz space .
The zero function is distribution-bounded
#zeroFor any dimension , the constant zero function (where for all ) is distribution-bounded.
The sum of two distribution-bounded functions is distribution-bounded
#addLet be two functions from a -dimensional Euclidean space to a normed space . If both and are distribution-bounded (satisfying the predicate `IsDistBounded`), then their sum is also distribution-bounded.
The Pointwise Sum of Distribution-Bounded Functions is Distribution-Bounded
#fun_addLet be functions from a -dimensional Euclidean space to a normed space . If both and are distribution-bounded (satisfying the predicate `IsDistBounded`), then their pointwise sum is also distribution-bounded.
Finite sums of distribution-bounded functions are distribution-bounded
#sumLet be a natural number and be a finite set of indices. Let be a family of functions from a -dimensional Euclidean space to a normed space indexed by . If for every , the function is distribution-bounded, then their sum is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exist constants , vectors , and integers such that .
The Pointwise Finite Sum of Distribution-Bounded Functions is Distribution-Bounded
#sum_funLet be a natural number and be a finite set of indices. Let be a family of functions from a -dimensional Euclidean space to a normed space indexed by . If for every , the function is distribution-bounded, then their pointwise sum is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exist a finite number of constants , vectors , and integers such that: \[ \|f(x)\| \le \sum_{j=1}^n c_j \|x + g_j\|^{p_j} \]
Scalar multiplication preserves distribution-boundedness
#const_smulLet be a natural number and be a normed space over . If a function is distribution-bounded, then for any constant , the scalar multiple is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exist constants , vectors , and integers such that its norm is bounded by a finite sum: \[ \|f(x)\| \le \sum_{i=1}^n c_i \|x + g_i\|^{p_i} \]
Negation preserves distribution-boundedness
#negLet be a natural number and be a normed space over . If a function is distribution-bounded, then its negation is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exist constants , vectors , and integers such that its norm is bounded by a finite sum: \[ \|f(x)\| \le \sum_{i=1}^n c_i \|x + g_i\|^{p_i} \]
Scalar multiplication of a distribution-bounded function is distribution-bounded
#const_fun_smulLet be a natural number and be a normed space over . If a function is distribution-bounded, then for any constant , the function is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exists a finite sum such that , where , , and .
Constant multiplication preserves distribution-boundedness
#const_mul_funLet be a natural number. If a function is distribution-bounded, then for any constant , the function is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exists a finite natural number such that its norm is bounded by a sum of the form: \[ \|f(x)\| \le \sum_{i=1}^n c_i \|x + g_i\|^{p_i} \] where for each , the coefficient is a non-negative real number (), is a vector in , and the exponent is an integer satisfying .
Multiplication by a constant preserves distribution-boundedness
#mul_const_funLet be a natural number and be a function. If is distribution-bounded, then for any constant , the function is also distribution-bounded.
Components of a Distribution-Bounded Function are Distribution-Bounded
#pi_compLet be a function from a -dimensional space to an -dimensional Euclidean space. If is distribution-bounded, then for any index , the -th component function is also distribution-bounded.
Components of a distribution-bounded Lorentz vector function are distribution-bounded
#vector_componentLet be a function from a -dimensional Euclidean space to the space of -dimensional Lorentz vectors. If is distribution-bounded, then for any index , the scalar-valued function (the -th component of ) is also distribution-bounded.
is distribution-bounded implies is distribution-bounded
#comp_add_rightLet be a function from a -dimensional space to a normed space . If is distribution-bounded (satisfies the predicate `IsDistBounded f`), then for any vector , the function is also distribution-bounded.
is distribution-bounded implies is distribution-bounded
#comp_sub_rightLet be a function from a -dimensional Euclidean space to a normed space . If is distribution-bounded (satisfies the predicate `IsDistBounded f`), then for any vector , the shifted function is also distribution-bounded.
Norm Equality preserves Distribution-Boundedness
#congrLet be a distribution-bounded function and be an almost everywhere strongly measurable function, where and are normed spaces. If for all , then is distribution-bounded.
If and is distribution-bounded, then is distribution-bounded
#monoLet be a natural number, and let and be functions mapping from a -dimensional Euclidean space into normed spaces and , respectively. If is distribution-bounded, is almost everywhere strongly measurable, and the norm of is point-wise bounded by the norm of (i.e., for all ), then is also distribution-bounded.
If is distribution-bounded, then is distribution-bounded
#inner_leftLet be a distribution-bounded function. This means that is almost everywhere strongly measurable and its norm is bounded by a finite sum of the form \[ \|f(x)\| \le \sum_{i=1}^k c_i \|x + g_i\|^{p_i} \] where , , and the integers satisfy . For any constant vector , the scalar-valued function mapping to the real inner product is also distribution-bounded.
Scalar multiplication by a constant vector preserves distribution-boundedness
#smul_constLet be a natural number and be a normed space over . If is a distribution-bounded function, then for any constant vector , the function mapping to the scalar product is also distribution-bounded.
Constant functions are distribution-bounded
#constLet be a natural number and be a normed space. For any element , the constant function defined by for all is distribution-bounded (satisfies `IsDistBounded`).
is distribution-bounded for
#powLet be a -dimensional Euclidean space. For any integer such that , the function defined by is distribution-bounded.
is distribution-bounded for
#pow_shiftFor any dimension , integer exponent such that , and any vector , the function mapping to is distribution-bounded (satisfies `IsDistBounded`).
is distribution-bounded for
#inv_shiftFor any dimension and any vector , the function mapping to the inverse Euclidean norm is distribution-bounded (satisfies the property `IsDistBounded`).
is distribution-bounded for
#nat_powLet be a -dimensional Euclidean space. For any natural number , the function defined by is distribution-bounded.
is distribution-bounded for
#norm_add_nat_powLet be a -dimensional Euclidean space. For any natural number and any real number , the function defined by is distribution-bounded (satisfies the predicate `IsDistBounded`). Here, denotes the Euclidean norm on .
is distribution-bounded for and
#norm_add_pos_nat_zpowLet be a -dimensional Euclidean space. For any integer and any real number , the function defined by is distribution-bounded (satisfies the predicate `IsDistBounded`). Here, denotes the Euclidean norm on .
is distribution-bounded for
#nat_pow_shiftFor any dimension , natural number exponent , and vector , the function mapping to is distribution-bounded (satisfies the predicate `IsDistBounded`).
is distribution-bounded
#norm_subFor any dimension and any vector , the function mapping to the Euclidean norm is distribution-bounded.
is distribution-bounded
#norm_addFor any dimension and any vector , the function mapping to the Euclidean norm is distribution-bounded (satisfies the predicate `IsDistBounded`).
is distribution-bounded for
#invFor any natural number , let be the dimension of the Euclidean space . The function defined by is distribution-bounded.
is distribution-bounded
#normLet be a -dimensional Euclidean space. The function defined by , which maps each vector to its Euclidean norm, is distribution-bounded.
is distribution-bounded for
#log_normFor any natural number , let be the dimension of the Euclidean space . The function defined by is distribution-bounded.
is distribution-bounded for
#zpow_smul_selfLet be a -dimensional Euclidean space. For any integer such that , the function defined by is distribution-bounded.
is distribution-bounded for
#zpow_smul_repr_selfLet be a -dimensional Euclidean space and let denote the coordinate representation of a vector with respect to the standard orthonormal basis. For any integer such that , the function is distribution-bounded.
is distribution-bounded for
#zpow_smul_repr_self_subLet be a -dimensional Euclidean space. For any vector and any integer such that , the function mapping to is distribution-bounded. Here, denotes the coordinate representation of a vector with respect to the standard orthonormal basis of .
is distribution-bounded for
#inv_pow_smul_selfLet be a -dimensional Euclidean space. For any natural number such that , the function defined by is distribution-bounded.
is distribution-bounded for
#inv_pow_smul_repr_selfLet be a -dimensional Euclidean space. For any natural number such that , the function , where denotes the coordinate representation of the vector with respect to the standard orthonormal basis, is distribution-bounded.
is distribution-bounded
#norm_smul_nat_powLet be a -dimensional Euclidean space. For any natural number and any vector , the function defined by is distribution-bounded. (A function is distribution-bounded if it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form where ).
is distribution-bounded for
#norm_smul_zpowLet be a -dimensional Euclidean space. For any vector and any integer such that , the function defined by is distribution-bounded. (A function is distribution-bounded if it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form where ).
Multiplication by the norm preserves distribution-boundedness
#norm_smul_isDistBoundedLet be a natural number and be a normed space over . If a function is distribution-bounded, then the function mapping to is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exists a finite natural number such that its norm is bounded by a sum of the form: \[ \|f(x)\| \le \sum_{i=1}^n c_i \|x + g_i\|^{p_i} \] where for each , the coefficient is a non-negative real number, is a vector in , and the exponent is an integer satisfying .
Multiplication by preserves distribution-boundedness for real-valued functions
#norm_mul_isDistBoundedLet be a natural number and be a real-valued function. If is distribution-bounded, then the function mapping to is also distribution-bounded. A function is distribution-bounded if it is almost everywhere strongly measurable and there exists a finite natural number such that its absolute value is bounded by a sum of the form: \[ |f(x)| \le \sum_{i=1}^n c_i \|x + g_i\|^{p_i} \] where for each , the coefficient is a non-negative real number, is a vector in , and the exponent is an integer satisfying .
Multiplication by a coordinate preserves distribution-boundedness
#component_smul_isDistBoundedLet be a natural number and be a normed space over . If a function is distribution-bounded, then for any coordinate index , the function mapping to the scalar product of its -th coordinate and the value , given by , is also distribution-bounded.
Multiplication by a coordinate preserves distribution-boundedness for real-valued functions
#component_mul_isDistBoundedLet be a natural number and let be a real-valued function. If is distribution-bounded, then for any coordinate index , the function mapping to is also distribution-bounded, where denotes the -th coordinate of the vector .
Scalar multiplication by preserves distribution-boundedness
#isDistBounded_smul_selfLet be a natural number and be a real-valued function. If is distribution-bounded, then the vector-valued function mapping to the scalar multiplication is also distribution-bounded.
If is distribution-bounded, then is distribution-bounded
#isDistBounded_smul_self_reprLet be a natural number and be a distribution-bounded function. Then the function mapping to the scalar-vector product is also distribution-bounded, where denotes the coordinate representation of with respect to the standard orthonormal basis of .
If is distribution-bounded, then is distribution-bounded
#isDistBounded_smul_innerLet be a natural number and be a normed space over . Suppose is a distribution-bounded function. For any fixed vector , the function , formed by scaling by the inner product of and , is also distribution-bounded. Recall that a function is distribution-bounded if it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form , where , , and .
If is distribution-bounded, then is distribution-bounded
#isDistBounded_smul_inner_of_smul_normLet be a natural number and be a normed space over . Let be an almost everywhere strongly measurable function. If the function is distribution-bounded, then for any fixed vector , the function is also distribution-bounded. Recall that a function is distribution-bounded if it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form , where and .
If is distribution-bounded, then is distribution-bounded
#isDistBounded_mul_innerLet be a natural number and let be a distribution-bounded function. For any fixed vector , the function , defined by the product of the inner product and , is also distribution-bounded. Recall that a function is distribution-bounded if it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form , where , , and .
If is distribution-bounded, then is distribution-bounded
#isDistBounded_mul_inner'Let be a natural number and let be a distribution-bounded function. For any fixed vector , the function , defined as the product of the inner product of and with the value of , is also distribution-bounded. Recall that a function is distribution-bounded if it is almost everywhere strongly measurable and its norm is bounded by a finite sum of terms of the form , where , , and .
If is distribution-bounded, then is distribution-bounded
#isDistBounded_mul_inner_of_smul_normLet be a natural number and let be an almost everywhere strongly measurable function. If the function is distribution-bounded, then for any fixed vector , the function is also distribution-bounded. Recall that a function is distribution-bounded if it is almost everywhere strongly measurable and its norm is bounded by a finite sum of the form , where and .
The function is distribution-bounded in dimension
#mul_inner_pow_neg_twoLet be a natural number and let be a Euclidean space of dimension . For any vector , the function defined by is distribution-bounded.
