Fernique's theorem for rotation-invariant measures #
Let μ be a finite measure on a second-countable normed space E such that the product measure
μ.prod μ on E × E is invariant by rotation of angle -π/4.
Then there exists a constant C > 0 such that the function x ↦ exp (C * ‖x‖ ^ 2) is integrable
with respect to μ.
Sketch of the proof #
The main case of the proof is for μ a probability measure such that there exists a positive
a : ℝ such that 2⁻¹ < μ {x | ‖x‖ ≤ a} < 1. If μ is a probability measure and a does not
exist then we can show that there is a ball with finite radius of measure 1, and the result is true
for C = 1 (for example), since x ↦ exp (‖x‖ ^ 2) is almost surely bounded.
We then choose such an a.
In order to show the existence of C such that x ↦ exp (C * ‖x‖ ^ 2) is integrable, we prove as
intermediate result that for a, c with 2⁻¹ < c ≤ μ {x | ‖x‖ ≤ a},
the integral ∫⁻ x, exp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2) ∂μ is bounded by a finite quantity
(logRatio c is a multiple of log (c / (1 - c))). We can then take C = logRatio c * a⁻¹ ^ 2.
We now turn to the proof of the intermediate result.
First in measure_le_mul_measure_gt_le_of_map_rotation_eq_self we prove that if a measure μ is
such that μ.prod μ is invariant by rotation of angle -π/4 then
μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2.
The rotation invariance is used only through that inequality.
We define a sequence of thresholds t n inductively by t 0 = a and t (n + 1) = √2 * t n + a.
They are chosen such that the invariance by rotation gives
μ {x | ‖x‖ ≤ a} * μ {x | t (n + 1) < ‖x‖} ≤ μ {x | t n < ‖x‖} ^ 2.
Thanks to that inequality we can show that μ {x | t n < ‖x‖} decreases fast with n:
for mₐ = μ {x | ‖x‖ ≤ a}, μ {x | t n < ‖x‖} ≤ mₐ * exp (- log (mₐ / (1 - mₐ)) * 2 ^ n).
We cut the space into annuli {x | t n < ‖x‖ ≤ t n + 1} and bound the integral separately on
each annulus. On that set the function exp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2) is bounded by
exp (logRatio c * a⁻¹ ^ 2 * t (n + 1) ^ 2), which is in turn less than
exp (2⁻¹ * log (c / (1 - c)) * 2 ^ n) (from the definition of the threshold t and logRatio c).
The measure of the annulus is bounded by μ {x | t n < ‖x‖}, for which we derived an upper bound
above. The function gets exponentially large, but μ {x | t n < ‖x‖} decreases even faster, so the
integral is bounded by a quantity of the form exp (- u * 2 ^ n) for u>0.
Summing over all annuli (over n) gives a finite value for the integral.
Main statements #
- lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self: for- μa probability measure whose product with itself is invariant by rotation and for- a, cwith- 2⁻¹ < c ≤ μ {x | ‖x‖ ≤ a}, the integral- ∫⁻ x, exp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2) ∂μis bounded by a quantity that does not depend on- a.
- exists_integrable_exp_sq_of_map_rotation_eq_self: Fernique's theorem for finite measures whose product is invariant by rotation.
References #
- [Xavier Fernique, Intégrabilité des vecteurs gaussiens][fernique1970integrabilite]
- [Martin Hairer, An introduction to stochastic PDEs][hairer2009introduction]
TODO #
From the intermediate result lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self,
we can deduce bounds on all the moments of the measure μ as function of powers of
the first moment.
The rotation in E × E with angle θ, as a continuous linear map.
Equations
Instances For
If a measure μ is such that μ.prod μ is invariant by rotation of angle -π/4 then
μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2.
A sequence of real thresholds that will be used to cut the space into annuli.
Chosen such that for a rotation invariant measure, an application of lemma
measure_le_mul_measure_gt_le_of_map_rotation_eq_self gives
μ {x | ‖x‖ ≤ a} * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2.
Equations
Instances For
Auxiliary lemma for lintegral_exp_mul_sq_norm_le_mul, in which we find an upper bound on an
integral by dealing separately with the contribution of each set in a sequence of annuli.
This is the bound of the integral over one of those annuli.
For μ a probability measure whose product with itself is invariant by rotation and for a, c
with 2⁻¹ < c ≤ μ {x | ‖x‖ ≤ a}, the integral ∫⁻ x, exp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2) ∂μ
is bounded by a quantity that does not depend on a.
Auxiliary lemma for exists_integrable_exp_sq_of_map_rotation_eq_self.
The assumptions on a and μ {x | ‖x‖ ≤ a} are not needed and will be removed in that more
general theorem.
Auxiliary lemma for exists_integrable_exp_sq_of_map_rotation_eq_self, in which we will replace
the assumption IsProbabilityMeasure μ by the weaker IsFiniteMeasure μ.
Fernique's theorem for finite measures whose product is invariant by rotation: there exists
C > 0 such that the function x ↦ exp (C * ‖x‖ ^ 2) is integrable.