WIP: Import markovprocess

LeanPool/MarkovProcess/MarkovProcess/Analysis.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2026 Scott Armstrong. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong
+-/
+
+module
+
+public import LeanPool.MarkovProcess.MarkovProcess.Analysis.ExpPrimitive
+public import LeanPool.MarkovProcess.MarkovProcess.Analysis.PaleyZygmund
+
+
+/-!
+# Analysis
+
+Supporting modules for MarkovProcess.
+-/

LeanPool/MarkovProcess/MarkovProcess/Analysis/PaleyZygmund.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 Scott Armstrong. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.MeanInequalities
+public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
+
+
+/-!
+# The Paley--Zygmund inequality
+
+For a nonnegative extended-real random variable `Z` with finite mean on a probability space and a
+level `rho`, the mass above `rho * E Z` is bounded below by the second-moment ratio,
+
+  `(1 - rho) ^ 2 * (E Z) ^ 2 ≤ E (Z ^ 2) * mu {rho * E Z ≤ Z}`.
+
+The subtraction is the truncated one of `ℝ≥0∞`, so a level `rho ≥ 1` leaves the trivial bound and
+needs no separate hypothesis.  The primary form
+(`MeasureTheory.lintegral_sq_mul_measure_ge_le`) is division-free, so it needs neither positivity
+nor finiteness of the second moment; the divided form
+(`MeasureTheory.le_measure_ge_of_lintegral_sq_ne_top`) is the familiar
+`(1 - rho) ^ 2 (E Z) ^ 2 / E (Z ^ 2) ≤ mu {rho * E Z ≤ Z}`, whose finite-mean hypothesis is
+supplied by the second moment through the Cauchy--Schwarz inequality
+(`MeasureTheory.lintegral_le_rpow_lintegral_sq`).
+
+Everything is stated for `ℝ≥0∞`-valued functions and carries no integrability side condition.
+-/
+
+@[expose] public section
+
+open scoped ENNReal NNReal
+
+-- The namespace placement is upstream-facing: this is pure measure theory, with no process
+-- structure and no state space.
+namespace MeasureTheory
+
+variable {Omega : Type*} [MeasurableSpace Omega]
+
+/-- Cauchy--Schwarz on a measurable set: the integral of a nonnegative extended-real function over
+`A` is at most the square root of its second moment times the square root of the mass of `A`. -/
+theorem setLIntegral_le_rpow_lintegral_sq_mul_rpow (mu : Measure Omega) {Z : Omega → ℝ≥0∞}
+    (hZ : AEMeasurable Z mu) {A : Set Omega} (hA : MeasurableSet A) :
+    ∫⁻ omega in A, Z omega ∂mu ≤
+      (∫⁻ omega, Z omega ^ 2 ∂mu) ^ (1 / 2 : ℝ) * (mu A) ^ (1 / 2 : ℝ) := by
+  have hindicator : AEMeasurable (A.indicator (fun _ ↦ (1 : ℝ≥0∞))) mu :=
+    (measurable_const.indicator hA).aemeasurable
+  have hsplit : ∫⁻ omega in A, Z omega ∂mu =
+      ∫⁻ omega, (Z * A.indicator (fun _ ↦ (1 : ℝ≥0∞))) omega ∂mu := by
+    rw [← lintegral_indicator hA]
+    refine lintegral_congr fun omega ↦ ?_
+    by_cases homega : omega ∈ A
+    · simp only [Pi.mul_apply, Set.indicator_of_mem homega, mul_one]
+    · simp only [Pi.mul_apply, Set.indicator_of_notMem homega, mul_zero]
+  have hholder := ENNReal.lintegral_mul_le_Lp_mul_Lq mu Real.HolderConjugate.two_two hZ hindicator
+  have hsquare : ∀ omega : Omega, Z omega ^ (2 : ℝ) = Z omega ^ (2 : ℕ) := by
+    intro omega
+    rw [← ENNReal.rpow_natCast (Z omega) 2]
+    norm_num
+  have hind : ∀ omega : Omega,
+      A.indicator (fun _ ↦ (1 : ℝ≥0∞)) omega ^ (2 : ℝ) =
+        A.indicator (fun _ ↦ (1 : ℝ≥0∞)) omega := by
+    intro omega
+    by_cases homega : omega ∈ A
+    · simp only [Set.indicator_of_mem homega, ENNReal.one_rpow]
+    · simp only [Set.indicator_of_notMem homega]
+      exact ENNReal.zero_rpow_of_pos (by norm_num)
+  rw [hsplit]
+  refine hholder.trans (le_of_eq ?_)
+  rw [lintegral_congr hsquare, lintegral_congr hind, lintegral_indicator_const hA (1 : ℝ≥0∞),
+    one_mul]
+
+/-- A finite second moment on a probability space forces a finite mean. -/
+theorem lintegral_le_rpow_lintegral_sq (mu : Measure Omega) [IsProbabilityMeasure mu]
+    {Z : Omega → ℝ≥0∞} (hZ : AEMeasurable Z mu) :
+    ∫⁻ omega, Z omega ∂mu ≤ (∫⁻ omega, Z omega ^ 2 ∂mu) ^ (1 / 2 : ℝ) := by
+  have h := setLIntegral_le_rpow_lintegral_sq_mul_rpow mu hZ MeasurableSet.univ
+  rwa [Measure.restrict_univ, measure_univ, ENNReal.one_rpow, mul_one] at h
+
+/-- **The Paley--Zygmund inequality**, in division-free form: on a probability space the mass of
+the event `{rho * E Z ≤ Z}` obeys
+`(1 - rho) ^ 2 * (E Z) ^ 2 ≤ E (Z ^ 2) * mu {rho * E Z ≤ Z}`.  The subtraction is the truncated one
+of `ℝ≥0∞`, so a level `rho ≥ 1` gives the trivial bound `0 ≤ …`. -/
+theorem lintegral_sq_mul_measure_ge_le (mu : Measure Omega) [IsProbabilityMeasure mu]
+    {Z : Omega → ℝ≥0∞} (hZ : Measurable Z) (hfin : ∫⁻ omega, Z omega ∂mu ≠ ⊤) (rho : ℝ≥0) :
+    ((1 : ℝ≥0∞) - rho) ^ 2 * (∫⁻ omega, Z omega ∂mu) ^ 2 ≤
+      (∫⁻ omega, Z omega ^ 2 ∂mu) *
+        mu {omega | (rho : ℝ≥0∞) * ∫⁻ omega, Z omega ∂mu ≤ Z omega} := by
+  set m : ℝ≥0∞ := ∫⁻ omega, Z omega ∂mu
+  set a : ℝ≥0∞ := (rho : ℝ≥0∞) * m with ha
+  set A : Set Omega := {omega | a ≤ Z omega}
+  have hA : MeasurableSet A := measurableSet_le measurable_const hZ
+  have hcompl : ∫⁻ omega in Aᶜ, Z omega ∂mu ≤ a := by
+    calc
+      ∫⁻ omega in Aᶜ, Z omega ∂mu ≤ ∫⁻ _omega in Aᶜ, a ∂mu := by
+        refine setLIntegral_mono' hA.compl fun omega homega ↦ ?_
+        exact le_of_lt (not_le.mp homega)
+      _ = a * mu Aᶜ := setLIntegral_const _ _
+      _ ≤ a * 1 := mul_le_mul_right prob_le_one a
+      _ = a := mul_one a
+  have hsum : m = ∫⁻ omega in A, Z omega ∂mu + ∫⁻ omega in Aᶜ, Z omega ∂mu :=
+    (lintegral_add_compl _ hA).symm
+  have hsub : m - a ≤ ∫⁻ omega in A, Z omega ∂mu := by
+    refine tsub_le_iff_right.mpr ?_
+    calc
+      m = ∫⁻ omega in A, Z omega ∂mu + ∫⁻ omega in Aᶜ, Z omega ∂mu := hsum
+      _ ≤ ∫⁻ omega in A, Z omega ∂mu + a := add_le_add le_rfl hcompl
+  have hlin : ((1 : ℝ≥0∞) - rho) * m = m - a := by
+    rw [ENNReal.sub_mul fun _ _ ↦ hfin, one_mul, ha]
+  have hCS := setLIntegral_le_rpow_lintegral_sq_mul_rpow mu hZ.aemeasurable hA
+  have hkey : ((1 : ℝ≥0∞) - rho) * m ≤
+      (∫⁻ omega, Z omega ^ 2 ∂mu) ^ (1 / 2 : ℝ) * (mu A) ^ (1 / 2 : ℝ) := by
+    rw [hlin]
+    exact hsub.trans hCS
+  calc
+    ((1 : ℝ≥0∞) - rho) ^ 2 * m ^ 2 = (((1 : ℝ≥0∞) - rho) * m) ^ 2 := (mul_pow _ _ 2).symm
+    _ ≤ ((∫⁻ omega, Z omega ^ 2 ∂mu) ^ (1 / 2 : ℝ) * (mu A) ^ (1 / 2 : ℝ)) ^ 2 :=
+      pow_le_pow_left' hkey 2
+    _ = (∫⁻ omega, Z omega ^ 2 ∂mu) * mu A := by
+      rw [mul_pow, ← ENNReal.rpow_natCast ((∫⁻ omega, Z omega ^ 2 ∂mu) ^ (1 / 2 : ℝ)) 2,
+        ← ENNReal.rpow_natCast ((mu A) ^ (1 / 2 : ℝ)) 2, ← ENNReal.rpow_mul, ← ENNReal.rpow_mul]
+      norm_num
+
+/-- **The Paley--Zygmund inequality**, in divided form.  The finite-mean hypothesis of the
+division-free version is supplied by the finite second moment. -/
+theorem le_measure_ge_of_lintegral_sq_ne_top (mu : Measure Omega) [IsProbabilityMeasure mu]
+    {Z : Omega → ℝ≥0∞} (hZ : Measurable Z) (hsq : ∫⁻ omega, Z omega ^ 2 ∂mu ≠ ⊤)
+    (rho : ℝ≥0) :
+    ((1 : ℝ≥0∞) - rho) ^ 2 * (∫⁻ omega, Z omega ∂mu) ^ 2 / (∫⁻ omega, Z omega ^ 2 ∂mu) ≤
+      mu {omega | (rho : ℝ≥0∞) * ∫⁻ omega, Z omega ∂mu ≤ Z omega} := by
+  have hfin : ∫⁻ omega, Z omega ∂mu ≠ ⊤ := by
+    refine ne_top_of_le_ne_top ?_ (lintegral_le_rpow_lintegral_sq mu hZ.aemeasurable)
+    exact ENNReal.rpow_ne_top_of_nonneg (by norm_num) hsq
+  exact ENNReal.div_le_of_le_mul
+    ((lintegral_sq_mul_measure_ge_le mu hZ hfin rho).trans_eq (mul_comm _ _))
+
+end MeasureTheory

LeanPool/MarkovProcess/MarkovProcess/Continuity.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Scott Armstrong. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong
+-/
+
+module
+
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.DenseTimeContinuousExtension
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.DenseTimeContinuousLaw
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.DenseTimeContinuousSupport
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.DyadicChaining
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.DyadicFloor
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.DyadicIncrements
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.DyadicPathChaining
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.GlobalDyadicFloorModification
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.KolmogorovDenseTimeContinuousSupport
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.KolmogorovTimeShift
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.PathModulus
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.PathTightness
+public import LeanPool.MarkovProcess.MarkovProcess.Continuity.ShiftedUnitModification
+
+
+/-!
+# Continuity
+
+Supporting modules for MarkovProcess.
+-/

LeanPool/MarkovProcess/MarkovProcess/Continuity/DenseTimeContinuousExtension.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2026 Scott Armstrong. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong
+-/
+module
+
+public import LeanPool.MarkovProcess.MarkovProcess.Path.Basic
+public import LeanPool.MarkovProcess.MarkovProcess.Time.CountableDenseTime
+public import Mathlib.MeasureTheory.Constructions.Polish.Basic
+
+
+/-!
+# Continuous extension from dense-time paths
+
+This file embeds ordinary continuous paths into paths on the fixed dense time carrier. It proves
+that the image is measurable and supplies a measurable total inverse. The inverse is the genuine
+continuous extension on the image and is arbitrarily equal to a caller-supplied default path away
+from the image.
+
+No probability law is shown to be supported on this image, and no continuous modification,
+stochastic-process association, or path-regularity claim is made here.
+-/
+
+@[expose] public section
+
+noncomputable section PortComputability
+
+open MeasureTheory Set
+
+namespace MarkovProcess
+
+section
+
+namespace ContinuousPath
+
+variable {alpha : Type*} [TopologicalSpace alpha]
+
+/-- Restriction of a continuous path to the fixed dense time carrier. -/
+def denseRestriction (omega : ContinuousPath alpha) : DenseTime → alpha :=
+  fun q ↦ omega (DenseTime.castOrderEmbedding q)
+
+@[simp]
+theorem denseRestriction_apply (omega : ContinuousPath alpha) (q : DenseTime) :
+    denseRestriction omega q = omega (DenseTime.castOrderEmbedding q) := rfl
+
+/-- The nonnegative rational times are dense in nonnegative real time. -/
+theorem denseRange_castOrderEmbedding : DenseRange DenseTime.castOrderEmbedding := by
+  rw [DenseRange]
+  apply dense_of_exists_between
+  intro a b hab
+  obtain ⟨q, haq, hqb⟩ := DenseTime.exists_cast_btwn hab
+  exact ⟨DenseTime.castOrderEmbedding q, ⟨q, rfl⟩, haq, hqb⟩
+
+/-- A continuous path is determined by its values at the dense times. -/
+theorem denseRestriction_injective [T2Space alpha] :
+    Function.Injective (denseRestriction (alpha := alpha)) := by
+  intro omega eta h
+  apply ContinuousMap.ext
+  have heq : (omega : NNReal → alpha) = eta :=
+    denseRange_castOrderEmbedding.equalizer omega.continuous eta.continuous h
+  exact congrFun heq
+
+/-- A total extension, equal to the inverse on the restriction range and arbitrarily equal to
+`default` away from that range. -/
+def continuousExtension (default : ContinuousPath alpha) :
+    (DenseTime → alpha) → ContinuousPath alpha :=
+  Function.extend denseRestriction id (fun _ ↦ default)
+
+@[simp]
+theorem continuousExtension_denseRestriction [T2Space alpha]
+    (default omega : ContinuousPath alpha) :
+    continuousExtension (alpha := alpha) default (denseRestriction omega) = omega := by
+  exact Function.Injective.extend_apply denseRestriction_injective _ _ _
+
+theorem denseRestriction_continuousExtension_of_mem_range [T2Space alpha]
+    (default : ContinuousPath alpha) {x : DenseTime → alpha}
+    (hx : x ∈ Set.range (denseRestriction (alpha := alpha))) :
+    denseRestriction (continuousExtension (alpha := alpha) default x) = x := by
+  obtain ⟨omega, rfl⟩ := hx
+  rw [continuousExtension_denseRestriction]
+
+@[simp]
+theorem continuousExtension_of_notMem_range (default : ContinuousPath alpha)
+    {x : DenseTime → alpha} (hx : x ∉ Set.range (denseRestriction (alpha := alpha))) :
+    continuousExtension (alpha := alpha) default x = default := by
+  exact Function.extend_apply' id (fun _ ↦ default) x hx
+
+section Measurable
+
+variable [MeasurableSpace alpha] [BorelSpace alpha]
+
+/-- Dense-time restriction is coordinatewise Borel measurable. -/
+theorem measurable_denseRestriction : Measurable (denseRestriction (alpha := alpha)) := by
+  rw [measurable_pi_iff]
+  intro q
+  exact
+    (continuous_eval (alpha := alpha) (DenseTime.castOrderEmbedding q)).borel_measurable.mono
+      le_rfl (le_of_eq BorelSpace.measurable_eq)
+
+variable [T2Space alpha] [StandardBorelSpace (ContinuousPath alpha)]
+  [MeasurableSpace.CountablySeparated (DenseTime → alpha)]
+
+/-- Dense-time restriction is a measurable embedding. -/
+theorem measurableEmbedding_denseRestriction :
+    MeasurableEmbedding (denseRestriction (alpha := alpha)) :=
+  measurable_denseRestriction.measurableEmbedding denseRestriction_injective
+
+/-- The set of dense-time paths admitting a continuous extension is measurable. -/
+theorem measurableSet_range_denseRestriction :
+    MeasurableSet (Set.range (denseRestriction (alpha := alpha))) :=
+  measurableEmbedding_denseRestriction.measurableSet_range
+
+/-- The total extension is measurable; away from the measurable restriction range its value is
+the arbitrary path `default`. -/
+theorem measurable_continuousExtension (default : ContinuousPath alpha) :
+    Measurable (continuousExtension (alpha := alpha) default) :=
+  measurableEmbedding_denseRestriction.measurable_extend measurable_id measurable_const
+
+end Measurable
+end ContinuousPath
+end
+end MarkovProcess
+
+end PortComputability