From measurable cube resolvents to stream transition laws

The analytic minimal resolvent is a countable supremum of cube resolvents, with positive and negative parts supplying its real-valued version.

theorem Algsuperdiff.Section5.Measurability.measurable_streamResolvent_of_cube {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (hcube : ∀ (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) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : Measurable fun (p : Field.FullSample d M.gamma × HCPolySupport.Vec d) => (((Field.streamWholeSpaceResolvent M p.1).operator mu) f) p.2

theorem Algsuperdiff.Section5.Measurability.measurable_streamTransition_of_cube {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (hcube : ∀ (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) (t : NNReal) : Measurable fun (p : Field.FullSample d M.gamma × HCPolySupport.Vec d) => ((Field.streamWholeSpaceResolvent M p.1).kernelSemigroup.kernel t) p.2