Documentation

Mathlib.Probability.Kernel.Basic

Markov Kernels #

A kernel from a measurable space α to another measurable space β is a measurable map α → MeasureTheory.Measure β, where the measurable space instance on measure β is the one defined in MeasureTheory.Measure.instMeasurableSpace. That is, a kernel κ verifies that for all measurable sets s of β, a ↦ κ a s is measurable.

Main definitions #

Classes of kernels:

Particular kernels:

Main statements #

structure ProbabilityTheory.Kernel (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] :
Type (max u_1 u_2)

A kernel from a measurable space α to another measurable space β is a measurable function κ : α → Measure β. The measurable space structure on MeasureTheory.Measure β is given by MeasureTheory.Measure.instMeasurableSpace. A map κ : α → MeasureTheory.Measure β is measurable iff ∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s).

  • toFun : αMeasureTheory.Measure β

    The underlying function of a kernel.

    Do not use this function directly. Instead use the coercion coming from the DFunLike instance.

  • measurable' : Measurable self.toFun

    A kernel is a measurable map.

    Do not use this lemma directly. Use Kernel.measurable instead.

Instances For
    theorem ProbabilityTheory.Kernel.measurable' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (self : ProbabilityTheory.Kernel α β) :
    Measurable self.toFun

    A kernel is a measurable map.

    Do not use this lemma directly. Use Kernel.measurable instead.

    @[deprecated ProbabilityTheory.Kernel]
    def ProbabilityTheory.kernel (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] :
    Type (max u_1 u_2)

    Alias of ProbabilityTheory.Kernel.


    A kernel from a measurable space α to another measurable space β is a measurable function κ : α → Measure β. The measurable space structure on MeasureTheory.Measure β is given by MeasureTheory.Measure.instMeasurableSpace. A map κ : α → MeasureTheory.Measure β is measurable iff ∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s).

    Equations
    Instances For
      Equations
      • ProbabilityTheory.Kernel.instFunLike = { coe := ProbabilityTheory.Kernel.toFun, coe_injective' := }
      theorem ProbabilityTheory.Kernel.measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :
      instance ProbabilityTheory.Kernel.instZero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
      Equations
      • ProbabilityTheory.Kernel.instZero = { zero := { toFun := 0, measurable' := } }
      noncomputable instance ProbabilityTheory.Kernel.instAdd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
      Equations
      • ProbabilityTheory.Kernel.instAdd = { add := fun (κ η : ProbabilityTheory.Kernel α β) => { toFun := κ + η, measurable' := } }
      noncomputable instance ProbabilityTheory.Kernel.instSMulNat {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
      Equations
      @[simp]
      theorem ProbabilityTheory.Kernel.coe_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
      0 = 0
      @[simp]
      theorem ProbabilityTheory.Kernel.coe_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) :
      (κ + η) = κ + η
      @[simp]
      theorem ProbabilityTheory.Kernel.coe_nsmul {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (n : ) (κ : ProbabilityTheory.Kernel α β) :
      (n κ) = n κ
      @[simp]
      theorem ProbabilityTheory.Kernel.zero_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (a : α) :
      0 a = 0
      @[simp]
      theorem ProbabilityTheory.Kernel.add_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) (a : α) :
      (κ + η) a = κ a + η a
      @[simp]
      theorem ProbabilityTheory.Kernel.nsmul_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (n : ) (κ : ProbabilityTheory.Kernel α β) (a : α) :
      (n κ) a = n κ a
      noncomputable instance ProbabilityTheory.Kernel.instAddCommMonoid {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
      Equations
      Equations
      Equations
      • =
      Equations

      Coercion to a function as an additive monoid homomorphism.

      Equations
      Instances For
        @[simp]
        theorem ProbabilityTheory.Kernel.coe_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ιProbabilityTheory.Kernel α β) :
        (iI, κ i) = iI, (κ i)
        theorem ProbabilityTheory.Kernel.finset_sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ιProbabilityTheory.Kernel α β) (a : α) :
        (iI, κ i) a = iI, (κ i) a
        theorem ProbabilityTheory.Kernel.finset_sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι) (κ : ιProbabilityTheory.Kernel α β) (a : α) (s : Set β) :
        ((iI, κ i) a) s = iI, ((κ i) a) s
        class ProbabilityTheory.IsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :

        A kernel is a Markov kernel if every measure in its image is a probability measure.

        Instances
          class ProbabilityTheory.IsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :

          A kernel is finite if every measure in its image is finite, with a uniform bound.

          • exists_univ_le : C < , ∀ (a : α), (κ a) Set.univ C
          Instances
            theorem ProbabilityTheory.IsFiniteKernel.exists_univ_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [self : ProbabilityTheory.IsFiniteKernel κ] :
            C < , ∀ (a : α), (κ a) Set.univ C

            A constant C : ℝ≥0∞ such that C < ∞ (ProbabilityTheory.IsFiniteKernel.bound_lt_top κ) and for all a : α and s : Set β, κ a s ≤ C (ProbabilityTheory.Kernel.measure_le_bound κ a s).

            Porting note (#11215): TODO: does it make sense to -- make ProbabilityTheory.IsFiniteKernel.bound the least possible bound? -- Should it be an NNReal number?

            Equations
            Instances For
              Equations
              • =
              theorem ProbabilityTheory.Kernel.ext {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} (h : ∀ (a : α), κ a = η a) :
              κ = η
              theorem ProbabilityTheory.Kernel.ext_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} :
              κ = η ∀ (a : α), κ a = η a
              theorem ProbabilityTheory.Kernel.ext_iff' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} :
              κ = η ∀ (a : α) (s : Set β), MeasurableSet s(κ a) s = (η a) s
              theorem ProbabilityTheory.Kernel.ext_fun {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} (h : ∀ (a : α) (f : βENNReal), Measurable f∫⁻ (b : β), f bκ a = ∫⁻ (b : β), f bη a) :
              κ = η
              theorem ProbabilityTheory.Kernel.ext_fun_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} :
              κ = η ∀ (a : α) (f : βENNReal), Measurable f∫⁻ (b : β), f bκ a = ∫⁻ (b : β), f bη a
              theorem ProbabilityTheory.Kernel.measurable_coe {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) {s : Set β} (hs : MeasurableSet s) :
              Measurable fun (a : α) => (κ a) s
              theorem ProbabilityTheory.Kernel.apply_congr_of_mem_measurableAtom {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) {y' : α} {y : α} (hy' : y' measurableAtom y) :
              κ y' = κ y
              noncomputable def ProbabilityTheory.Kernel.sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ιProbabilityTheory.Kernel α β) :

              Sum of an indexed family of kernels.

              Equations
              Instances For
                theorem ProbabilityTheory.Kernel.sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ιProbabilityTheory.Kernel α β) (a : α) :
                theorem ProbabilityTheory.Kernel.sum_apply' {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ιProbabilityTheory.Kernel α β) (a : α) {s : Set β} (hs : MeasurableSet s) :
                ((ProbabilityTheory.Kernel.sum κ) a) s = ∑' (n : ι), ((κ n) a) s
                @[simp]
                theorem ProbabilityTheory.Kernel.sum_zero {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] :
                (ProbabilityTheory.Kernel.sum fun (x : ι) => 0) = 0
                theorem ProbabilityTheory.Kernel.sum_comm {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ιιProbabilityTheory.Kernel α β) :
                @[simp]
                theorem ProbabilityTheory.Kernel.sum_fintype {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Fintype ι] (κ : ιProbabilityTheory.Kernel α β) :
                ProbabilityTheory.Kernel.sum κ = i : ι, κ i
                theorem ProbabilityTheory.Kernel.sum_add {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ιProbabilityTheory.Kernel α β) (η : ιProbabilityTheory.Kernel α β) :
                class ProbabilityTheory.IsSFiniteKernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :

                A kernel is s-finite if it can be written as the sum of countably many finite kernels.

                Instances
                  noncomputable def ProbabilityTheory.Kernel.seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [h : ProbabilityTheory.IsSFiniteKernel κ] :

                  A sequence of finite kernels such that κ = ProbabilityTheory.Kernel.sum (seq κ). See ProbabilityTheory.Kernel.isFiniteKernel_seq and ProbabilityTheory.Kernel.kernel_sum_seq.

                  Equations
                  • κ.seq = .choose
                  Instances For
                    theorem ProbabilityTheory.Kernel.measure_sum_seq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [h : ProbabilityTheory.IsSFiniteKernel κ] (a : α) :
                    (MeasureTheory.Measure.sum fun (n : ) => (κ.seq n) a) = κ a
                    Equations
                    • =
                    theorem ProbabilityTheory.Kernel.IsSFiniteKernel.finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κs : ιProbabilityTheory.Kernel α β} (I : Finset ι) (h : iI, ProbabilityTheory.IsSFiniteKernel (κs i)) :
                    noncomputable def ProbabilityTheory.Kernel.deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : αβ) (hf : Measurable f) :

                    Kernel which to a associates the dirac measure at f a. This is a Markov kernel.

                    Equations
                    Instances For
                      theorem ProbabilityTheory.Kernel.deterministic_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} (hf : Measurable f) (a : α) :
                      theorem ProbabilityTheory.Kernel.deterministic_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} (hf : Measurable f) (a : α) {s : Set β} (hs : MeasurableSet s) :
                      ((ProbabilityTheory.Kernel.deterministic f hf) a) s = s.indicator (fun (x : β) => 1) (f a)
                      theorem ProbabilityTheory.Kernel.lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {g : αβ} {a : α} (hg : Measurable g) (hf : Measurable f) :
                      ∫⁻ (x : β), f x(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
                      @[simp]
                      theorem ProbabilityTheory.Kernel.lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {g : αβ} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] :
                      ∫⁻ (x : β), f x(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
                      theorem ProbabilityTheory.Kernel.setLIntegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {g : αβ} {a : α} (hg : Measurable g) (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a s)] :
                      ∫⁻ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0
                      @[deprecated ProbabilityTheory.Kernel.setLIntegral_deterministic']
                      theorem ProbabilityTheory.Kernel.set_lintegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {g : αβ} {a : α} (hg : Measurable g) (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a s)] :
                      ∫⁻ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0

                      Alias of ProbabilityTheory.Kernel.setLIntegral_deterministic'.

                      @[simp]
                      theorem ProbabilityTheory.Kernel.setLIntegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {g : αβ} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (s : Set β) [Decidable (g a s)] :
                      ∫⁻ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0
                      @[deprecated ProbabilityTheory.Kernel.setLIntegral_deterministic]
                      theorem ProbabilityTheory.Kernel.set_lintegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {g : αβ} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (s : Set β) [Decidable (g a s)] :
                      ∫⁻ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0

                      Alias of ProbabilityTheory.Kernel.setLIntegral_deterministic.

                      theorem ProbabilityTheory.Kernel.integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : βE} {g : αβ} {a : α} (hg : Measurable g) (hf : MeasureTheory.StronglyMeasurable f) :
                      ∫ (x : β), f x(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
                      @[simp]
                      theorem ProbabilityTheory.Kernel.integral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : βE} {g : αβ} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] :
                      ∫ (x : β), f x(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
                      theorem ProbabilityTheory.Kernel.setIntegral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : βE} {g : αβ} {a : α} (hg : Measurable g) (hf : MeasureTheory.StronglyMeasurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a s)] :
                      ∫ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0
                      @[deprecated ProbabilityTheory.Kernel.setIntegral_deterministic']
                      theorem ProbabilityTheory.Kernel.set_integral_deterministic' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : βE} {g : αβ} {a : α} (hg : Measurable g) (hf : MeasureTheory.StronglyMeasurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a s)] :
                      ∫ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0

                      Alias of ProbabilityTheory.Kernel.setIntegral_deterministic'.

                      @[simp]
                      theorem ProbabilityTheory.Kernel.setIntegral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : βE} {g : αβ} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (s : Set β) [Decidable (g a s)] :
                      ∫ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0
                      @[deprecated ProbabilityTheory.Kernel.setIntegral_deterministic]
                      theorem ProbabilityTheory.Kernel.set_integral_deterministic {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : βE} {g : αβ} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] (s : Set β) [Decidable (g a s)] :
                      ∫ (x : β) in s, f x(ProbabilityTheory.Kernel.deterministic g hg) a = if g a s then f (g a) else 0

                      Alias of ProbabilityTheory.Kernel.setIntegral_deterministic.

                      Constant kernel, which always returns the same measure.

                      Equations
                      Instances For
                        @[simp]
                        theorem ProbabilityTheory.Kernel.const_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μβ : MeasureTheory.Measure β) (a : α) :
                        @[simp]
                        @[simp]
                        theorem ProbabilityTheory.Kernel.lintegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {μ : MeasureTheory.Measure β} {a : α} :
                        ∫⁻ (x : β), f x(ProbabilityTheory.Kernel.const α μ) a = ∫⁻ (x : β), f xμ
                        @[simp]
                        theorem ProbabilityTheory.Kernel.setLIntegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {μ : MeasureTheory.Measure β} {a : α} {s : Set β} :
                        ∫⁻ (x : β) in s, f x(ProbabilityTheory.Kernel.const α μ) a = ∫⁻ (x : β) in s, f xμ
                        @[deprecated ProbabilityTheory.Kernel.setLIntegral_const]
                        theorem ProbabilityTheory.Kernel.set_lintegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : βENNReal} {μ : MeasureTheory.Measure β} {a : α} {s : Set β} :
                        ∫⁻ (x : β) in s, f x(ProbabilityTheory.Kernel.const α μ) a = ∫⁻ (x : β) in s, f xμ

                        Alias of ProbabilityTheory.Kernel.setLIntegral_const.

                        @[simp]
                        theorem ProbabilityTheory.Kernel.integral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] {f : βE} {μ : MeasureTheory.Measure β} {a : α} :
                        ∫ (x : β), f x(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β), f xμ
                        @[simp]
                        theorem ProbabilityTheory.Kernel.setIntegral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] {f : βE} {μ : MeasureTheory.Measure β} {a : α} {s : Set β} :
                        ∫ (x : β) in s, f x(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β) in s, f xμ
                        @[deprecated ProbabilityTheory.Kernel.setIntegral_const]
                        theorem ProbabilityTheory.Kernel.set_integral_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] {f : βE} {μ : MeasureTheory.Measure β} {a : α} {s : Set β} :
                        ∫ (x : β) in s, f x(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β) in s, f xμ

                        Alias of ProbabilityTheory.Kernel.setIntegral_const.

                        def ProbabilityTheory.Kernel.ofFunOfCountable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] :
                        {x : MeasurableSpace β} → [inst : Countable α] → [inst : MeasurableSingletonClass α] → (αMeasureTheory.Measure β)ProbabilityTheory.Kernel α β

                        In a countable space with measurable singletons, every function α → MeasureTheory.Measure β defines a kernel.

                        Equations
                        Instances For
                          noncomputable def ProbabilityTheory.Kernel.restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) :

                          Kernel given by the restriction of the measures in the image of a kernel to a set.

                          Equations
                          • κ.restrict hs = { toFun := fun (a : α) => (κ a).restrict s, measurable' := }
                          Instances For
                            theorem ProbabilityTheory.Kernel.restrict_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α) :
                            (κ.restrict hs) a = (κ a).restrict s
                            theorem ProbabilityTheory.Kernel.restrict_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} {t : Set β} (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α) (ht : MeasurableSet t) :
                            ((κ.restrict hs) a) t = (κ a) (t s)
                            @[simp]
                            theorem ProbabilityTheory.Kernel.restrict_univ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} :
                            κ.restrict = κ
                            @[simp]
                            theorem ProbabilityTheory.Kernel.lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α) (f : βENNReal) :
                            ∫⁻ (b : β), f b(κ.restrict hs) a = ∫⁻ (b : β) in s, f bκ a
                            @[simp]
                            theorem ProbabilityTheory.Kernel.setLIntegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α) (f : βENNReal) (t : Set β) :
                            ∫⁻ (b : β) in t, f b(κ.restrict hs) a = ∫⁻ (b : β) in t s, f bκ a
                            @[deprecated ProbabilityTheory.Kernel.setLIntegral_restrict]
                            theorem ProbabilityTheory.Kernel.set_lintegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α) (f : βENNReal) (t : Set β) :
                            ∫⁻ (b : β) in t, f b(κ.restrict hs) a = ∫⁻ (b : β) in t s, f bκ a

                            Alias of ProbabilityTheory.Kernel.setLIntegral_restrict.

                            @[simp]
                            theorem ProbabilityTheory.Kernel.setIntegral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {s : Set β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] {f : βE} {a : α} (hs : MeasurableSet s) (t : Set β) :
                            ∫ (x : β) in t, f x(κ.restrict hs) a = ∫ (x : β) in t s, f xκ a
                            @[deprecated ProbabilityTheory.Kernel.setIntegral_restrict]
                            theorem ProbabilityTheory.Kernel.set_integral_restrict {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {s : Set β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] {f : βE} {a : α} (hs : MeasurableSet s) (t : Set β) :
                            ∫ (x : β) in t, f x(κ.restrict hs) a = ∫ (x : β) in t s, f xκ a

                            Alias of ProbabilityTheory.Kernel.setIntegral_restrict.

                            Equations
                            • =
                            noncomputable def ProbabilityTheory.Kernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γβ} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f) :

                            Kernel with value (κ a).comap f, for a measurable embedding f. That is, for a measurable set t : Set β, ProbabilityTheory.Kernel.comapRight κ hf a t = κ a (f '' t).

                            Equations
                            Instances For
                              theorem ProbabilityTheory.Kernel.comapRight_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γβ} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f) (a : α) :
                              (κ.comapRight hf) a = MeasureTheory.Measure.comap f (κ a)
                              theorem ProbabilityTheory.Kernel.comapRight_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γβ} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f) (a : α) {t : Set γ} (ht : MeasurableSet t) :
                              ((κ.comapRight hf) a) t = (κ a) (f '' t)
                              @[simp]
                              theorem ProbabilityTheory.Kernel.comapRight_id {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) :
                              κ.comapRight = κ
                              theorem ProbabilityTheory.Kernel.IsMarkovKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γβ} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f) (hκ : ∀ (a : α), (κ a) (Set.range f) = 1) :
                              instance ProbabilityTheory.Kernel.IsFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γβ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (hf : MeasurableEmbedding f) :
                              Equations
                              • =
                              instance ProbabilityTheory.Kernel.IsSFiniteKernel.comapRight {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γβ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf : MeasurableEmbedding f) :
                              Equations
                              • =
                              def ProbabilityTheory.Kernel.piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} [DecidablePred fun (x : α) => x s] (hs : MeasurableSet s) (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) :

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

                              Equations
                              Instances For
                                theorem ProbabilityTheory.Kernel.piecewise_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] (a : α) :
                                (ProbabilityTheory.Kernel.piecewise hs κ η) a = if a s then κ a else η a
                                theorem ProbabilityTheory.Kernel.piecewise_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] (a : α) (t : Set β) :
                                ((ProbabilityTheory.Kernel.piecewise hs κ η) a) t = if a s then (κ a) t else (η a) t
                                theorem ProbabilityTheory.Kernel.lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] (a : α) (g : βENNReal) :
                                ∫⁻ (b : β), g b(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a s then ∫⁻ (b : β), g bκ a else ∫⁻ (b : β), g bη a
                                theorem ProbabilityTheory.Kernel.setLIntegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] (a : α) (g : βENNReal) (t : Set β) :
                                ∫⁻ (b : β) in t, g b(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a s then ∫⁻ (b : β) in t, g bκ a else ∫⁻ (b : β) in t, g bη a
                                @[deprecated ProbabilityTheory.Kernel.setLIntegral_piecewise]
                                theorem ProbabilityTheory.Kernel.set_lintegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] (a : α) (g : βENNReal) (t : Set β) :
                                ∫⁻ (b : β) in t, g b(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a s then ∫⁻ (b : β) in t, g bκ a else ∫⁻ (b : β) in t, g bη a

                                Alias of ProbabilityTheory.Kernel.setLIntegral_piecewise.

                                theorem ProbabilityTheory.Kernel.integral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] (a : α) (g : βE) :
                                ∫ (b : β), g b(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a s then ∫ (b : β), g bκ a else ∫ (b : β), g bη a
                                theorem ProbabilityTheory.Kernel.setIntegral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] (a : α) (g : βE) (t : Set β) :
                                ∫ (b : β) in t, g b(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a s then ∫ (b : β) in t, g bκ a else ∫ (b : β) in t, g bη a
                                @[deprecated ProbabilityTheory.Kernel.setIntegral_piecewise]
                                theorem ProbabilityTheory.Kernel.set_integral_piecewise {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {s : Set α} {hs : MeasurableSet s} [DecidablePred fun (x : α) => x s] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] (a : α) (g : βE) (t : Set β) :
                                ∫ (b : β) in t, g b(ProbabilityTheory.Kernel.piecewise hs κ η) a = if a s then ∫ (b : β) in t, g bκ a else ∫ (b : β) in t, g bη a

                                Alias of ProbabilityTheory.Kernel.setIntegral_piecewise.