AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup

- A time-homogeneous Markov transition-kernel contract at nonnegative times. `chapmanKolmogorov` is oriented so that first evolving for time `s` and then for time `t` is the kernel composition `K t ∘ₖ K s`. The contract is the kernel-level consequence of the Markov property used by Chewi's Lemma 1.2.2; it does not assume any continuity or generator-domain statement.

structure TransitionKernelContract (K : ℝ≥0 → Kernel E E) : Prop where
  isMarkov : ∀ t, IsMarkovKernel (K t)
  initial : K 0 = Kernel.id
  chapmanKolmogorov : ∀ s t, K (s + t) = K t ∘ₖ K s

/-- The measurable nonnegative observables on a measurable state space. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:37published source at 77184245109a

- The measurable nonnegative observables on a measurable state space.

def MeasurableENNReal (E : Type*) [MeasurableSpace E] :=
  {f : E → ℝ≥0∞ // Measurable f}

instance : CoeFun (MeasurableENNReal E) (fun _ => E → ℝ≥0∞) :=
  ⟨fun f => f.1⟩

/-- A constant measurable nonnegative observable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:43published source at 77184245109a

- A constant measurable nonnegative observable.

def MeasurableENNReal.const (c : ℝ≥0∞) : MeasurableENNReal E :=
  ⟨fun _ => c, measurable_const⟩

/-- The Markov operator induced by a transition-kernel contract. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:50published source at 77184245109a

- The Markov operator induced by a transition-kernel contract.

def markovOperator {K : ℝ≥0 → Kernel E E}
    (_hK : TransitionKernelContract K) (t : ℝ≥0) :
    MeasurableENNReal E → MeasurableENNReal E :=
  fun f => by
    exact ⟨fun x => ∫⁻ y, f y ∂K t x, f.2.lintegral_kernel⟩

/-- A Markov operator preserves constant nonnegative observables. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:54published source at 77184245109aOpen detailed card

- A Markov operator preserves constant nonnegative observables.

theorem markovOperator_const {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) (t : ℝ≥0) (c : ℝ≥0∞) :
    markovOperator hK t (MeasurableENNReal.const c) =
      MeasurableENNReal.const c := by
  apply Subtype.ext
  funext x
  change (∫⁻ _y, c ∂K t x) = c
  let : IsMarkovKernel (K t) := hK.isMarkov t
  simp

/-- Markov integration is monotone in the observable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:61published source at 77184245109aOpen detailed card

- Markov integration is monotone in the observable.

theorem markovOperator_apply_mono {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) (t : ℝ≥0)
    {f g : MeasurableENNReal E} (hfg : ∀ y, f y ≤ g y) (x : E) :
    markovOperator hK t f x ≤ markovOperator hK t g x := by
  change (∫⁻ y, f y ∂K t x) ≤ ∫⁻ y, g y ∂K t x
  exact lintegral_mono hfg

/-- At time zero, the transition-kernel Markov operator is the identity. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:72published source at 77184245109aOpen detailed card

- At time zero, the transition-kernel Markov operator is the identity.

theorem markovOperator_zero {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) :
    markovOperator hK 0 = id := by
  funext f
  apply Subtype.ext
  funext x
  change (∫⁻ y, f y ∂K 0 x) = f x
  rw [hK.initial]
  exact Kernel.lintegral_id' f.2 x

/-- Chapman--Kolmogorov becomes composition of Markov operators. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:80published source at 77184245109a

- Chapman--Kolmogorov becomes composition of Markov operators.

theorem markovOperator_comp {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) (s t : ℝ≥0) :
    markovOperator hK s ∘ markovOperator hK t =
      markovOperator hK (s + t) := by
  funext f
  apply Subtype.ext
  funext x
  change
    (∫⁻ y, (∫⁻ z, f z ∂K t y) ∂K s x) =
      ∫⁻ z, f z ∂K (s + t) x
  rw [hK.chapmanKolmogorov s t]
  exact (Kernel.lintegral_comp (K t) (K s) x f.2).symm

/-- Time-homogeneous Markov operators commute because nonnegative-time
addition is commutative. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:91published source at 77184245109a

- Time-homogeneous Markov operators commute because nonnegative-time addition is commutative.

theorem markovOperator_comm {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) (s t : ℝ≥0) :
    markovOperator hK s ∘ markovOperator hK t =
      markovOperator hK t ∘ markovOperator hK s := by
  calc
    markovOperator hK s ∘ markovOperator hK t =
        markovOperator hK (s + t) := markovOperator_comp hK s t
    _ = markovOperator hK (t + s) := by rw [add_comm]
    _ = markovOperator hK t ∘ markovOperator hK s :=
      (markovOperator_comp hK t s).symm

/-- Chewi, Lemma 1.2.2: the zero-time and two-time Markov-operator laws,
under the explicit transition-kernel contract. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:106published source at 77184245109a

- Chewi, Lemma 1.2.2: the zero-time and two-time Markov-operator laws, under the explicit transition-kernel contract.

theorem chewi_lemma_1_2_2 {K : ℝ≥0 → Kernel E E}
    (hK : TransitionKernelContract K) :
    markovOperator hK 0 = id ∧
      ∀ s t : ℝ≥0,
        markovOperator hK s ∘ markovOperator hK t =
            markovOperator hK (s + t) ∧
          markovOperator hK t ∘ markovOperator hK s =
            markovOperator hK (s + t) := by
  constructor
  · exact markovOperator_zero hK
  · intro s t
    constructor
    · exact markovOperator_comp hK s t
    · simpa [add_comm] using markovOperator_comp hK t s

end

end MarkovSemigroup
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean:119published source at 77184245109aOpen detailed card