Measurable families generated by positive C₀ resolvents

This file propagates joint parameter/state measurability of resolvent evaluations through the Poisson--Yosida construction of the generated semigroup. It is deliberately independent of any particular coefficient field.

noncomputable def Algsuperdiff.Section5.Measurability.scaledResolventKernel {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (R : Ω → MarkovProcess.PositiveC0ContractiveResolvent X) (hR : ∀ (alpha : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap X ℝ), Measurable fun (p : Ω × X) => (((R p.1).operator alpha) f) p.2) (alpha : ↑MarkovProcess.Semigroup.PositiveShift) : ProbabilityTheory.Kernel (Ω × X) X

The Riesz kernel of a normalized member of a parameterized resolvent family.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Measurability.measurable_generatedSemigroup_apply {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (R : Ω → MarkovProcess.PositiveC0ContractiveResolvent X) (hR : ∀ (alpha : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap X ℝ), Measurable fun (p : Ω × X) => (((R p.1).operator alpha) f) p.2) (t : NNReal) (f : ZeroAtInftyContinuousMap X ℝ) : Measurable fun (p : Ω × X) => (((R p.1).generatedSemigroup.operator t) f) p.2

Joint parameter/state measurability of evaluations of the semigroup canonically generated by a positive C₀ contractive resolvent family.

theorem Algsuperdiff.Section5.Measurability.measurable_kernelSemigroup_family {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (R : Ω → MarkovProcess.PositiveC0ContractiveResolvent X) (hR : ∀ (alpha : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap X ℝ), Measurable fun (p : Ω × X) => (((R p.1).operator alpha) f) p.2) (t : NNReal) : Measurable fun (p : Ω × X) => ((R p.1).kernelSemigroup.kernel t) p.2

At every fixed time, the transition measures represented by a jointly measurable positive C₀ resolvent family form a jointly measurable family in the parameter and starting state.