Documentation

Mathlib.Probability.Kernel.Disintegration.Density

Kernel density #

Let κ : kernel α (γ × β) and ν : kernel α γ be two finite kernels with kernel.fst κ ≤ ν, where γ has a countably generated σ-algebra (true in particular for standard Borel spaces). We build a function density κ ν : α → γ → Set β → ℝ jointly measurable in the first two arguments such that for all a : α and all measurable sets s : Set β and A : Set γ, ∫ x in A, density κ ν a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal.

There are two main applications of this construction (still TODO, in other files).

Main definitions #

Main statements #

Construction of the density #

If we were interested only in a fixed a : α, then we could use the Radon-Nikodym derivative to build the density function density κ ν, as follows.

def density' (κ : kernel α (γ × β)) (ν : kernel a γ) (a : α) (x : γ) (s : Set β) : ℝ :=
  (((κ a).restrict (univ ×ˢ s)).fst.rnDeriv (ν a) x).toReal

However, we can't turn those functions for each a into a measurable function of the pair (a, x).

In order to obtain measurability through countability, we use the fact that the measurable space γ is countably generated. For each n : ℕ, we define (in the file Mathlib.Probability.Process.PartitionFiltration) a finite partition of γ, such that those partitions are finer as n grows, and the σ-algebra generated by the union of all partitions is the σ-algebra of γ. For x : γ, countablePartitionSet n x denotes the set in the partition such that x ∈ countablePartitionSet n x.

For a given n, the function densityProcess κ ν n : α → γ → Set β → ℝ defined by fun a x s ↦ (κ a (countablePartitionSet n x ×ˢ s) / ν a (countablePartitionSet n x)).toReal has the desired property that ∫ x in A, densityProcess κ ν n a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal for all A in the σ-algebra generated by the partition at scale n and is measurable in (a, x).

countableFiltration γ is the filtration of those σ-algebras for all n : ℕ. The functions densityProcess κ ν n described here are a bounded ν-martingale for the filtration countableFiltration γ. By Doob's martingale L1 convergence theorem, that martingale converges to a limit, which has a product-measurable version and satisfies the integral equality for all A in ⨆ n, countableFiltration γ n. Finally, the partitions were chosen such that that supremum is equal to the σ-algebra on γ, hence the equality holds for all measurable sets. We have obtained the desired density function.

References #

The construction of the density process in this file follows the proof of Theorem 9.27 in [O. Kallenberg, Foundations of modern probability][kallenberg2021], adapted to use a countably generated hypothesis instead of specializing to .

noncomputable def ProbabilityTheory.kernel.densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) (a : α) (x : γ) (s : Set β) :

An -indexed martingale that is a density for κ with respect to ν on the sets in countablePartition γ n. Used to define its limit ProbabilityTheory.kernel.density, which is a density for those kernels for all measurable sets.

Equations
Instances For
    theorem ProbabilityTheory.kernel.densityProcess_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) (a : α) (s : Set β) :
    (fun (t : γ) => ProbabilityTheory.kernel.densityProcess κ ν n a t s) = fun (t : γ) => ((κ a) (MeasurableSpace.countablePartitionSet n t ×ˢ s) / (ν a) (MeasurableSpace.countablePartitionSet n t)).toReal
    theorem ProbabilityTheory.kernel.measurable_densityProcess_aux {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) {s : Set β} (hs : MeasurableSet s) :
    theorem ProbabilityTheory.kernel.measurable_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) {s : Set β} (hs : MeasurableSet s) :
    Measurable fun (p : α × γ) => ProbabilityTheory.kernel.densityProcess κ ν n p.1 p.2 s
    theorem ProbabilityTheory.kernel.measurable_densityProcess_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) (x : γ) {s : Set β} (hs : MeasurableSet s) :
    theorem ProbabilityTheory.kernel.measurable_densityProcess_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) {s : Set β} (a : α) (hs : MeasurableSet s) :
    theorem ProbabilityTheory.kernel.measurable_countableFiltration_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    theorem ProbabilityTheory.kernel.densityProcess_nonneg {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) (a : α) (x : γ) (s : Set β) :
    theorem ProbabilityTheory.kernel.densityProcess_le_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (n : ) (a : α) (x : γ) (s : Set β) :
    theorem ProbabilityTheory.kernel.snorm_densityProcess_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (n : ) (a : α) (s : Set β) :
    MeasureTheory.snorm (fun (x : γ) => ProbabilityTheory.kernel.densityProcess κ ν n a x s) 1 (ν a) (ν a) Set.univ
    theorem ProbabilityTheory.kernel.integrable_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    theorem ProbabilityTheory.kernel.setIntegral_densityProcess_of_mem {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [hν : ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {u : Set γ} (hu : u MeasurableSpace.countablePartition γ n) :
    ∫ (x : γ) in u, ProbabilityTheory.kernel.densityProcess κ ν n a x sν a = ((κ a) (u ×ˢ s)).toReal
    @[deprecated ProbabilityTheory.kernel.setIntegral_densityProcess_of_mem]
    theorem ProbabilityTheory.kernel.set_integral_densityProcess_of_mem {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [hν : ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {u : Set γ} (hu : u MeasurableSpace.countablePartition γ n) :
    ∫ (x : γ) in u, ProbabilityTheory.kernel.densityProcess κ ν n a x sν a = ((κ a) (u ×ˢ s)).toReal

    Alias of ProbabilityTheory.kernel.setIntegral_densityProcess_of_mem.

    theorem ProbabilityTheory.kernel.setIntegral_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, ProbabilityTheory.kernel.densityProcess κ ν n a x sν a = ((κ a) (A ×ˢ s)).toReal
    @[deprecated ProbabilityTheory.kernel.setIntegral_densityProcess]
    theorem ProbabilityTheory.kernel.set_integral_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, ProbabilityTheory.kernel.densityProcess κ ν n a x sν a = ((κ a) (A ×ˢ s)).toReal

    Alias of ProbabilityTheory.kernel.setIntegral_densityProcess.

    theorem ProbabilityTheory.kernel.integral_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∫ (x : γ), ProbabilityTheory.kernel.densityProcess κ ν n a x sν a = ((κ a) (Set.univ ×ˢ s)).toReal
    theorem ProbabilityTheory.kernel.setIntegral_densityProcess_of_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] {n : } {m : } (hnm : n m) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, ProbabilityTheory.kernel.densityProcess κ ν m a x sν a = ((κ a) (A ×ˢ s)).toReal
    @[deprecated ProbabilityTheory.kernel.setIntegral_densityProcess_of_le]
    theorem ProbabilityTheory.kernel.set_integral_densityProcess_of_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] {n : } {m : } (hnm : n m) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, ProbabilityTheory.kernel.densityProcess κ ν m a x sν a = ((κ a) (A ×ˢ s)).toReal

    Alias of ProbabilityTheory.kernel.setIntegral_densityProcess_of_le.

    theorem ProbabilityTheory.kernel.condexp_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] {i : } {j : } (hij : i j) (a : α) {s : Set β} (hs : MeasurableSet s) :
    theorem ProbabilityTheory.kernel.densityProcess_mono_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (n : ) (a : α) (x : γ) {s : Set β} {s' : Set β} (h : s s') :
    theorem ProbabilityTheory.kernel.densityProcess_mono_kernel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} {κ' : (ProbabilityTheory.kernel α (γ × β))} (hκκ' : κ κ') (hκ'ν : ProbabilityTheory.kernel.fst κ' ν) (n : ) (a : α) (x : γ) (s : Set β) :
    theorem ProbabilityTheory.kernel.densityProcess_antitone_kernel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} {ν' : (ProbabilityTheory.kernel α γ)} (hνν' : ν ν') (hκν : ProbabilityTheory.kernel.fst κ ν) (n : ) (a : α) (x : γ) (s : Set β) :
    @[simp]
    theorem ProbabilityTheory.kernel.densityProcess_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (n : ) (a : α) (x : γ) :
    theorem ProbabilityTheory.kernel.tendsto_densityProcess_atTop_empty_of_antitone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) [ProbabilityTheory.IsFiniteKernel κ] (n : ) (a : α) (x : γ) (seq : Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ (i : ), seq i = ) (hseq_meas : ∀ (m : ), MeasurableSet (seq m)) :
    Filter.Tendsto (fun (m : ) => ProbabilityTheory.kernel.densityProcess κ ν n a x (seq m)) Filter.atTop (nhds (ProbabilityTheory.kernel.densityProcess κ ν n a x ))
    theorem ProbabilityTheory.kernel.tendsto_densityProcess_atTop_of_antitone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) [ProbabilityTheory.IsFiniteKernel κ] (n : ) (a : α) (x : γ) (seq : Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ (i : ), seq i = ) (hseq_meas : ∀ (m : ), MeasurableSet (seq m)) :
    Filter.Tendsto (fun (m : ) => ProbabilityTheory.kernel.densityProcess κ ν n a x (seq m)) Filter.atTop (nhds 0)
    theorem ProbabilityTheory.kernel.tendsto_densityProcess_limitProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun (n : ) => ProbabilityTheory.kernel.densityProcess κ ν n a x s) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => ProbabilityTheory.kernel.densityProcess κ ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a) x))
    theorem ProbabilityTheory.kernel.tendsto_snorm_one_restrict_densityProcess_limitProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} [ProbabilityTheory.IsFiniteKernel ν] (hκν : ProbabilityTheory.kernel.fst κ ν) (a : α) {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
    Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((fun (x : γ) => ProbabilityTheory.kernel.densityProcess κ ν n a x s) - MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => ProbabilityTheory.kernel.densityProcess κ ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)) 1 ((ν a).restrict A)) Filter.atTop (nhds 0)
    noncomputable def ProbabilityTheory.kernel.density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (a : α) (x : γ) (s : Set β) :

    Density of the kernel κ with respect to ν. This is a function α → γ → Set β → ℝ which is measurable on α × γ for all measurable sets s : Set β and satisfies that ∫ x in A, density κ ν a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal for all measurable A : Set γ.

    Equations
    Instances For
      theorem ProbabilityTheory.kernel.tendsto_m_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (a : α) [ProbabilityTheory.IsFiniteKernel ν] {s : Set β} (hs : MeasurableSet s) :
      ∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun (n : ) => ProbabilityTheory.kernel.densityProcess κ ν n a x s) Filter.atTop (nhds (ProbabilityTheory.kernel.density κ ν a x s))
      theorem ProbabilityTheory.kernel.measurable_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) {s : Set β} (hs : MeasurableSet s) :
      Measurable fun (p : α × γ) => ProbabilityTheory.kernel.density κ ν p.1 p.2 s
      theorem ProbabilityTheory.kernel.measurable_density_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) (x : γ) {s : Set β} (hs : MeasurableSet s) :
      Measurable fun (a : α) => ProbabilityTheory.kernel.density κ ν a x s
      theorem ProbabilityTheory.kernel.measurable_density_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : (ProbabilityTheory.kernel α γ)) {s : Set β} (hs : MeasurableSet s) (a : α) :
      Measurable fun (x : γ) => ProbabilityTheory.kernel.density κ ν a x s
      theorem ProbabilityTheory.kernel.density_mono_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (a : α) (x : γ) {s : Set β} {s' : Set β} (h : s s') :
      theorem ProbabilityTheory.kernel.density_nonneg {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (a : α) (x : γ) (s : Set β) :
      theorem ProbabilityTheory.kernel.density_le_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (a : α) (x : γ) (s : Set β) :
      theorem ProbabilityTheory.kernel.snorm_density_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) (a : α) (s : Set β) :
      MeasureTheory.snorm (fun (x : γ) => ProbabilityTheory.kernel.density κ ν a x s) 1 (ν a) (ν a) Set.univ
      theorem ProbabilityTheory.kernel.integrable_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
      MeasureTheory.Integrable (fun (x : γ) => ProbabilityTheory.kernel.density κ ν a x s) (ν a)
      theorem ProbabilityTheory.kernel.tendsto_setIntegral_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
      Filter.Tendsto (fun (i : ) => ∫ (x : γ) in A, ProbabilityTheory.kernel.densityProcess κ ν i a x sν a) Filter.atTop (nhds (∫ (x : γ) in A, ProbabilityTheory.kernel.density κ ν a x sν a))
      @[deprecated ProbabilityTheory.kernel.tendsto_setIntegral_densityProcess]
      theorem ProbabilityTheory.kernel.tendsto_set_integral_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
      Filter.Tendsto (fun (i : ) => ∫ (x : γ) in A, ProbabilityTheory.kernel.densityProcess κ ν i a x sν a) Filter.atTop (nhds (∫ (x : γ) in A, ProbabilityTheory.kernel.density κ ν a x sν a))

      Alias of ProbabilityTheory.kernel.tendsto_setIntegral_densityProcess.

      theorem ProbabilityTheory.kernel.setIntegral_density_of_measurableSet {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, ProbabilityTheory.kernel.density κ ν a x sν a = ((κ a) (A ×ˢ s)).toReal

      Auxiliary lemma for setIntegral_density.

      @[deprecated ProbabilityTheory.kernel.setIntegral_density_of_measurableSet]
      theorem ProbabilityTheory.kernel.set_integral_density_of_measurableSet {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, ProbabilityTheory.kernel.density κ ν a x sν a = ((κ a) (A ×ˢ s)).toReal

      Alias of ProbabilityTheory.kernel.setIntegral_density_of_measurableSet.


      Auxiliary lemma for setIntegral_density.

      theorem ProbabilityTheory.kernel.integral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
      ∫ (x : γ), ProbabilityTheory.kernel.density κ ν a x sν a = ((κ a) (Set.univ ×ˢ s)).toReal
      theorem ProbabilityTheory.kernel.setIntegral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, ProbabilityTheory.kernel.density κ ν a x sν a = ((κ a) (A ×ˢ s)).toReal
      @[deprecated ProbabilityTheory.kernel.setIntegral_density]
      theorem ProbabilityTheory.kernel.set_integral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, ProbabilityTheory.kernel.density κ ν a x sν a = ((κ a) (A ×ˢ s)).toReal

      Alias of ProbabilityTheory.kernel.setIntegral_density.

      theorem ProbabilityTheory.kernel.set_lintegral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫⁻ (x : γ) in A, ENNReal.ofReal (ProbabilityTheory.kernel.density κ ν a x s)ν a = (κ a) (A ×ˢ s)
      theorem ProbabilityTheory.kernel.lintegral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
      ∫⁻ (x : γ), ENNReal.ofReal (ProbabilityTheory.kernel.density κ ν a x s)ν a = (κ a) (Set.univ ×ˢ s)
      theorem ProbabilityTheory.kernel.tendsto_integral_density_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ (i : ), seq i = Set.univ) (hseq_meas : ∀ (m : ), MeasurableSet (seq m)) :
      Filter.Tendsto (fun (m : ) => ∫ (x : γ), ProbabilityTheory.kernel.density κ ν a x (seq m)ν a) Filter.atTop (nhds ((κ a) Set.univ).toReal)
      theorem ProbabilityTheory.kernel.tendsto_integral_density_of_antitone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ (i : ), seq i = ) (hseq_meas : ∀ (m : ), MeasurableSet (seq m)) :
      Filter.Tendsto (fun (m : ) => ∫ (x : γ), ProbabilityTheory.kernel.density κ ν a x (seq m)ν a) Filter.atTop (nhds 0)
      theorem ProbabilityTheory.kernel.tendsto_density_atTop_ae_of_antitone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : (ProbabilityTheory.kernel α γ)} (hκν : ProbabilityTheory.kernel.fst κ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ (i : ), seq i = ) (hseq_meas : ∀ (m : ), MeasurableSet (seq m)) :
      ∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun (m : ) => ProbabilityTheory.kernel.density κ ν a x (seq m)) Filter.atTop (nhds 0)

      We specialize to ν = fst κ, for which density κ (fst κ) a t univ = 1 almost everywhere.

      theorem ProbabilityTheory.kernel.tendsto_densityProcess_fst_atTop_univ_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) (n : ) (a : α) (x : γ) (seq : Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ (i : ), seq i = Set.univ) :
      theorem ProbabilityTheory.kernel.tendsto_densityProcess_fst_atTop_ae_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : (ProbabilityTheory.kernel α (γ × β))) [ProbabilityTheory.IsFiniteKernel κ] (n : ) (a : α) (seq : Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ (i : ), seq i = Set.univ) :
      ∀ᵐ (x : γ) ∂(ProbabilityTheory.kernel.fst κ) a, Filter.Tendsto (fun (m : ) => ProbabilityTheory.kernel.densityProcess κ (ProbabilityTheory.kernel.fst κ) n a x (seq m)) Filter.atTop (nhds 1)
      theorem ProbabilityTheory.kernel.tendsto_density_fst_atTop_ae_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : (ProbabilityTheory.kernel α (γ × β))} [ProbabilityTheory.IsFiniteKernel κ] (a : α) (seq : Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ (i : ), seq i = Set.univ) (hseq_meas : ∀ (m : ), MeasurableSet (seq m)) :
      ∀ᵐ (x : γ) ∂(ProbabilityTheory.kernel.fst κ) a, Filter.Tendsto (fun (m : ) => ProbabilityTheory.kernel.density κ (ProbabilityTheory.kernel.fst κ) a x (seq m)) Filter.atTop (nhds 1)