# 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, 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`.
- `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.

source
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)
source
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

- ContinuousLinearMap.rotation θ = { toFun := fun (x : E × E) => (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Instances For

source
theorem ContinuousLinearMap.rotation_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (θ : ℝ) (x : E × E) :
(rotation θ) x = (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2)
source
theorem ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_self {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] (h : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) (a b : ℝ) :
μ {x : E | ‖x‖ ≤ a} * μ {x : E | b < ‖x‖} ≤ μ {x : E | (b - a) / √2 < ‖x‖} ^ 2

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`.

source
noncomputable def ProbabilityTheory.Fernique.normThreshold (a : ℝ) :
ℕ → ℝ

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

- ProbabilityTheory.Fernique.normThreshold a = arithGeom (√2) a a

Instances For

source
theorem ProbabilityTheory.Fernique.normThreshold_zero {a : ℝ} :
normThreshold a 0 = a
source
theorem ProbabilityTheory.Fernique.normThreshold_add_one {a : ℝ} (n : ℕ) :
normThreshold a (n + 1) = √2 * normThreshold a n + a
source
theorem ProbabilityTheory.Fernique.measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) (a : ℝ) (n : ℕ) :
μ {x : E | ‖x‖ ≤ a} * μ {x : E | normThreshold a (n + 1) < ‖x‖} ≤ μ {x : E | normThreshold a n < ‖x‖} ^ 2
source
theorem ProbabilityTheory.Fernique.lt_normThreshold_zero {a : ℝ} (ha_pos : 0 < a) :
a / (1 - √2) < normThreshold a 0
source
theorem ProbabilityTheory.Fernique.normThreshold_strictMono {a : ℝ} (ha_pos : 0 < a) :
StrictMono (normThreshold a)
source
theorem ProbabilityTheory.Fernique.tendsto_normThreshold_atTop {a : ℝ} (ha_pos : 0 < a) :
Filter.Tendsto (normThreshold a) Filter.atTop Filter.atTop
source
theorem ProbabilityTheory.Fernique.normThreshold_eq {a : ℝ} (n : ℕ) :
normThreshold a n = a * (1 + √2) * (√2 ^ (n + 1) - 1)
source
theorem ProbabilityTheory.Fernique.sq_normThreshold_add_one_le {a : ℝ} (n : ℕ) :
normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)
source
theorem ProbabilityTheory.Fernique.measure_gt_normThreshold_le_rpow {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) (ha_gt : 2⁻¹ < μ {x : E | ‖x‖ ≤ a}) (n : ℕ) :
μ {x : E | normThreshold a n < ‖x‖} ≤ μ {x : E | ‖x‖ ≤ a} * ((1 - μ {x : E | ‖x‖ ≤ a}) / μ {x : E | ‖x‖ ≤ a}) ^ 2 ^ n
source
theorem ProbabilityTheory.Fernique.measure_gt_normThreshold_le_exp {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) (ha_gt : 2⁻¹ < μ {x : E | ‖x‖ ≤ a}) (ha_lt : μ {x : E | ‖x‖ ≤ a} < 1) (n : ℕ) :
μ {x : E | normThreshold a n < ‖x‖} ≤ μ {x : E | ‖x‖ ≤ a} * ENNReal.ofReal (Real.exp (-Real.log (μ {x : E | ‖x‖ ≤ a} / (1 - μ {x : E | ‖x‖ ≤ a})).toReal * 2 ^ n))
source
noncomputable def ProbabilityTheory.Fernique.logRatio (c : ENNReal) :
ℝ

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

Equations

- ProbabilityTheory.Fernique.logRatio c = Real.log (c.toReal / (1 - c).toReal) / (8 * (1 + √2) ^ 2)

Instances For

source
theorem ProbabilityTheory.Fernique.logRatio_pos {c : ENNReal} (hc_gt : 2⁻¹ < c) (hc_lt : c < 1) :
0 < logRatio c
source
theorem ProbabilityTheory.Fernique.logRatio_nonneg {c : ENNReal} (hc_ge : 2⁻¹ ≤ c) (hc_le : c ≤ 1) :
0 ≤ logRatio c
source
theorem ProbabilityTheory.Fernique.logRatio_mono {c d : ENNReal} (hc : 2⁻¹ < c) (hd : d < 1) (h : c ≤ d) :
logRatio c ≤ logRatio d
source
theorem ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_le {a : ℝ} {c : ENNReal} (hc_gt : 2⁻¹ < c) (hc_lt : c < 1) (n : ℕ) :
logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2 ≤ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n
source
theorem ProbabilityTheory.Fernique.lintegral_closedBall_diff_exp_logRatio_mul_sq_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) (ha_gt : 2⁻¹ < μ {x : E | ‖x‖ ≤ a}) (ha_lt : μ {x : E | ‖x‖ ≤ a} < 1) (n : ℕ) :
∫⁻ (x : E) in Metric.closedBall 0 (normThreshold a (n + 1)) \ Metric.closedBall 0 (normThreshold a n), ENNReal.ofReal (Real.exp (logRatio (μ {x : E | ‖x‖ ≤ a}) * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤ μ {x : E | ‖x‖ ≤ a} * ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (μ {x : E | ‖x‖ ≤ a} / (1 - μ {x : E | ‖x‖ ≤ a})).toReal * 2 ^ n))

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.

source
theorem ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) (ha_pos : 0 < a) {c' : ENNReal} (hc' : c' ≤ μ {x : E | ‖x‖ ≤ a}) (hc'_gt : 2⁻¹ < c') :
∫⁻ (x : E), ENNReal.ofReal (Real.exp (logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤ μ {x : E | ‖x‖ ≤ a} * (ENNReal.ofReal (Real.exp (logRatio c')) + ∑' (n : ℕ), ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))
source
theorem ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) {c : ENNReal} (hc : c ≤ μ {x : E | ‖x‖ ≤ a}) (hc_gt : 2⁻¹ < c) :
∫⁻ (x : E), ENNReal.ofReal (Real.exp (Fernique.logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (Real.exp (Fernique.logRatio c)) + ∑' (n : ℕ), ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

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`.

source
theorem ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self' {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) {a : ℝ} (ha_pos : 0 < a) (ha_gt : 2⁻¹ < μ {x : E | ‖x‖ ≤ a}) (ha_lt : μ {x : E | ‖x‖ ≤ a} < 1) :
∃ (C : ℝ), 0 < C ∧ MeasureTheory.Integrable (fun (x : E) => Real.exp (C * ‖x‖ ^ 2)) μ

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.

source
theorem ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) :
∃ (C : ℝ), 0 < C ∧ MeasureTheory.Integrable (fun (x : E) => Real.exp (C * ‖x‖ ^ 2)) μ

Auxiliary lemma for `exists_integrable_exp_sq_of_map_rotation_eq_self`, in which we will replace the assumption `IsProbabilityMeasure μ` by the weaker `IsFiniteMeasure μ`.

source
theorem ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) :
∃ (C : ℝ), 0 < C ∧ MeasureTheory.Integrable (fun (x : E) => Real.exp (C * ‖x‖ ^ 2)) μ

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.