AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StationarityEquivalence

- Chewi Proposition 1.2.7, invariant-to-infinitesimal direction: `ell(P_t f) = ell(f)` for all `t >= 0` implies `ell(Af) = 0` on the right-generator domain.

theorem chewi_proposition_1_2_7_invariant_implies_generator_zero
    (S : ContinuousLinearSemigroup M)
    (ell : M →L[ℝ] ℝ)
    (hinv : ∀ (t : ℝ≥0) (f : M), ell (S.op t f) = ell f)
    (f : generatorDomainSubmodule S) :
    ell (rightGenerator S f) = 0 :=
  GeneratorStationarity.invariantFunctional_rightGenerator_eq_zero S ell hinv f

/-- Chewi Proposition 1.2.7, infinitesimal-to-invariant direction on an
explicit generator domain.

The integrated-generator contract is precisely the analytic input needed to
turn `∫ Lf dμ = 0` into `∫ P_t f dμ = ∫ f dμ`; it contains orbit-domain
preservation and the right derivative of the semigroup pairing, rather than
assuming stationarity itself. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StationarityEquivalence.lean:34published source at 0e31a3cda412

- Chewi Proposition 1.2.7, infinitesimal-to-invariant direction on an explicit generator domain. The integrated-generator contract is precisely the analytic input needed to turn `∫ Lf dμ = 0` into `∫ P_t f dμ = ∫ f dμ`; it contains orbit-domain preservation and the right derivative of the semigroup pairing, rather than assuming stationarity itself.

theorem chewi_proposition_1_2_7_generator_zero_implies_invariant
    {E : Type*} [MeasurableSpace E]
    {P : ℝ → (E → ℝ) → E → ℝ}
    {generator : (E → ℝ) → E → ℝ}
    {domain : Set (E → ℝ)} {μ : Measure E}
    (hsemigroup :
      WeakGenerator.IntegratedSemigroupGeneratorContract P generator domain μ)
    (hzero : ∀ f ∈ domain, ∫ x, generator f x ∂μ = 0) :
    WeakGenerator.IsInvariantOn P μ domain :=
  WeakGenerator.isInvariantOn_of_integral_generator_eq_zero hsemigroup hzero

end

end StationarityEquivalence
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

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