Measurability of stream cube resolvents

The stream coefficient on a compact cube is a measurable continuous-map-valued random variable. Continuous dependence of the shifted weak solution gives measurability of its local integrals, and continuity of the analytic representative then gives pointwise measurability.

theorem Algsuperdiff.Section5.Measurability.measurable_analyticCubeResolvent_stream {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : HCPolySupport.Vec d → ℝ) (hf : Measurable f) (D : ℝ) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) (x : HCPolySupport.Vec d) : Measurable fun (omega : Field.FullSample d M.gamma) => (Field.streamWholeSpaceAnalyticData M omega).analyticCubeResolvent mu f hf hfD m x