The softmax kernel of an extended-real score

This file defines ProbabilityTheory.Kernel.softmax, the kernel whose row at w is proportional to the exponential of an extended-real score. A point of score ⊥ gets no mass, so the score both ranks the points and says which of them are available.

Main definitions

• ProbabilityTheory.Kernel.softmax: the weight kernel of EReal.exp (score w u).

Main results

• ProbabilityTheory.Kernel.softmax_coe_real_singleton: a real score gives each row Real.softmax of the score.
• ProbabilityTheory.Kernel.softmax_real_singleton_lt_iff: row preference is score comparison.
• ProbabilityTheory.Kernel.softmax_real_singleton_of_pair: with two available points the share of one is the logistic function of the score difference.
• ProbabilityTheory.Kernel.softmax_eq_tilted, ProbabilityTheory.Kernel.isGreatest_freeEnergy_softmax: a row is the uniform measure on the available points tilted by the score, and so maximizes the expected score less the divergence from that uniform measure, by the Gibbs variational principle.

noncomputable def ProbabilityTheory.Kernel.softmax {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (score : α → β → EReal) : Kernel α β

The softmax kernel of an extended-real score has row w proportional to the exponential of the score, so a point of score ⊥ gets no mass.

Equations

• ProbabilityTheory.Kernel.softmax score = ProbabilityTheory.Kernel.ofWeights fun (w : α) (u : β) => (score w u).exp

instance ProbabilityTheory.Kernel.instIsFiniteKernelSoftmax {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (score : α → β → EReal) : IsFiniteKernel (softmax score)

theorem ProbabilityTheory.Kernel.isMarkovKernel_softmax {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {score : α → β → EReal} (h0 : ∀ (w : α), ∃ (u : β), score w u ≠ ⊥) (htop : ∀ (w : α) (u : β), score w u ≠ ⊤) : IsMarkovKernel (softmax score)

The softmax kernel is a probability kernel whenever every row has a point of score above ⊥ and no score is ⊤.

@[simp]

theorem ProbabilityTheory.Kernel.softmax_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (score : α → β → EReal) (w : α) (u : β) : ((softmax score) w) {u} = (score w u).exp / ∑ u' : β, (score w u').exp

theorem ProbabilityTheory.Kernel.softmax_apply_singleton_eq_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {score : α → β → EReal} [MeasurableSingletonClass β] {w : α} {u : β} (h : score w u = ⊥) : ((softmax score) w) {u} = 0

A point of score ⊥ gets no mass.

theorem ProbabilityTheory.Kernel.softmax_apply_singleton_ne_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {score : α → β → EReal} [MeasurableSingletonClass β] {w : α} {u : β} (h : score w u ≠ ⊥) (htop : ∀ (u' : β), score w u' ≠ ⊤) : ((softmax score) w) {u} ≠ 0

A point of score above ⊥ gets positive mass when no score is ⊤.

theorem ProbabilityTheory.Kernel.softmax_apply_eq_of_add {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {score : α → β → EReal} [MeasurableSingletonClass β] {w₁ w₂ : α} {k : ℝ} (h : ∀ (u : β), score w₂ u = score w₁ u + ↑k) : (softmax score) w₂ = (softmax score) w₁

Two rows whose scores differ by a real constant are the same.

theorem ProbabilityTheory.Kernel.softmax_eq_of_add {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {score : α → β → EReal} [MeasurableSingletonClass β] {score' : α → β → EReal} {k : α → ℝ} (h : ∀ (w : α) (u : β), score' w u = score w u + ↑(k w)) : softmax score' = softmax score

Two scores differing by a real constant per row give the same kernel, since a term that does not depend on the point cancels in the normalization.

theorem ProbabilityTheory.Kernel.softmax_real_singleton_lt_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {score : α → β → EReal} [MeasurableSingletonClass β] {w : α} (htop : ∀ (u : β), score w u ≠ ⊤) (h0 : ∃ (u : β), score w u ≠ ⊥) {u u' : β} : ((softmax score) w).real {u} < ((softmax score) w).real {u'} ↔ score w u < score w u'

Row preference of the softmax kernel is score comparison, since the normalization cancels.

theorem ProbabilityTheory.Kernel.softmax_coe_real_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (f : α → β → ℝ) (w : α) (u : β) : ((softmax fun (w : α) (u : β) => ↑(f w u)) w).real {u} = Real.softmax (f w) u

A real-valued score gives each row the softmax of the score.

theorem ProbabilityTheory.Kernel.softmax_coe_real_singleton_lt_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (f : α → β → ℝ) (w : α) {u u' : β} : ((softmax fun (w : α) (u : β) => ↑(f w u)) w).real {u} < ((softmax fun (w : α) (u : β) => ↑(f w u)) w).real {u'} ↔ f w u < f w u'

A real-valued score excludes no point, so row preference is comparison of reals.

theorem ProbabilityTheory.Kernel.softmax_real_singleton_of_pair {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {score : α → β → EReal} [MeasurableSingletonClass β] {w : α} {u u' : β} (huu' : u ≠ u') (hu : score w u ≠ ⊥) (hu' : score w u' ≠ ⊥) (htop : ∀ (v : β), score w v ≠ ⊤) (hsupp : ∀ (v : β), score w v ≠ ⊥ → v = u ∨ v = u') : ((softmax score) w).real {u} = ((score w u).toReal - (score w u').toReal).sigmoid

When exactly two points of a row have score above ⊥, the share of one is the logistic function of the score difference.

The softmax row as a Gibbs measure

theorem ProbabilityTheory.Kernel.softmax_eq_tilted {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {score : α → β → EReal} {w : α} (htop : ∀ (u : β), score w u ≠ ⊤) (h0 : ∃ (u : β), score w u ≠ ⊥) : (softmax score) w = (uniformOn {u : β | score w u ≠ ⊥}).tilted fun (u : β) => (score w u).toReal

A row of the softmax kernel is the uniform measure on the points of score above ⊥, tilted by the score.

theorem ProbabilityTheory.Kernel.freeEnergy_softmax {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {score : α → β → EReal} {w : α} (htop : ∀ (u : β), score w u ≠ ⊤) (h0 : ∃ (u : β), score w u ≠ ⊥) : (uniformOn {u : β | score w u ≠ ⊥}).freeEnergy (fun (u : β) => (score w u).toReal) ((softmax score) w) = cgf (fun (u : β) => (score w u).toReal) (uniformOn {u : β | score w u ≠ ⊥}) 1

A row of the softmax kernel attains the log partition function as its free energy relative to the uniform measure on the points of score above ⊥.

theorem ProbabilityTheory.Kernel.isGreatest_freeEnergy_softmax {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {score : α → β → EReal} {w : α} (htop : ∀ (u : β), score w u ≠ ⊤) (h0 : ∃ (u : β), score w u ≠ ⊥) : IsGreatest (((uniformOn {u : β | score w u ≠ ⊥}).freeEnergy fun (u : β) => (score w u).toReal) '' {q : MeasureTheory.Measure β | MeasureTheory.IsProbabilityMeasure q ∧ q.AbsolutelyContinuous (uniformOn {u : β | score w u ≠ ⊥}) ∧ MeasureTheory.Integrable (MeasureTheory.llr q (uniformOn {u : β | score w u ≠ ⊥})) q ∧ MeasureTheory.Integrable (fun (u : β) => (score w u).toReal) q}) ((uniformOn {u : β | score w u ≠ ⊥}).freeEnergy (fun (u : β) => (score w u).toReal) ((softmax score) w))

A row of the softmax kernel is the Gibbs optimizer. Among the distributions absolutely continuous with respect to the uniform measure on the points of score above ⊥, it has the greatest expected score less divergence from that uniform measure.