Documentation

Mathlib.Probability.Distributions.Fernique

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 #

References #

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.

theorem StrictMono.exists_between_of_tendsto_atTop {β : Type u_1} [LinearOrder β] {t : β} (ht_mono : StrictMono t) (ht_tendsto : Filter.Tendsto t Filter.atTop Filter.atTop) {x : β} (hx : t 0 < x) :
∃ (n : ), t n < x x t (n + 1)
noncomputable def ContinuousLinearMap.rotation {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] (θ : ) :
E × E →L[] E × E

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

          A quantity that appears in exponentials in the proof of Fernique's theorem.

          Equations
            Instances For
              theorem ProbabilityTheory.Fernique.logRatio_pos {c : ENNReal} (hc_gt : 2⁻¹ < c) (hc_lt : c < 1) :

              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.

              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.