MarkovProcess.Path.DenseRestrictionIntegral
DefinitionMarkovProcessModule_MarkovProcess_Path_DenseRestrictionIntegralmarkovprocessmarkovprocess-module-importscope-mainscott-armstrongsource-faithful
Integrals of finite dense-time marginals of a path measure
Integrating a compactly supported test against the finite dense-time marginal of a measure on continuous-path space is integrating the composed test against the measure itself. This is a change-of-variables identity with no probabilistic content.
Complete pinned Lean module MarkovProcess.Path.DenseRestrictionIntegral by Scott Armstrong (Apache-2.0). Contains the original definitions, instances, theorems and proofs in their original declaration order. Only local MarkovProcess import directives have been rewritten for Prove2Me; source mathematical declarations are unchanged. The bundle must pass Prove2Me's remote compiler before it can be used as a dependency.
Definition code
/-
Copyright (c) 2026 Scott Armstrong. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Armstrong
-/
import Definitions.Def_MarkovProcessModule_MarkovProcess_Continuity_DenseTimeContinuousExtension
import Mathlib.Topology.ContinuousMap.CompactlySupported
/-!
# Integrals of finite dense-time marginals of a path measure
Integrating a compactly supported test against the finite dense-time marginal of a measure on
continuous-path space is integrating the composed test against the measure itself. This is a
change-of-variables identity with no probabilistic content.
-/
open MeasureTheory
open scoped CompactlySupported
namespace MarkovProcess
namespace ContinuousPath
variable {alpha : Type*} [TopologicalSpace alpha] [SecondCountableTopology alpha]
[MeasurableSpace alpha] [BorelSpace alpha]
/-- A compactly supported test integrated against a finite dense-time marginal of a path measure
is the composed test integrated against the path measure. -/
theorem integral_map_denseRestriction_map_restrict
(nu : Measure (ContinuousPath alpha)) (J : Finset DenseTime) (f : C_c(J → alpha, ℝ)) :
∫ z, f z ∂((nu.map denseRestriction).map J.restrict) =
∫ omega, f (J.restrict (denseRestriction omega)) ∂nu := by
have hdense := measurable_denseRestriction (alpha := alpha)
have hrestrict := Finset.measurable_restrict (X := fun _ ↦ alpha) J
rw [Measure.map_map hrestrict hdense]
exact integral_map (hrestrict.comp hdense).aemeasurable
f.continuous.stronglyMeasurable.aestronglyMeasurable
end ContinuousPath
end MarkovProcess
Source