production module

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge`

4 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerGeneratorBridge.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroupAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GeneratorStationarity

Imported by

Tests.FellerGeneratorBridge

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge.fellerOperator_const Partial Not mapped

No declaration docstring.

theorem fellerOperator_const
    {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K)
    (t : ℝ≥0) (c : ℝ) :
    fellerOperator hK t (BoundedContinuousFunction.const E c) =
      BoundedContinuousFunction.const E c := by
  letI : IsMarkovKernel (K t) := hK.toTransitionKernelContract.isMarkov t
  ext x
  change (∫ _y, c ∂K t x) = c
  simp

/-- The continuous-linear semigroup induced by a Feller kernel fixes every
constant observable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerGeneratorBridge.lean:33published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge.continuousLinearSemigroupOfFeller_op_const Partial Not mapped

- The continuous-linear semigroup induced by a Feller kernel fixes every constant observable.

theorem continuousLinearSemigroupOfFeller_op_const
    {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K)
    (t : ℝ≥0) (c : ℝ) :
    (continuousLinearSemigroupOfFeller hK).op t
        (BoundedContinuousFunction.const E c) =
      BoundedContinuousFunction.const E c :=
  fellerOperator_const hK t c

/-- Every constant bounded continuous observable has right-generator value
zero for the Feller continuous-linear semigroup. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerGeneratorBridge.lean:46published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge.hasRightGeneratorAt_const Partial Not mapped

- Every constant bounded continuous observable has right-generator value zero for the Feller continuous-linear semigroup.

theorem hasRightGeneratorAt_const
    {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K)
    (c : ℝ) :
    HasRightGeneratorAt (continuousLinearSemigroupOfFeller hK)
      (BoundedContinuousFunction.const E c) 0 :=
  hasRightGeneratorAt_zero_of_fixed
    (continuousLinearSemigroupOfFeller hK)
    (fun t => continuousLinearSemigroupOfFeller_op_const hK t c)

/-- Constants belong to the canonical Feller generator domain. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerGeneratorBridge.lean:57published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge.const_mem_generatorDomainSubmodule Partial Not mapped

- Constants belong to the canonical Feller generator domain.

theorem const_mem_generatorDomainSubmodule
    {K : ℝ≥0 → Kernel E E}
    (hK : FellerTransitionKernelContract K)
    (c : ℝ) :
    BoundedContinuousFunction.const E c ∈
      generatorDomainSubmodule (continuousLinearSemigroupOfFeller hK) :=
  mem_generatorDomainSubmodule_of_fixed
    (continuousLinearSemigroupOfFeller hK)
    (fun t => continuousLinearSemigroupOfFeller_op_const hK t c)

end

end FellerGeneratorBridge
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerGeneratorBridge.lean:68published source at 0e31a3cda412