AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovMeasureEvolution

- Evolve a measure by the transition kernel at elapsed time `t`.

noncomputable def evolveMeasure
    {K : ℝ≥0 → Kernel E E} (_hK : TransitionKernelContract K)
    (t : ℝ≥0) (mu : Measure E) : Measure E :=
  K t ∘ₘ mu

/-- Measure-level Chapman--Kolmogorov: evolving for `s+t` is the same as
first evolving for `s` and then for `t`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:31published source at 0e31a3cda412

- Measure-level Chapman--Kolmogorov: evolving for `s+t` is the same as first evolving for `s` and then for `t`.

theorem evolveMeasure_add
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (mu : Measure E) (s t : ℝ≥0) :
    evolveMeasure hK (s + t) mu =
      evolveMeasure hK t (evolveMeasure hK s mu) := by
  change K (s + t) ∘ₘ mu = K t ∘ₘ (K s ∘ₘ mu)
  rw [hK.chapmanKolmogorov s t]
  exact (Measure.comp_assoc
    (μ := mu) (κ := K s) (η := K t)).symm

/-- A Markov kernel sends a probability law to a probability law. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:38published source at 0e31a3cda412

- A Markov kernel sends a probability law to a probability law.

theorem isProbabilityMeasure_evolveMeasure
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (mu : Measure E) [IsProbabilityMeasure mu] (t : ℝ≥0) :
    IsProbabilityMeasure (evolveMeasure hK t mu) := by
  letI : IsMarkovKernel (K t) := hK.isMarkov t
  dsimp [evolveMeasure]
  infer_instance

/-- Integrating a Markov observable against the input law is the same as
integrating the original observable against the evolved law.

This is the measure/operator compatibility identity behind the usual formula
`∫ P_t f dμ = ∫ f d(μ P_t)`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:49published source at 0e31a3cda412

- Integrating a Markov observable against the input law is the same as integrating the original observable against the evolved law. This is the measure/operator compatibility identity behind the usual formula `∫ P_t f dμ = ∫ f d(μ P_t)`.

theorem lintegral_markovOperator_eq_lintegral_evolveMeasure
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (mu : Measure E) (t : ℝ≥0) (f : MeasurableENNReal E) :
    (∫⁻ x, markovOperator hK t f x ∂mu) =
      ∫⁻ y, f y ∂evolveMeasure hK t mu := by
  change (∫⁻ x, (∫⁻ y, f y ∂K t x) ∂mu) =
    ∫⁻ y, f y ∂(mu.bind (K t))
  rw [Measure.lintegral_bind (K t).aemeasurable f.2.aemeasurable]

/-- A measure is stationary for a transition-kernel semigroup when it is fixed
by every nonnegative-time law evolution.

This is the direct measure-level notion used in Chewi Proposition 1.2.7. The
generator characterization `∫ L f dπ = 0` needs a semigroup-stable generator
domain and is intentionally a separate theorem. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:62published source at 0e31a3cda412

- A measure is stationary for a transition-kernel semigroup when it is fixed by every nonnegative-time law evolution. This is the direct measure-level notion used in Chewi Proposition 1.2.7. The generator characterization `∫ L f dπ = 0` needs a semigroup-stable generator domain and is intentionally a separate theorem.

def IsStationary
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (pi : Measure E) : Prop :=
  ∀ t : ℝ≥0, evolveMeasure hK t pi = pi

/-- Unfold the stationary-measure predicate. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:77published source at 0e31a3cda412

- Unfold the stationary-measure predicate.

theorem isStationary_iff
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (pi : Measure E) :
    IsStationary hK pi ↔ ∀ t : ℝ≥0, evolveMeasure hK t pi = pi :=
  Iff.rfl

/-- ASTIS semigroup stationarity is exactly Mathlib kernel invariance at every
time. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:83published source at 0e31a3cda412

- ASTIS semigroup stationarity is exactly Mathlib kernel invariance at every time.

theorem isStationary_iff_kernel_invariant
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (pi : Measure E) :
    IsStationary hK pi ↔ ∀ t : ℝ≥0, Kernel.Invariant (K t) pi := by
  constructor
  · intro hpi t
    change K t ∘ₘ pi = pi
    exact hpi t
  · intro hpi t
    change K t ∘ₘ pi = pi
    exact (hpi t).def

/-- Detailed balance for every transition kernel implies stationarity of the
whole semigroup. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:91published source at 0e31a3cda412

- Detailed balance for every transition kernel implies stationarity of the whole semigroup.

theorem isStationary_of_kernel_reversible
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (pi : Measure E)
    (hrev : ∀ t : ℝ≥0, Kernel.IsReversible (K t) pi) :
    IsStationary hK pi := by
  rw [isStationary_iff_kernel_invariant]
  intro t
  letI : IsMarkovKernel (K t) := hK.isMarkov t
  exact (hrev t).invariant

/-- Stationarity implies invariance of every measurable nonnegative expectation
under the Markov operator. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:105published source at 0e31a3cda412

- Stationarity implies invariance of every measurable nonnegative expectation under the Markov operator.

theorem IsStationary.lintegral_markovOperator_eq
    {K : ℝ≥0 → Kernel E E} {hK : TransitionKernelContract K}
    {pi : Measure E} (hpi : IsStationary hK pi)
    (t : ℝ≥0) (f : MeasurableENNReal E) :
    (∫⁻ x, markovOperator hK t f x ∂pi) = ∫⁻ x, f x ∂pi := by
  rw [lintegral_markovOperator_eq_lintegral_evolveMeasure hK pi t f, hpi t]

/-- Conversely, invariance of all measurable nonnegative expectations under
every Markov operator determines the stationary measure. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:117published source at 0e31a3cda412

- Conversely, invariance of all measurable nonnegative expectations under every Markov operator determines the stationary measure.

theorem isStationary_of_lintegral_markovOperator_eq
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (pi : Measure E)
    (hinv : ∀ (t : ℝ≥0) (f : MeasurableENNReal E),
      (∫⁻ x, markovOperator hK t f x ∂pi) = ∫⁻ x, f x ∂pi) :
    IsStationary hK pi := by
  intro t
  ext s hs
  let f : MeasurableENNReal E :=
    ⟨s.indicator (fun _ => (1 : ℝ≥0∞)), measurable_const.indicator hs⟩
  have h := hinv t f
  rw [lintegral_markovOperator_eq_lintegral_evolveMeasure hK pi t f] at h
  simpa [f, hs] using h

/-- Measure stationarity is equivalent to expectation invariance for all
measurable nonnegative observables. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:126published source at 0e31a3cda412

- Measure stationarity is equivalent to expectation invariance for all measurable nonnegative observables.

theorem isStationary_iff_lintegral_markovOperator_eq
    {K : ℝ≥0 → Kernel E E} (hK : TransitionKernelContract K)
    (pi : Measure E) :
    IsStationary hK pi ↔
      ∀ (t : ℝ≥0) (f : MeasurableENNReal E),
        (∫⁻ x, markovOperator hK t f x ∂pi) = ∫⁻ x, f x ∂pi := by
  constructor
  · intro hpi t f
    exact hpi.lintegral_markovOperator_eq t f
  · exact isStationary_of_lintegral_markovOperator_eq hK pi

/-- A stationary law remains unchanged at every named time. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:142published source at 0e31a3cda412

- A stationary law remains unchanged at every named time.

theorem IsStationary.evolveMeasure_eq
    {K : ℝ≥0 → Kernel E E} {hK : TransitionKernelContract K}
    {pi : Measure E} (hpi : IsStationary hK pi) (t : ℝ≥0) :
    evolveMeasure hK t pi = pi :=
  hpi t

/-- Stationarity is preserved after any elapsed time. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:154published source at 0e31a3cda412

- Stationarity is preserved after any elapsed time.

theorem IsStationary.after
    {K : ℝ≥0 → Kernel E E} {hK : TransitionKernelContract K}
    {pi : Measure E} (hpi : IsStationary hK pi) (s : ℝ≥0) :
    IsStationary hK (evolveMeasure hK s pi) := by
  rw [hpi s]
  exact hpi

end

end MarkovSemigroup
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean:161published source at 0e31a3cda412