Theorems · Theorem · probability

ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self

∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∃ C, 0 < C ∧ MeasureTheory.Integrable (fun x => 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.

Defined in

Mathlib.Probability.Distributions.Fernique

Cited by

1 results in Mathlib

Foundations

Depth 227 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupNormedSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasure