Measurability of continuous representatives from their averages

Continuity in the spatial variable recovers the value at every interior point from measurable integrals over shrinking balls.

theorem Algsuperdiff.Section5.Measurability.measurable_eval_of_continuousOn_of_setIntegral {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (F : Ω → HCPolySupport.Vec d → ℝ) (hF : ∀ (omega : Ω), ContinuousOn (F omega) U) (hI : ∀ B ⊆ U, Measurable fun (omega : Ω) => ∫ (y : HCPolySupport.Vec d) in B, F omega y) {x : HCPolySupport.Vec d} (hx : x ∈ U) : Measurable fun (omega : Ω) => F omega x