Theorems · Theorem · probability

ProbabilityTheory.measure_le_mul_measure_gt_le_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.SFinite μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∀ (a b : ℝ), μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (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.

Defined in

Mathlib.Probability.Distributions.Fernique

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupNormedSpaceSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.SFinite