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 #

noncomputable def ProbabilityTheory.kernel (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] :

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.instFunLikeSubtypeForallMeasureMemAddSubmonoidKernel = { coe := Subtype.val, coe_injective' := }
    instance ProbabilityTheory.kernel.instCovariantAddLE {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
    CovariantClass ((ProbabilityTheory.kernel α β)) ((ProbabilityTheory.kernel α β)) (fun (x x_1 : (ProbabilityTheory.kernel α β)) => x + x_1) fun (x x_1 : (ProbabilityTheory.kernel α β)) => x x_1
    Equations
    • =
    noncomputable instance ProbabilityTheory.kernel.instOrderBot {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
    Equations
    @[simp]
    theorem ProbabilityTheory.kernel.coeFn_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} :
    0 = 0
    @[simp]
    theorem ProbabilityTheory.kernel.coeFn_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : (ProbabilityTheory.kernel α β)) (η : (ProbabilityTheory.kernel α β)) :
    (κ + η) = κ + η

    Coercion to a function as an additive monoid homomorphism.

    Equations
    Instances For
      @[simp]
      theorem ProbabilityTheory.kernel.zero_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (a : α) :
      0 a = 0
      @[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
          noncomputable def ProbabilityTheory.IsFiniteKernel.bound {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : (ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsFiniteKernel κ] :

          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
            • =
            @[instance 100]
            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 {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : (ProbabilityTheory.kernel α β)) :
            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
            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
                Instances For
                  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
                        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 : α) :
                          (ProbabilityTheory.kernel.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) :
                          ((ProbabilityTheory.kernel.restrict κ hs) a) t = (κ a) (t s)
                          @[simp]
                          @[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(ProbabilityTheory.kernel.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(ProbabilityTheory.kernel.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(ProbabilityTheory.kernel.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(ProbabilityTheory.kernel.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(ProbabilityTheory.kernel.restrict κ hs) a = ∫ (x : β) in t s, f xκ a

                          Alias of ProbabilityTheory.kernel.setIntegral_restrict.

                          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 : α) :
                            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) :
                            ((ProbabilityTheory.kernel.comapRight κ hf) a) t = (κ a) (f '' t)
                            @[simp]
                            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) :
                            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.