Measurability and measure extensionality on ordered Borel spaces

A lower semicontinuous function into a second-countable linear order is Borel measurable (LowerSemicontinuous.measurable). The same holds when lower semicontinuity fails at countably many points: each superlevel set {f > y} is the union of its interior, which contains every superlevel point where f is lower semicontinuous, and of a countable set.

Such functions arise, for instance, as the perimeter of the superlevel sets {u > t} of a function u as a function of the level t, which is lower semicontinuous at every level whose level set is null, hence off a countable set.

Main results

• TauCeti.measurable_of_countable_not_lowerSemicontinuousAt: a function that is lower semicontinuous at all but countably many points is measurable.
• MeasureTheory.Measure.ext_of_Iic': measures finite on initial intervals are determined by their masses on those intervals, without a finite-total-mass assumption.

theorem TauCeti.measurable_of_countable_not_lowerSemicontinuousAt {α : Type u_1} {δ : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [TopologicalSpace δ] [MeasurableSpace δ] [OpensMeasurableSpace δ] [MeasurableSingletonClass δ] {f : δ → α} (hf : {x : δ | ¬LowerSemicontinuousAt f x}.Countable) : Measurable f

A function that is lower semicontinuous at all but countably many points is measurable.

theorem MeasureTheory.Measure.ext_of_Iic' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α) (hμ : ∀ (a : α), μ (Set.Iic a) ≠ ⊤) (h : ∀ (a : α), μ (Set.Iic a) = ν (Set.Iic a)) : μ = ν

Two measures finite on initial intervals are equal if they agree on all initial intervals. Unlike Measure.ext_of_Iic, this does not require finite total mass.