Leray Limit Measurability

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_measurableOn_extension {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] (s : Set α) [(x : α) → Decidable (x ∈ s)] (hs : MeasurableSet s) (f g : α → β) (hf : ContinuousOn f s) (hg : ContinuousOn g sᶜ) : Measurable (s.piecewise f g)

Fields continuous on complementary measurable regions define a measurable piecewise field, as used for extensions in prop:leray-limit.