Kernels from a density against a base measure

This file defines ProbabilityTheory.Kernel.ofDensity, the kernel whose row at a reweights a base measure by the density f a and normalizes. It is Bayes' rule for a likelihood given as a function: with the prior as base and the likelihood of an observation as density, the row is the posterior. A row whose density has zero or infinite total mass collapses to the zero measure, so the kernel is always finite.

Main definitions

• ProbabilityTheory.Kernel.ofDensity: row a is proportional to μ.withDensity (f a).

Main results

• ProbabilityTheory.Kernel.ofDensity_apply_singleton: the mass of an atom is its density times its base mass, over the total.
• ProbabilityTheory.Kernel.ofDensity_indicator_one_apply: at an indicator density the row is the base measure conditioned on the set.
• ProbabilityTheory.Kernel.ofDensity_div_iSup: a bounded density may be taken in the unit interval, since dividing each row by its supremum leaves the kernel unchanged.
• ProbabilityTheory.Kernel.ofDensity_count: against the counting measure the density kernel is the weight kernel Kernel.ofWeights.
• ProbabilityTheory.Kernel.ofDensity_apply_eq_posterior: with a kernel's likelihood as density the row is the posterior, at every observation of positive marginal.

noncomputable def ProbabilityTheory.Kernel.ofDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) : Kernel α β

The kernel that reweights a base measure by a density and normalizes. Row a is the probability measure proportional to μ.withDensity (f a), and the zero measure when the density has zero or infinite total mass.

Equations

• ProbabilityTheory.Kernel.ofDensity μ f = ProbabilityTheory.Kernel.ofFunOfCountable fun (a : α) => (μ.withDensity (f a))[|Set.univ]

theorem ProbabilityTheory.Kernel.ofDensity_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) (a : α) : (ofDensity μ f) a = (μ.withDensity (f a))[|Set.univ]

instance ProbabilityTheory.Kernel.instIsZeroOrProbabilityMeasureCoeMeasureOfDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) (a : α) : MeasureTheory.IsZeroOrProbabilityMeasure ((ofDensity μ f) a)

instance ProbabilityTheory.Kernel.instIsFiniteKernelOfDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) : IsFiniteKernel (ofDensity μ f)

theorem ProbabilityTheory.Kernel.ofDensity_indicator_one_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (s : α → Set β) (a : α) (hs : MeasurableSet (s a)) : (ofDensity μ fun (a : α) => (s a).indicator 1) a = μ[|s a]

At the indicator of a measurable set the row is the base measure conditioned on the set.

theorem ProbabilityTheory.Kernel.ofDensity_apply_eq_of_eq_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) {f f' : α → β → ENNReal} {a : α} {c : ENNReal} (hc0 : c ≠ 0) (hc : c ≠ ⊤) (h : ∀ (b : β), f' a b = c * f a b) : (ofDensity μ f') a = (ofDensity μ f) a

A row depends on its density only up to a positive finite scalar, which the normalization absorbs.

theorem ProbabilityTheory.Kernel.ofDensity_const_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) {c : ENNReal} (hc0 : c ≠ 0) (hc : c ≠ ⊤) : (ofDensity μ fun (a : α) (b : β) => c * f a b) = ofDensity μ f

The kernel depends on the density only up to a positive finite scalar.

theorem ProbabilityTheory.Kernel.ofDensity_div_iSup {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) (hf : ∀ (a : α), ⨆ (b : β), f a b ≠ ⊤) : (ofDensity μ fun (a : α) (b : β) => f a b / ⨆ (b' : β), f a b') = ofDensity μ f

Dividing each row's density by its supremum, which puts the density in the unit interval, leaves the kernel unchanged.

theorem ProbabilityTheory.Kernel.ofDensity_div {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Countable β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (b : β), μ {b} ≠ 0) (ν : α → MeasureTheory.Measure β) (a : α) : (ofDensity μ fun (a : α) (b : β) => (ν a) {b} / μ {b}) a = (ν a)[|Set.univ]

Every finite measure on a countable discrete space is a row of the density kernel at a base of positive mass everywhere, with the measure's density against the base as the density.

theorem ProbabilityTheory.Kernel.ofDensity_apply_singleton' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) (a : α) (b : β) : ((ofDensity μ f) a) {b} = f a b * μ {b} / ∫⁻ (b' : β), f a b' ∂μ

theorem ProbabilityTheory.Kernel.ofDensity_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) (a : α) (b : β) : ((ofDensity μ f) a) {b} = f a b * μ {b} / ∑ b' : β, f a b' * μ {b'}

theorem ProbabilityTheory.Kernel.ofDensity_apply_singleton_ne_zero_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure μ] {f : α → β → ENNReal} {a : α} (hf : ∀ (b : β), f a b ≠ ⊤) (b : β) : ((ofDensity μ f) a) {b} ≠ 0 ↔ f a b ≠ 0 ∧ μ {b} ≠ 0

An atom has positive mass in a row of finite density exactly when its density and its base mass are positive.

theorem ProbabilityTheory.Kernel.ofDensity_apply_singleton_of_equiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] {α' : Type u_3} {β' : Type u_4} [MeasurableSpace α'] [MeasurableSpace β'] [Countable α'] [MeasurableSingletonClass α'] [Fintype β] [MeasurableSingletonClass β] [Fintype β'] [MeasurableSingletonClass β'] (e : β ≃ β') {μ : MeasureTheory.Measure β} {μ' : MeasureTheory.Measure β'} {f : α → β → ENNReal} {f' : α' → β' → ENNReal} {a : α} {a' : α'} (hμ : ∀ (b : β), μ' {e b} = μ {b}) (hf : ∀ (b : β), f' a' (e b) = f a b) (b : β) : ((ofDensity μ' f') a') {e b} = ((ofDensity μ f) a) {b}

A relabelling of the target that carries one base and density to another carries the density kernel along.

theorem ProbabilityTheory.Kernel.isProbabilityMeasure_ofDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure β) (f : α → β → ENNReal) (a : α) (h0 : ∫⁻ (b : β), f a b ∂μ ≠ 0) (htop : ∫⁻ (b : β), f a b ∂μ ≠ ⊤) : MeasureTheory.IsProbabilityMeasure ((ofDensity μ f) a)

A row whose density has positive finite mass under the base is a probability measure.

theorem ProbabilityTheory.Kernel.ofDensity_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] {γ : Type u_3} [MeasurableSpace γ] (μ : MeasureTheory.Measure β) {f : α → γ → ENNReal} {g : β → γ} {a : α} (hf : AEMeasurable (f a) (MeasureTheory.Measure.map g μ)) (hg : AEMeasurable g μ) : MeasureTheory.Measure.map g ((ofDensity μ fun (a : α) => f a ∘ g) a) = (ofDensity (MeasureTheory.Measure.map g μ) f) a

Pushing a row forward along a map through which its density factors gives the row on the pushed-forward base. With a projection as the map, marginalizing a row whose density ignores a coordinate gives the row on the marginal base.

theorem ProbabilityTheory.Kernel.ofDensity_natCast_real_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : β → ℕ) (lik : α → β → ℕ) (a : α) (x : β) : ((ofDensity (MeasureTheory.Measure.ofWeights fun (x : β) => ↑(w x)) fun (a : α) (x : β) => ↑(lik a x)) a).real {x} = ↑(lik a x) * ↑(w x) / ∑ x' : β, ↑(lik a x') * ↑(w x')

On natural-number weights and densities the mass of an atom is its weighted density over the total.

theorem ProbabilityTheory.Kernel.ofDensity_uniformOn_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] [Nonempty β] (f : α → β → ENNReal) (a : α) (b : β) : ((ofDensity (uniformOn Set.univ) f) a) {b} = f a b / ∑ b' : β, f a b'

Against the uniform measure a density normalizes to its share of the row sum, since the base cancels.

theorem ProbabilityTheory.Kernel.ofDensity_uniformOn_ofReal_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] [Nonempty β] (f : α → β → ℝ) (a : α) (b : β) (hf : ∀ (b' : β), 0 ≤ f a b') (hpos : 0 < ∑ b' : β, f a b') : ((ofDensity (uniformOn Set.univ) fun (a : α) (b : β) => ENNReal.ofReal (f a b)) a) {b} = ENNReal.ofReal (f a b / ∑ b' : β, f a b')

With a real-valued density the share is the real ratio of the row.

theorem ProbabilityTheory.Kernel.ofDensity_count {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) : ofDensity MeasureTheory.Measure.count w = ofWeights w

Against the counting measure the density kernel is the weight kernel.

theorem ProbabilityTheory.Kernel.ofDensity_apply_eq_posterior {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Countable β] [MeasurableSingletonClass β] [StandardBorelSpace β] [Nonempty β] (κ : Kernel β α) [IsFiniteKernel κ] (μ : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure μ] {a : α} (ha : (μ.bind ⇑κ) {a} ≠ 0) : (ofDensity μ fun (a : α) (b : β) => (κ b) {a}) a = (posterior κ μ) a

Bayes' rule. With a kernel's likelihood of the observation as density against the prior, the row at an observation of positive marginal is the posterior.