Kernels from weight functions

This file defines ProbabilityTheory.Kernel.ofWeights, the kernel that normalizes a nonnegative weight function on a finite target into a probability measure per row, and evaluates it at singletons. A row of zero or infinite total weight collapses to the zero measure, so the kernel is always finite; it is Markov exactly on rows with a positive finite total.

Main definitions

• ProbabilityTheory.Kernel.ofWeights — row a is proportional to w a.

Main results

• ProbabilityTheory.Kernel.ofWeights_apply_singleton — w a b / ∑ b', w a b'; ofWeights_apply_finset, ofWeights_real_setOf for finite events.
• ProbabilityTheory.Kernel.ofWeights_real_singleton_lt_iff — row preference is weight comparison.
• ProbabilityTheory.Kernel.ofWeights_uniformOn_mul_uniformOn — the product of two uniform experts is uniform on their agreement set.

theorem MeasureTheory.Measure.sum_smul_dirac_apply_singleton {β : Type u_1} [MeasurableSpace β] [Fintype β] [MeasurableSingletonClass β] (w : β → ENNReal) (b : β) : (∑ b' : β, w b' • dirac b') {b} = w b

A finite sum of scaled Dirac measures evaluates at a singleton to its weight.

theorem ProbabilityTheory.Kernel.ofFunOfCountable_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (f : α → MeasureTheory.Measure β) (a : α) : (ofFunOfCountable f) a = f a

noncomputable def ProbabilityTheory.Kernel.ofWeights {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (w : α → β → ENNReal) : Kernel α β

The kernel that normalizes a nonnegative weight function on a finite target: row a is the probability measure proportional to w a. A row of zero (or infinite) total weight collapses to the zero measure.

Equations

• ProbabilityTheory.Kernel.ofWeights w = ProbabilityTheory.Kernel.ofFunOfCountable fun (a : α) => (∑ b : β, w a b)⁻¹ • ∑ b : β, w a b • MeasureTheory.Measure.dirac b

@[simp]

theorem ProbabilityTheory.Kernel.ofWeights_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) (a : α) (b : β) : ((ofWeights w) a) {b} = w a b / ∑ b' : β, w a b'

theorem ProbabilityTheory.Kernel.ofWeights_apply_singleton_eq_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {w : α → β → ENNReal} {a : α} {b : β} (h : w a b = 0) : ((ofWeights w) a) {b} = 0

A zero weight gives zero mass.

theorem ProbabilityTheory.Kernel.ofWeights_apply_singleton_ne_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {w : α → β → ENNReal} {a : α} {b : β} (h : w a b ≠ 0) (htop : ∀ (c : β), w a c ≠ ⊤) : ((ofWeights w) a) {b} ≠ 0

A nonzero weight in a row of finite weights gives positive mass.

theorem ProbabilityTheory.Kernel.ofWeights_apply_eq_of_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {w : α → β → ENNReal} {a₁ a₂ : α} {c : ENNReal} (hc0 : c ≠ 0) (hc : c ≠ ⊤) (h : ∀ (b : β), w a₂ b = w a₁ b * c) : (ofWeights w) a₂ = (ofWeights w) a₁

Two rows whose weights differ by a positive finite factor are the same row.

theorem ProbabilityTheory.Kernel.ofWeights_real_singleton_of_pair {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {w : α → β → ENNReal} (a : α) {b b' : β} (hbb' : b ≠ b') (htop : ∀ (c : β), w a c ≠ ⊤) (hsupp : ∀ (c : β), w a c ≠ 0 → c = b ∨ c = b') : ((ofWeights w) a).real {b} = (w a b).toReal / ((w a b).toReal + (w a b').toReal)

In a row with exactly two nonzero weights, both finite, the real mass of one is its share of the two.

theorem ProbabilityTheory.Kernel.ofWeights_apply_finset {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) (a : α) (E : Finset β) : ((ofWeights w) a) ↑E = (∑ b ∈ E, w a b) / ∑ b : β, w a b

The mass of a finite event under a weight-kernel row.

theorem ProbabilityTheory.Kernel.ofWeights_apply_setOf_eq_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) (a : α) : ((ofWeights w) a) {b : β | w a b = 0} = 0

A weight-kernel row is carried by the support of its weights.

theorem ProbabilityTheory.Kernel.ofWeights_real_finset {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) (a : α) (hw : ∀ (b : β), w a b ≠ ⊤) (E : Finset β) : ((ofWeights w) a).real ↑E = (∑ b ∈ E, (w a b).toReal) / ∑ b : β, (w a b).toReal

The real mass of a finite event under a weight-kernel row with finite weights.

theorem ProbabilityTheory.Kernel.ofWeights_real_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) (a : α) (hw : ∀ (b : β), w a b ≠ ⊤) (b : β) : ((ofWeights w) a).real {b} = (w a b).toReal / ∑ b' : β, (w a b').toReal

The real mass of an atom under a weight-kernel row with finite weights.

theorem ProbabilityTheory.Kernel.ofWeights_real_setOf {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) (a : α) (hw : ∀ (b : β), w a b ≠ ⊤) (p : β → Prop) [DecidablePred p] : ((ofWeights w) a).real {b : β | p b} = (∑ b : β with p b, (w a b).toReal) / ∑ b : β, (w a b).toReal

The real mass of a decidable event under a weight-kernel row with finite weights.

theorem ProbabilityTheory.Kernel.isMarkovKernel_ofWeights {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {w : α → β → ENNReal} (h0 : ∀ (a : α), ∃ (b : β), w a b ≠ 0) (htop : ∀ (a : α) (b : β), w a b ≠ ⊤) : IsMarkovKernel (ofWeights w)

A row with a positive entry and finite entries normalizes to a probability measure.

theorem ProbabilityTheory.Kernel.ofWeights_real_singleton_lt_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {w : α → β → ENNReal} (a : α) (h0 : ∑ b : β, w a b ≠ 0) (htop : ∑ b : β, w a b ≠ ⊤) {b₁ b₂ : β} : ((ofWeights w) a).real {b₁} < ((ofWeights w) a).real {b₂} ↔ w a b₁ < w a b₂

Row-preference in a weight kernel reduces to weight comparison; the normalization cancels.

theorem ProbabilityTheory.Kernel.ofWeights_apply_univ_le_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (w : α → β → ENNReal) (a : α) : ((ofWeights w) a) Set.univ ≤ 1

Weight-kernel rows are subprobabilities: normalization gives mass 1 on positive finite total weight and 0 otherwise.

instance ProbabilityTheory.Kernel.instIsFiniteKernelOfWeights {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (w : α → β → ENNReal) : IsFiniteKernel (ofWeights w)

theorem ProbabilityTheory.Kernel.uniformOn_mul_uniformOn_apply_singleton {β : Type u_2} [MeasurableSpace β] [MeasurableSingletonClass β] [DecidableEq β] (A B : Finset β) (b : β) : (uniformOn ↑A) {b} * (uniformOn ↑B) {b} = if b ∈ A ∩ B then (↑A.card * ↑B.card)⁻¹ else 0

Two uniform experts weight a point by (#A · #B)⁻¹ on their agreement set and 0 off it.

theorem ProbabilityTheory.Kernel.ofWeights_uniformOn_mul_uniformOn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] [DecidableEq β] (A B : α → Finset β) (a : α) : (ofWeights fun (a : α) (b : β) => (uniformOn ↑(A a)) {b} * (uniformOn ↑(B a)) {b}) a = uniformOn ↑(A a ∩ B a)

Product of Experts of two uniform experts: the row is uniform on their agreement set, and collapses to the zero measure when they agree nowhere.