Theorems · Theorem · probability

ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure

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

Defined in

Mathlib.Probability.Distributions.Fernique

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsProbabilityMeasure