Interval contents on ordered types

[Kri89] [Kri98] [Rou26]

A finitely additive, strictly positive content on the nonempty closed intervals of a preorder, valued in an ordered additive monoid. The order-theoretic sibling of ExtMeasure (Semantics/Mereology.lean, [Kri98]'s extensive measure functions over a SemilatticeSup): disjoint intervals have no interval join, so the two substrates coexist rather than one subsuming the other.

Mathlib's NonemptyInterval.length is the canonical group-valued example (ofStrictMono at F = id); its length_add is additivity over Minkowski interval addition, orthogonal to the concatenation additivity axiomatized here, which mathlib does not state.

Main declarations

• IsIntervalContent: additivity over interval concatenation plus strict positivity on nondegenerate intervals.
• IsIntervalContent.ofStrictMono: Stieltjes-style constructor — a strictly monotone potential F into an ordered group induces the content fun i => F i.snd - F i.fst.
• IsIntervalContent.measure_lt_of_left_lt: moving the left endpoint strictly right strictly decreases measure.
• IsIntervalContent.not_isLeast_rightAnchored: over a dense order, the measures of right-anchored covers [l, s] with l strictly below a point have no least element — the domain-general form of [Rou26]'s G-TIA information collapse.

class Core.Order.IsIntervalContent {α : Type u_1} {M : Type u_2} [Preorder α] [AddCommMonoid M] [PartialOrder M] (μ : NonemptyInterval α → M) : Prop

A finitely additive, strictly positive content on the nonempty closed intervals of a preorder: the order-interval counterpart of [Kri98]'s extensive measure functions (ExtMeasure).

• additive (a b c : α) (hab : a ≤ b) (hbc : b ≤ c) : μ { fst := a, snd := c, fst_le_snd := ⋯ } = μ { fst := a, snd := b, fst_le_snd := hab } + μ { fst := b, snd := c, fst_le_snd := hbc }

  Additivity over interval concatenation.

• positive (a b : α) (h : a < b) : 0 < μ { fst := a, snd := b, fst_le_snd := ⋯ }

  Strict positivity on nondegenerate intervals.

theorem Core.Order.IsIntervalContent.degenerate_eq_zero {α : Type u_1} {M : Type u_2} [Preorder α] [AddCommMonoid M] [PartialOrder M] (μ : NonemptyInterval α → M) [IsIntervalContent μ] [IsCancelAdd M] (a : α) : μ { fst := a, snd := a, fst_le_snd := ⋯ } = 0

Degenerate intervals have measure zero, given cancellation.

theorem Core.Order.IsIntervalContent.measure_lt_of_left_lt {α : Type u_1} {M : Type u_2} [Preorder α] [AddCommMonoid M] [PartialOrder M] (μ : NonemptyInterval α → M) [IsIntervalContent μ] [AddRightStrictMono M] {a b s : α} (hab : a < b) (hbs : b ≤ s) : μ { fst := b, snd := s, fst_le_snd := hbs } < μ { fst := a, snd := s, fst_le_snd := ⋯ }

Moving the left endpoint strictly right strictly decreases measure.

theorem Core.Order.IsIntervalContent.measure_lt_of_lt_right {α : Type u_1} {M : Type u_2} [Preorder α] [AddCommMonoid M] [PartialOrder M] (μ : NonemptyInterval α → M) [IsIntervalContent μ] [AddLeftStrictMono M] {a b s : α} (hab : a ≤ b) (hbs : b < s) : μ { fst := a, snd := b, fst_le_snd := hab } < μ { fst := a, snd := s, fst_le_snd := ⋯ }

Moving the right endpoint strictly right strictly increases measure.

theorem Core.Order.IsIntervalContent.not_isLeast_rightAnchored {α : Type u_1} {M : Type u_2} [LinearOrder α] [DenselyOrdered α] [AddCommMonoid M] [PartialOrder M] [AddRightStrictMono M] (μ : NonemptyInterval α → M) [IsIntervalContent μ] {a s : α} (has : a ≤ s) (x : M) : ¬IsLeast (Set.range fun (l : ↑(Set.Iio a)) => μ { fst := ↑l, snd := s, fst_le_snd := ⋯ }) x

No minimal right-anchored cover: over a dense order, the measures of intervals [l, s] with left endpoint strictly below a have no least element — the domain-general form of [Rou26]'s G-TIA information collapse ("there cannot be a smallest open interval to include a closed time"). Decomposes through StrictAnti.map_isLeast: a least measure would be a greatest left endpoint, which density forbids.

theorem Core.Order.IsIntervalContent.ofStrictMono {α : Type u_1} [Preorder α] {G : Type u_3} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] (F : α → G) (hF : StrictMono F) : IsIntervalContent fun (i : NonemptyInterval α) => F i.toProd.2 - F i.toProd.1

Stieltjes-style constructor: a strictly monotone potential into an ordered group induces an interval content. Additivity is telescoping; positivity is the strict monotonicity. At F = id this recovers NonemptyInterval.length.