The common ground of a measure

This file makes a measure over worlds a discourse state: its common ground is its almost-everywhere filter — what holds almost surely is mutually accepted — and its context set is the set of positive-mass worlds. A graded common ground of this kind is [anderson-2021]'s, updated by mixture rather than by intersection.

Main results

• HasCommonGround.contextSet_measure: the context set of μ is {w | μ {w} ≠ 0}.

References

• [Sta02] — the context set
• [anderson-2021] — the common ground as a distribution over worlds

@[instance_reducible]

instance instHasCommonGroundMeasure {W : Type u_1} [MeasurableSpace W] : HasCommonGround (MeasureTheory.Measure W) W

Equations

• instHasCommonGroundMeasure = { commonGround := MeasureTheory.ae }

@[simp]

theorem HasCommonGround.commonGround_measure {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) : commonGround μ = MeasureTheory.ae μ

theorem HasCommonGround.contextSet_measure {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) : contextSet μ = {w : W | μ {w} ≠ 0}