test module
Tests.FellerSemigroup
1 named declarations scanned from Tests/FellerSemigroup.lean.
Declarations
theorem AutoSamplingTheory.Tests.FellerSemigroup.identityFellerContract Partial Not mapped
- The identity transition kernel is the basic Feller semigroup.
theorem identityFellerContract :
FellerTransitionKernelContract
(fun _ : ℝ≥0 => (Kernel.id : Kernel E E)) where
isMarkov := by
intro t
infer_instance
initial := rfl
chapmanKolmogorov := by
intro s t
simp
mapsContinuous := by
intro t f
have hfun :
(fun x => ∫ y, f y ∂(Kernel.id : Kernel E E) x) =
fun x => f x := by
funext x
rw [Kernel.id_apply]
exact integral_dirac' f x f.continuous.stronglyMeasurable
rw [hfun]
exact f.continuous
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) (t : ℝ≥0)
(f : E →ᵇ ℝ) (x : E) :
fellerOperator hK t f x = ∫ y, f y ∂K t x :=
fellerOperator_apply hK t f x
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) (t : ℝ≥0)
(f : E →ᵇ ℝ) :
‖fellerOperator hK t f‖ ≤ ‖f‖ :=
norm_fellerOperator_apply_le hK t f
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) (t : ℝ≥0)
(f : E →ᵇ ℝ) (x : E) :
(fellerOperator hK t f x) ^ 2 ≤
fellerOperator hK t (f * f) x :=
sq_fellerOperator_apply_le hK t f x
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) :
fellerOperator hK 0 = ContinuousLinearMap.id ℝ (E →ᵇ ℝ) :=
fellerOperator_zero hK
-- Source excerpt truncated; follow the exact source link.Tests/FellerSemigroup.lean:17published source at ed709a7f320d
Excerpt truncated; the exact source link is authoritative.
Complete Lean source
Tests/FellerSemigroup.lean — full module with imports and context
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup
namespace AutoSamplingTheory.Tests.FellerSemigroup
open MeasureTheory ProbabilityTheory
open scoped NNReal ProbabilityTheory BoundedContinuousFunction
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup
noncomputable section
variable {E : Type*} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E]
/-- The identity transition kernel is the basic Feller semigroup. -/
theorem identityFellerContract :
FellerTransitionKernelContract
(fun _ : ℝ≥0 => (Kernel.id : Kernel E E)) where
isMarkov := by
intro t
infer_instance
initial := rfl
chapmanKolmogorov := by
intro s t
simp
mapsContinuous := by
intro t f
have hfun :
(fun x => ∫ y, f y ∂(Kernel.id : Kernel E E) x) =
fun x => f x := by
funext x
rw [Kernel.id_apply]
exact integral_dirac' f x f.continuous.stronglyMeasurable
rw [hfun]
exact f.continuous
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) (t : ℝ≥0)
(f : E →ᵇ ℝ) (x : E) :
fellerOperator hK t f x = ∫ y, f y ∂K t x :=
fellerOperator_apply hK t f x
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) (t : ℝ≥0)
(f : E →ᵇ ℝ) :
‖fellerOperator hK t f‖ ≤ ‖f‖ :=
norm_fellerOperator_apply_le hK t f
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) (t : ℝ≥0)
(f : E →ᵇ ℝ) (x : E) :
(fellerOperator hK t f x) ^ 2 ≤
fellerOperator hK t (f * f) x :=
sq_fellerOperator_apply_le hK t f x
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) :
fellerOperator hK 0 = ContinuousLinearMap.id ℝ (E →ᵇ ℝ) :=
fellerOperator_zero hK
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) (s t : ℝ≥0) :
fellerOperator hK (s + t) =
(fellerOperator hK s).comp (fellerOperator hK t) :=
fellerOperator_add hK s t
example {K : ℝ≥0 → Kernel E E}
(hK : FellerTransitionKernelContract K) :
ContinuousLinearSemigroup (E →ᵇ ℝ) :=
continuousLinearSemigroupOfFeller hK
example (t : ℝ≥0) (f : E →ᵇ ℝ) :
fellerOperator
(identityFellerContract : FellerTransitionKernelContract
(fun _ : ℝ≥0 => (Kernel.id : Kernel E E))) t f = f := by
ext x
change (∫ y, f y ∂(Kernel.id : Kernel E E) x) = f x
rw [Kernel.id_apply]
exact integral_dirac' f x f.continuous.stronglyMeasurable
example (t : ℝ≥0) (f : E →ᵇ ℝ) (x : E) :
(fellerOperator identityFellerContract t f x) ^ 2 =
fellerOperator identityFellerContract t (f * f) x := by
simp only [fellerOperator_apply, Kernel.id_apply]
rw [integral_dirac' f x f.continuous.stronglyMeasurable]
rw [integral_dirac' (f * f) x (f * f).continuous.stronglyMeasurable]
simp [pow_two]
end
end AutoSamplingTheory.Tests.FellerSemigroup