Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section5.Measurability.DisplacementExpectations

Measurability of canonical quenched expectations #

The transition argument is adapted from the Apache-2.0 upstream SuperdiffusionAudit/Support/SuperdiffusivityTransition.lean at commit 7f20476385d4af418f110303085ad0740c9eba46. Here it applies directly to the production process, so no duplicate diffusion characterization is needed.

source
theorem Algsuperdiff.Section5.Measurability.integral_streamProcess_eq_transition {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (x : HCPolySupport.Vec d) (t : NNReal) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {G : HCPolySupport.Vec d → E} (hG : Continuous G) :
∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), G (DivergenceFormProcess.Form.onePointRetract 0 (path t)) ∂(Field.streamProcess M omega) ↑x = ∫ (y : HCPolySupport.Vec d), G y ∂((Field.streamWholeSpaceResolvent M omega).kernelSemigroup.kernel t) x

The canonical displacement observable has the live transition law.

source
theorem Algsuperdiff.Section5.Measurability.measurable_streamTransition_point {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (x : HCPolySupport.Vec d) (t : NNReal) :
Measurable fun (omega : Field.FullSample d M.gamma) => ((Field.streamWholeSpaceResolvent M omega).kernelSemigroup.kernel t) x

A fixed starting point gives a measurable family of live transition measures.

source
theorem Algsuperdiff.Section5.Measurability.measurable_integral_streamProcess {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (x : HCPolySupport.Vec d) (t : NNReal) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {G : HCPolySupport.Vec d → E} (hG : Continuous G) :
Measurable fun (omega : Field.FullSample d M.gamma) => ∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), G (DivergenceFormProcess.Form.onePointRetract 0 (path t)) ∂(Field.streamProcess M omega) ↑x

Continuous observables of the canonical process have measurable quenched expectations.

source
theorem Algsuperdiff.Section5.Measurability.measurable_streamProcess_displacement_expectations {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (t : NNReal) :
(Measurable fun (omega : Field.FullSample d M.gamma) => ∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (path t) ∂(Field.streamProcess M omega) ↑0) ∧ Measurable fun (omega : Field.FullSample d M.gamma) => ∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (path t)) ∂(Field.streamProcess M omega) ↑0

Both quenched displacement expectations in Theorem A are measurable.