EconCSLib.SocialChoice.FairDivision.Divisible.UnitInterval #

Shared measure-theoretic helpers for divisible allocation on intervals.

This file collects reusable facts that are needed by multiple cake-cutting proofs. It keeps the algorithm files focused on their allocation arguments rather than duplicating basic measure-continuity infrastructure.

source

instance SocialChoice.FairDivision.Divisible.noAtomsMapSubtypeVal (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.NoAtoms μ] :

MeasureTheory.NoAtoms (MeasureTheory.Measure.map Subtype.val μ)

Non-atomicity is preserved when a measure on the unit interval is pushed forward along the subtype inclusion into ℝ.

source

theorem SocialChoice.FairDivision.Divisible.cdfRealContinuous (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.NoAtoms ν] :

Continuous fun (t : ℝ) => (ν (Set.Iic t)).toReal

The CDF t ↦ (ν (Iic t)).toReal is continuous for a non-atomic finite measure on ℝ.