Tests.FellerSemigroup

- 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 77184245109a

Excerpt truncated; the exact source link is authoritative.