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.

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 has row a 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

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

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

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

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)

@[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

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

theorem ProbabilityTheory.Kernel.isProbabilityMeasure_ofWeights_of_absolutelyContinuous {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {w : α → β → ENNReal} {a : α} {μ : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] (htop : ∀ (b : β), w a b ≠ ⊤) (hμ : μ.AbsolutelyContinuous ((ofWeights w) a)) : MeasureTheory.IsProbabilityMeasure ((ofWeights w) a)

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₁

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

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)

theorem ProbabilityTheory.Kernel.ofWeights_apply_eq_dirac {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] [DecidableEq β] {w : α → β → ENNReal} {a : α} {b₀ : β} {c : ENNReal} (hc0 : c ≠ 0) (hc : c ≠ ⊤) (h : ∀ (b : β), w a b = if b = b₀ then c else 0) : (ofWeights w) a = MeasureTheory.Measure.dirac b₀

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

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

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

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

The product of two uniform experts is uniform on their agreement set, and collapses to the zero measure when they agree nowhere.