AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GeneratorStationarity

- A vector fixed by the entire semigroup has right-generator value zero.

theorem hasRightGeneratorAt_zero_of_fixed
    (S : ContinuousLinearSemigroup M)
    {f : M}
    (hfix : ∀ t : ℝ≥0, S.op t f = f) :
    HasRightGeneratorAt S f 0 := by
  unfold HasRightGeneratorAt rightDifferenceQuotient
  simp [hfix]

/-- Consequently a fixed vector belongs to the canonical generator domain. -/

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

- Consequently a fixed vector belongs to the canonical generator domain.

theorem mem_generatorDomainSubmodule_of_fixed
    (S : ContinuousLinearSemigroup M)
    {f : M}
    (hfix : ∀ t : ℝ≥0, S.op t f = f) :
    f ∈ generatorDomainSubmodule S :=
  ⟨0, hasRightGeneratorAt_zero_of_fixed S hfix⟩

/-- An invariant continuous linear functional annihilates every right-generator
value.

This is the abstract infinitesimal-stationarity argument: apply the functional
to the semigroup difference quotient. Invariance makes every quotient equal
to zero, while continuity of the functional transports the generator limit. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GeneratorStationarity.lean:47published source at 0e31a3cda412

- An invariant continuous linear functional annihilates every right-generator value. This is the abstract infinitesimal-stationarity argument: apply the functional to the semigroup difference quotient. Invariance makes every quotient equal to zero, while continuity of the functional transports the generator limit.

theorem invariantFunctional_generator_eq_zero
    (S : ContinuousLinearSemigroup M)
    (ell : M →L[ℝ] ℝ)
    (hinv : ∀ (t : ℝ≥0) (f : M), ell (S.op t f) = ell f)
    {f Af : M}
    (hf : HasRightGeneratorAt S f Af) :
    ell Af = 0 := by
  have hell : Tendsto ell (𝓝 Af) (𝓝 (ell Af)) :=
    ell.continuous.continuousAt
  have hmap :
      Tendsto
        (fun h : ℝ≥0 => ell (rightDifferenceQuotient S h f))
        (nhdsWithin 0 (Ioi 0)) (𝓝 (ell Af)) :=
    hell.comp hf
  have hzero : ∀ h : ℝ≥0,
      ell (rightDifferenceQuotient S h f) = 0 := by
    intro h
    simp [rightDifferenceQuotient, hinv h f]
  have hzeroLimit :
      Tendsto
        (fun h : ℝ≥0 => ell (rightDifferenceQuotient S h f))
        (nhdsWithin 0 (Ioi 0)) (𝓝 (0 : ℝ)) := by
    simpa only [hzero] using
      (tendsto_const_nhds :
        Tendsto (fun _ : ℝ≥0 => (0 : ℝ))
          (nhdsWithin 0 (Ioi 0)) (𝓝 0))
  exact tendsto_nhds_unique hmap hzeroLimit

/-- Bundled generator-domain form of infinitesimal stationarity. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GeneratorStationarity.lean:60published source at 0e31a3cda412

- Bundled generator-domain form of infinitesimal stationarity.

theorem invariantFunctional_rightGenerator_eq_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 :=
  invariantFunctional_generator_eq_zero S ell hinv
    (rightGeneratorValue_spec S f)

end

end GeneratorStationarity
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GeneratorStationarity.lean:89published source at 0e31a3cda412