Determining a symmetric real probability measure from positive tails

Symmetric probability measures with equal positive upper tails agree. The cap formula then identifies the sphere height distribution with uniform measure on [-1,1].

theorem LiebThirring.symmetric_probability_ext_of_positive_tails (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : MeasureTheory.Measure.map (fun (x : ℝ) => -x) μ = μ) (hν : MeasureTheory.Measure.map (fun (x : ℝ) => -x) ν = ν) (h : ∀ t > 0, μ (Set.Ioi t) = ν (Set.Ioi t)) : μ = ν

Reflection symmetry and agreement of strictly positive upper tails determine an arbitrary real probability measure.

theorem LiebThirring.eq_uniform_interval_of_symmetric_positive_tails (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Measure.map (fun (z : ℝ) => -z) μ = μ) (h : ∀ t > 0, μ (Set.Ioi t) = (ENNReal.ofReal 2)⁻¹ * ENNReal.ofReal (max (1 - t) 0)) : μ = (ENNReal.ofReal 2)⁻¹ • MeasureTheory.volume.restrict (Set.Icc (-1) 1)

A symmetric probability distribution with the uniform positive-tail formula is normalized Lebesgue measure on [-1, 1].