# 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).

• Disintegration of kernels: for κ : kernel α (γ × β), we want to build a kernel η : kernel (α × γ) β such that κ = fst κ ⊗ₖ η. For β = ℝ, we can use the density of κ with respect to fst κ for intervals to build a kernel cumulative distribution function for η. The construction can then be extended to β standard Borel.
• Radon-Nikodym theorem for kernels: for κ ν : kernel α γ, we can use the density to build a Radon-Nikodym derivative of κ with respect to ν. We don't need β here but we can apply the density construction to β = Unit. The derivative construction will use density but will not be exactly equal to it because we will want to remove the fst κ ≤ ν assumption.

## Main definitions #

• ProbabilityTheory.kernel.density: for κ : kernel α (γ × β) and ν : kernel α γ two finite kernels, kernel.density κ ν is a function α → γ → Set β → ℝ.

## Main statements #

• ProbabilityTheory.kernel.setIntegral_density: for all measurable sets A : Set γ and s : Set β, ∫ x in A, kernel.density κ ν a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal.
• ProbabilityTheory.kernel.measurable_density: the function p : α × γ ↦ kernel.density κ ν p.1 p.2 s is measurable.

## 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α : } {mβ : } {mγ : } (κ : (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
• = ((κ a) / (ν a) ).toReal
Instances For
theorem ProbabilityTheory.kernel.densityProcess_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) (a : α) (s : Set β) :
(fun (t : γ) => ) = fun (t : γ) => ((κ a) / (ν a) ).toReal
theorem ProbabilityTheory.kernel.measurable_densityProcess_countableFiltration_aux {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) {s : Set β} (hs : ) :
Measurable fun (p : α × γ) => (κ p.1) () / (ν p.1)
theorem ProbabilityTheory.kernel.measurable_densityProcess_aux {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) {s : Set β} (hs : ) :
Measurable fun (p : α × γ) => (κ p.1) () / (ν p.1)
theorem ProbabilityTheory.kernel.measurable_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) {s : Set β} (hs : ) :
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α : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) (x : γ) {s : Set β} (hs : ) :
Measurable fun (a : α) =>
theorem ProbabilityTheory.kernel.measurable_densityProcess_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) {s : Set β} (a : α) (hs : ) :
Measurable fun (x : γ) =>
theorem ProbabilityTheory.kernel.measurable_countableFiltration_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) (a : α) {s : Set β} (hs : ) :
Measurable fun (x : γ) =>
theorem ProbabilityTheory.kernel.stronglyMeasurable_countableFiltration_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) (a : α) {s : Set β} (hs : ) :
theorem ProbabilityTheory.kernel.adapted_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (a : α) {s : Set β} (hs : ) :
MeasureTheory.Adapted fun (n : ) (x : γ) =>
theorem ProbabilityTheory.kernel.densityProcess_nonneg {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) (a : α) (x : γ) (s : Set β) :
0
theorem ProbabilityTheory.kernel.meas_countablePartitionSet_le_of_fst_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) (x : γ) (s : Set β) :
(κ a) (ν a)
theorem ProbabilityTheory.kernel.densityProcess_le_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) (x : γ) (s : Set β) :
1
theorem ProbabilityTheory.kernel.snorm_densityProcess_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) (s : Set β) :
MeasureTheory.snorm (fun (x : γ) => ) 1 (ν a) (ν a) Set.univ
theorem ProbabilityTheory.kernel.integrable_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) {s : Set β} (hs : ) :
MeasureTheory.Integrable (fun (x : γ) => ) (ν a)
theorem ProbabilityTheory.kernel.setIntegral_densityProcess_of_mem {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) [hν : ] (n : ) (a : α) {s : Set β} (hs : ) {u : Set γ} (hu : ) :
∫ (x : γ) in u, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) [hν : ] (n : ) (a : α) {s : Set β} (hs : ) {u : Set γ} (hu : ) :
∫ (x : γ) in u, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) {s : Set β} (hs : ) :
∫ (x : γ), ν a = ((κ a) (Set.univ ×ˢ s)).toReal
theorem ProbabilityTheory.kernel.setIntegral_densityProcess_of_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) {n : } {m : } (hnm : n m) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) {n : } {m : } (hnm : n m) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) {i : } {j : } (hij : i j) (a : α) {s : Set β} (hs : ) :
(MeasureTheory.condexp (ν a) fun (x : γ) => ) =ᵐ[ν a] fun (x : γ) =>
theorem ProbabilityTheory.kernel.martingale_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
MeasureTheory.Martingale (fun (n : ) (x : γ) => ) (ν a)
theorem ProbabilityTheory.kernel.densityProcess_mono_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} {κ' : (ProbabilityTheory.kernel α (γ × β))} (hκκ' : κ κ') (hκ'ν : ) (n : ) (a : α) (x : γ) (s : Set β) :
theorem ProbabilityTheory.kernel.densityProcess_antitone_kernel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} {ν' : ()} (hνν' : ν ν') (hκν : ) (n : ) (a : α) (x : γ) (s : Set β) :
@[simp]
theorem ProbabilityTheory.kernel.densityProcess_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (n : ) (a : α) (x : γ) :
= 0
theorem ProbabilityTheory.kernel.tendsto_densityProcess_atTop_empty_of_antitone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (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 ())
theorem ProbabilityTheory.kernel.tendsto_densityProcess_atTop_of_antitone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun (n : ) => ) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => ) (ν a) x))
theorem ProbabilityTheory.kernel.memL1_limitProcess_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
MeasureTheory.Memℒp (MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => ) (ν a)) 1 (ν a)
theorem ProbabilityTheory.kernel.tendsto_snorm_one_densityProcess_limitProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((fun (x : γ) => ) - MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => ) (ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) (A : Set γ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((fun (x : γ) => ) - MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => ) (ν a)) 1 ((ν a).restrict A)) Filter.atTop (nhds 0)
noncomputable def ProbabilityTheory.kernel.density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (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.density_ae_eq_limitProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
(fun (x : γ) => ) =ᵐ[ν a] MeasureTheory.Filtration.limitProcess (fun (n : ) (x : γ) => ) (ν a)
theorem ProbabilityTheory.kernel.tendsto_m_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun (n : ) => ) Filter.atTop (nhds ())
theorem ProbabilityTheory.kernel.measurable_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) {s : Set β} (hs : ) :
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α : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) (x : γ) {s : Set β} (hs : ) :
Measurable fun (a : α) =>
theorem ProbabilityTheory.kernel.measurable_density_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (ν : ()) {s : Set β} (hs : ) (a : α) :
Measurable fun (x : γ) =>
theorem ProbabilityTheory.kernel.density_mono_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) (x : γ) {s : Set β} {s' : Set β} (h : s s') :
theorem ProbabilityTheory.kernel.density_nonneg {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) (x : γ) (s : Set β) :
0
theorem ProbabilityTheory.kernel.density_le_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) (x : γ) (s : Set β) :
1
theorem ProbabilityTheory.kernel.snorm_density_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) (s : Set β) :
MeasureTheory.snorm (fun (x : γ) => ) 1 (ν a) (ν a) Set.univ
theorem ProbabilityTheory.kernel.integrable_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
MeasureTheory.Integrable (fun (x : γ) => ) (ν a)
theorem ProbabilityTheory.kernel.tendsto_setIntegral_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) (A : Set γ) :
Filter.Tendsto (fun (i : ) => ∫ (x : γ) in A, ν a) Filter.atTop (nhds (∫ (x : γ) in A, ν a))
@[deprecated ProbabilityTheory.kernel.tendsto_setIntegral_densityProcess]
theorem ProbabilityTheory.kernel.tendsto_set_integral_densityProcess {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) (A : Set γ) :
Filter.Tendsto (fun (i : ) => ∫ (x : γ) in A, ν a) Filter.atTop (nhds (∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (n : ) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
∫ (x : γ), ν a = ((κ a) (Set.univ ×ˢ s)).toReal
theorem ProbabilityTheory.kernel.setIntegral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫ (x : γ) in A, ν 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) {A : Set γ} (hA : ) :
∫⁻ (x : γ) in A, ENNReal.ofReal ()ν a = (κ a) (A ×ˢ s)
theorem ProbabilityTheory.kernel.lintegral_density {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (a : α) {s : Set β} (hs : ) :
∫⁻ (x : γ), ENNReal.ofReal ()ν a = (κ a) (Set.univ ×ˢ s)
theorem ProbabilityTheory.kernel.tendsto_integral_density_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} {ν : ()} (hκν : ) (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.densityProcess_fst_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} (n : ) (a : α) (x : γ) :
= if then 0 else 1
theorem ProbabilityTheory.kernel.densityProcess_fst_univ_ae {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (n : ) (a : α) :
∀ᵐ (x : γ) ∂, = 1
theorem ProbabilityTheory.kernel.tendsto_densityProcess_fst_atTop_univ_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (n : ) (a : α) (x : γ) (seq : Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ (i : ), seq i = Set.univ) :
Filter.Tendsto (fun (m : ) => ) Filter.atTop (nhds ())
theorem ProbabilityTheory.kernel.tendsto_densityProcess_fst_atTop_ae_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (n : ) (a : α) (seq : Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ (i : ), seq i = Set.univ) :
∀ᵐ (x : γ) ∂, Filter.Tendsto (fun (m : ) => ) Filter.atTop (nhds 1)
theorem ProbabilityTheory.kernel.density_fst_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } {mβ : } {mγ : } (κ : (ProbabilityTheory.kernel α (γ × β))) (a : α) :
∀ᵐ (x : γ) ∂, ProbabilityTheory.kernel.density κ 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α : } {mβ : } {mγ : } {κ : (ProbabilityTheory.kernel α (γ × β))} (a : α) (seq : Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ (i : ), seq i = Set.univ) (hseq_meas : ∀ (m : ), MeasurableSet (seq m)) :
∀ᵐ (x : γ) ∂, Filter.Tendsto (fun (m : ) => ) Filter.atTop (nhds 1)