Theorems · Definition · probability

ProbabilityTheory.Kernel.piecewise

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {s : Set α} →
          [DecidablePred fun x => x ∈ s] →
            MeasurableSet s → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α β

ProbabilityTheory.Kernel.piecewise hs κ η is the kernel equal to κ on the measurable set s and to η on its complement.

Defined in

Mathlib.Probability.Kernel.Basic

Cited by

10 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePred