test module

`Tests.FellerGeneratorBridge`

0 named declarations scanned from Tests/FellerGeneratorBridge.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/FellerGeneratorBridge.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge

namespace AutoSamplingTheory.Tests.FellerGeneratorBridge

open MeasureTheory ProbabilityTheory
open scoped NNReal ProbabilityTheory BoundedContinuousFunction

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridge

noncomputable section

#check fellerOperator_const
#check continuousLinearSemigroupOfFeller_op_const
#check hasRightGeneratorAt_const
#check const_mem_generatorDomainSubmodule

example {E : Type*} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E]
    {K : ℝ≥0 → Kernel E E} (hK : FellerTransitionKernelContract K)
    (t : ℝ≥0) (c : ℝ) :
    fellerOperator hK t (BoundedContinuousFunction.const E c) =
      BoundedContinuousFunction.const E c :=
  fellerOperator_const hK t c

example {E : Type*} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E]
    {K : ℝ≥0 → Kernel E E} (hK : FellerTransitionKernelContract K)
    (c : ℝ) :
    HasRightGeneratorAt (continuousLinearSemigroupOfFeller hK)
      (BoundedContinuousFunction.const E c) 0 :=
  hasRightGeneratorAt_const hK c

end

end AutoSamplingTheory.Tests.FellerGeneratorBridge