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, 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 : γ) => κ.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 : α × γ) => κ.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) :
    Measurable fun (a : α) => κ.densityProcess ν n a x 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) :
    Measurable fun (x : γ) => κ.densityProcess ν n a x 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) :
    Measurable fun (x : γ) => κ.densityProcess ν n a x s
    theorem ProbabilityTheory.Kernel.stronglyMeasurable_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) :
    MeasureTheory.StronglyMeasurable fun (x : γ) => κ.densityProcess ν n a x s
    theorem ProbabilityTheory.Kernel.adapted_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β)) (ν : ProbabilityTheory.Kernel α γ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    MeasureTheory.Adapted (ProbabilityTheory.countableFiltration γ) fun (n : ) (x : γ) => κ.densityProcess ν n a x 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 β) :
    0 κ.densityProcess ν n a x s
    theorem ProbabilityTheory.Kernel.meas_countablePartitionSet_le_of_fst_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} {ν : ProbabilityTheory.Kernel α γ} (hκν : κ.fst ν) (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κν : κ.fst ν) (n : ) (a : α) (x : γ) (s : Set β) :
    κ.densityProcess ν n a x s 1
    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κν : κ.fst ν) (n : ) (a : α) (s : Set β) :
    MeasureTheory.snorm (fun (x : γ) => κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    MeasureTheory.Integrable (fun (x : γ) => κ.densityProcess ν n a x s) (ν a)
    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κν : κ.fst ν) [hν : ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {u : Set γ} (hu : u MeasurableSpace.countablePartition γ n) :
    ∫ (x : γ) in u, κ.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κν : κ.fst ν) [hν : ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {u : Set γ} (hu : u MeasurableSpace.countablePartition γ n) :
    ∫ (x : γ) in u, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∫ (x : γ), κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] {n : } {m : } (hnm : n m) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] {n : } {m : } (hnm : n m) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] {i : } {j : } (hij : i j) (a : α) {s : Set β} (hs : MeasurableSet s) :
    (MeasureTheory.condexp ((ProbabilityTheory.countableFiltration γ) i) (ν a) fun (x : γ) => κ.densityProcess ν j a x s) =ᵐ[ν a] fun (x : γ) => κ.densityProcess ν i a x s
    theorem ProbabilityTheory.Kernel.martingale_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} {ν : ProbabilityTheory.Kernel α γ} (hκν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    MeasureTheory.Martingale (fun (n : ) (x : γ) => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)
    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κν : κ.fst ν) (n : ) (a : α) (x : γ) {s : Set β} {s' : Set β} (h : s s') :
    κ.densityProcess ν n a x s κ.densityProcess ν n a x 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κ'ν : κ'.fst ν) (n : ) (a : α) (x : γ) (s : Set β) :
    κ.densityProcess ν n a x s κ'.densityProcess ν n a x s
    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κν : κ.fst ν) (n : ) (a : α) (x : γ) (s : Set β) :
    κ.densityProcess ν' n a x s κ.densityProcess ν n a x s
    @[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 : γ) :
    κ.densityProcess ν n a x = 0
    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 : ) => κ.densityProcess ν n a x (seq m)) Filter.atTop (nhds (κ.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 : ) => κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun (n : ) => κ.densityProcess ν n a x s) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a) x))
    theorem ProbabilityTheory.Kernel.memL1_limitProcess_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} {ν : ProbabilityTheory.Kernel α γ} (hκν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    MeasureTheory.Memℒp (MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)) 1 (ν a)
    theorem ProbabilityTheory.Kernel.tendsto_snorm_one_densityProcess_limitProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} {ν : ProbabilityTheory.Kernel α γ} (hκν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((fun (x : γ) => κ.densityProcess ν n a x s) - MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)) 1 (ν a)) Filter.atTop (nhds 0)
    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κν : κ.fst ν) (a : α) {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
    Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((fun (x : γ) => κ.densityProcess ν n a x s) - MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => κ.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
    • κ.density ν a x s = Filter.limsup (fun (n : ) => κ.densityProcess ν n a x s) Filter.atTop
    Instances For
      theorem ProbabilityTheory.Kernel.density_ae_eq_limitProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} {ν : ProbabilityTheory.Kernel α γ} (hκν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
      (fun (x : γ) => κ.density ν a x s) =ᵐ[ν a] MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)
      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κν : κ.fst ν) (a : α) [ProbabilityTheory.IsFiniteKernel ν] {s : Set β} (hs : MeasurableSet s) :
      ∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun (n : ) => κ.densityProcess ν n a x s) Filter.atTop (nhds (κ.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 : α × γ) => κ.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 : α) => κ.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 : γ) => κ.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κν : κ.fst ν) (a : α) (x : γ) {s : Set β} {s' : Set β} (h : s s') :
      κ.density ν a x s κ.density ν a x 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κν : κ.fst ν) (a : α) (x : γ) (s : Set β) :
      0 κ.density ν a x s
      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κν : κ.fst ν) (a : α) (x : γ) (s : Set β) :
      κ.density ν a x s 1
      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κν : κ.fst ν) (a : α) (s : Set β) :
      MeasureTheory.snorm (fun (x : γ) => κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
      MeasureTheory.Integrable (fun (x : γ) => κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
      Filter.Tendsto (fun (i : ) => ∫ (x : γ) in A, κ.densityProcess ν i a x sν a) Filter.atTop (nhds (∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
      Filter.Tendsto (fun (i : ) => ∫ (x : γ) in A, κ.densityProcess ν i a x sν a) Filter.atTop (nhds (∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (n : ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
      ∫ (x : γ), κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, κ.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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫ (x : γ) in A, κ.density ν a x sν a = ((κ a) (A ×ˢ s)).toReal

      Alias of ProbabilityTheory.Kernel.setIntegral_density.

      theorem ProbabilityTheory.Kernel.setLIntegral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} {ν : ProbabilityTheory.Kernel α γ} (hκν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s)ν a = (κ a) (A ×ˢ s)
      @[deprecated ProbabilityTheory.Kernel.setLIntegral_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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
      ∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s)ν a = (κ a) (A ×ˢ s)

      Alias of ProbabilityTheory.Kernel.setLIntegral_density.

      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κν : κ.fst ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
      ∫⁻ (x : γ), ENNReal.ofReal (κ.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κν : κ.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 : γ), κ.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κν : κ.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 : γ), κ.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κν : κ.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 : ) => κ.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.densityProcess_fst_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} [ProbabilityTheory.IsFiniteKernel κ] (n : ) (a : α) (x : γ) :
      κ.densityProcess κ.fst n a x Set.univ = if (κ.fst a) (MeasurableSpace.countablePartitionSet n x) = 0 then 0 else 1
      theorem ProbabilityTheory.Kernel.densityProcess_fst_univ_ae {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β)) [ProbabilityTheory.IsFiniteKernel κ] (n : ) (a : α) :
      ∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x Set.univ = 1
      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) :
      Filter.Tendsto (fun (m : ) => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop (nhds (κ.densityProcess κ.fst n a x 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 : γ) ∂κ.fst a, Filter.Tendsto (fun (m : ) => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop (nhds 1)
      theorem ProbabilityTheory.Kernel.density_fst_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β)) [ProbabilityTheory.IsFiniteKernel κ] (a : α) :
      ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x Set.univ = 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 : γ) ∂κ.fst a, Filter.Tendsto (fun (m : ) => κ.density κ.fst a x (seq m)) Filter.atTop (nhds 1)