The RSA speaker as a Gibbs (exponentially-tilted) measure

[FG12] [GS13]

Layer 1 of the analytic theory of RSA (Measure/Kernel-native foundation). The pragmatic speaker S1(· | w) is the exponential tilting of a base utterance measure by the rationality-scaled utility score w u = α · (log L0(w | u) − cost u):

S1(· | w) = base.tilted (score w)

i.e. the speaker is a Gibbs measure in mathlib's sense (MeasureTheory.Measure.tilted). This grounds the RSA speaker in mathlib's exponential-family machinery rather than a bespoke PMF.normalize ∘ exp reimplementation, and is the object on which the variational (free-energy / klDiv) characterization is the Gibbs / Donsker–Varadhan variational principle in Core/Probability/GibbsVariational.lean, applied here via speaker_isGreatest.

Main statements

• speaker_count_singleton / speaker_countRestrict_singleton — closed form of the speaker mass at an utterance (softmax over the base / over the applicable set A); speaker_countRestrict_singleton_of_not_mem gives 0 off A.
• speaker_count_lt_iff_score_lt / speaker_lt_iff_score_lt / speaker_countRestrict_lt_iff_score_lt — monotonicity in informativity: the speaker prefers b over a iff its utility is higher. The partition function cancels; reduces to strict monotonicity of Real.exp.
• speakerAlpha — the rationality parameter α (S₁ ∝ L0^α, Boltzmann/softmax at inverse temperature α): speakerAlpha_count_lt_iff_score_lt (α > 0 keeps the order), speakerAlpha_count_zero_singleton (α = 0 is uniform), and the zero-temperature limits speakerAlpha_countRestrict_tendsto_one_of_isMax / _tendsto_zero_of_exists_gt (α → ∞ is the argmax / fully-rational speaker, over the applicable set).
• listener / listener_comp_speaker_marginal / listener_eq_withDensity / listener_region — the pragmatic listener as the Bayesian posterior S1 † prior, stated measure-natively (Bayes consistency, density reweighting, region inference).
• speaker_isGreatest — the RSA speaker is the rational optimizer (Gibbs / Donsker–Varadhan variational principle).

noncomputable def RSA.Gibbs.speaker {U : Type u_1} [MeasurableSpace U] (base : MeasureTheory.Measure U) (score : U → ℝ) : MeasureTheory.Measure U

The RSA pragmatic speaker as an exponentially-tilted (Gibbs) measure: the base utterance measure tilted by the utility score. With score u = α · (log L0(w|u) − cost u) this is S1(· | w) ∝ L0(w|u)^α · exp(−α·cost).

Equations

• RSA.Gibbs.speaker base score = base.tilted score

theorem RSA.Gibbs.speaker_count_singleton {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (score : U → ℝ) (a : U) : (speaker MeasureTheory.Measure.count score) {a} = ENNReal.ofReal (Real.exp (score a) / ∑ u : U, Real.exp (score u))

Closed form of the speaker mass at a single utterance, for the counting base: ofReal (exp (score u) / Z) with partition Z = ∑ u', exp (score u').

theorem RSA.Gibbs.speaker_count_lt_iff_score_lt {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (score : U → ℝ) (a b : U) : (speaker MeasureTheory.Measure.count score) {a} < (speaker MeasureTheory.Measure.count score) {b} ↔ score a < score b

Speaker monotonicity in informativity: at a fixed world, the speaker assigns more mass to b than to a iff b has the higher utility. The partition function cancels exactly; the comparison reduces to the strict monotonicity of Real.exp. The RSA "speaker prefers the more informative utterance" fact, as a theorem about the Gibbs measure.

theorem RSA.Gibbs.speaker_lt_iff_score_lt {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (base : MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure base] (score : U → ℝ) (a b : U) (hmass : base {a} = base {b}) (hpos : base {a} ≠ 0) (hexp : MeasureTheory.Integrable (fun (u : U) => Real.exp (score u)) base) : (speaker base score) {a} < (speaker base score) {b} ↔ score a < score b

Speaker monotonicity, general probability/finite base: for any finite base measure that assigns equal nonzero mass to the two utterances, the speaker prefers b over a iff b has the higher utility. Generalizes speaker_count_lt_iff_score_lt off the counting base — the form the variational principle needs, where the base is a probability measure (e.g. ProbabilityTheory.uniformOn). The shared singleton mass and the partition function Z = ∫ y, exp (score y) ∂base cancel, reducing to Real.exp monotonicity.

An integrability hypothesis on exp ∘ score is required (and is automatic on a Fintype): without it a non-integrable tilt collapses to the zero measure (MeasureTheory.tilted_of_not_integrable), making both sides vanish and the equivalence false. It mirrors the h_exp hypothesis of speaker_isGreatest.

Finite-support speaker (counting base restricted to the applicable set)

The faithful RSA speaker normalizes over only the utterances that apply to the referent ([FG12]'s set W in eq. 2), not the whole utterance type. Tilting Measure.count restricted to a finite applicable set A realizes this: the closed form at an applicable utterance is the softmax over A, and a non-applicable utterance gets mass 0.

theorem RSA.Gibbs.speaker_countRestrict_singleton {U : Type u_1} [Fintype U] [DecidableEq U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (score : U → ℝ) (a : U) (ha : a ∈ A) : (speaker (MeasureTheory.Measure.count.restrict ↑A) score) {a} = ENNReal.ofReal (Real.exp (score a) / ∑ x ∈ A, Real.exp (score x))

Finite-support speaker, closed form: tilting Measure.count restricted to a finite set A gives, at any a ∈ A, the softmax ofReal (exp (score a) / ∑ x ∈ A, exp (score x)) over A. With score u = log (1 / |u|) this is [FG12]'s eq. (2).

theorem RSA.Gibbs.speaker_countRestrict_singleton_of_not_mem {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (score : U → ℝ) (a : U) (ha : a ∉ A) : (speaker (MeasureTheory.Measure.count.restrict ↑A) score) {a} = 0

A non-applicable utterance (a ∉ A) gets zero speaker mass: the finite-support speaker is supported exactly on the applicable set A.

theorem RSA.Gibbs.speaker_countRestrict_lt_iff_score_lt {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (score : U → ℝ) (a b : U) (ha : a ∈ A) (hb : b ∈ A) : (speaker (MeasureTheory.Measure.count.restrict ↑A) score) {a} < (speaker (MeasureTheory.Measure.count.restrict ↑A) score) {b} ↔ score a < score b

Finite-support speaker monotonicity: among applicable utterances, the speaker prefers b over a iff b has the higher utility. The softmax normalizer over A cancels. A specialization of speaker_lt_iff_score_lt to the restricted counting base, with the equal-mass and nonzero side conditions discharged.

Rationality parameter α

The full RSA speaker scales the utility by a rationality parameter α ≥ 0: S₁(· | w) ∝ L0(w | ·)^α, i.e. tilt the base by α · score. α = 1 is the canonical speaker; α → ∞ is the fully-rational argmax speaker (it concentrates on the most informative utterances); α → 0 is the uniform (random) speaker.

noncomputable def RSA.Gibbs.speakerAlpha {U : Type u_1} [MeasurableSpace U] (base : MeasureTheory.Measure U) (α : ℝ) (score : U → ℝ) : MeasureTheory.Measure U

The α-rational speaker: the base tilted by the utility scaled by rationality α. With score = log L0 this is S₁(· | w) ∝ L0(w | ·)^α.

Equations

• RSA.Gibbs.speakerAlpha base α score = RSA.Gibbs.speaker base fun (u : U) => α * score u

@[simp]

theorem RSA.Gibbs.speakerAlpha_one {U : Type u_1} [MeasurableSpace U] (base : MeasureTheory.Measure U) (score : U → ℝ) : speakerAlpha base 1 score = speaker base score

theorem RSA.Gibbs.speakerAlpha_count_singleton {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (α : ℝ) (score : U → ℝ) (a : U) : (speakerAlpha MeasureTheory.Measure.count α score) {a} = ENNReal.ofReal (Real.exp (α * score a) / ∑ u : U, Real.exp (α * score u))

Closed form of the α-speaker over the counting base: the Boltzmann/softmax distribution exp (α · score a) / ∑ u, exp (α · score u) at inverse temperature α.

theorem RSA.Gibbs.speakerAlpha_count_lt_iff_score_lt {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {α : ℝ} (hα : 0 < α) (score : U → ℝ) (a b : U) : (speakerAlpha MeasureTheory.Measure.count α score) {a} < (speakerAlpha MeasureTheory.Measure.count α score) {b} ↔ score a < score b

α-monotonicity (α > 0): any positively-rational speaker prefers the higher-utility utterance. The rationality scaling preserves the order; the partition cancels.

theorem RSA.Gibbs.speakerAlpha_count_zero_singleton {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (score : U → ℝ) (a : U) : (speakerAlpha MeasureTheory.Measure.count 0 score) {a} = ENNReal.ofReal (↑(Fintype.card U))⁻¹

α = 0 is the uniform (indifferent) speaker: with zero rationality the speaker ignores utility and spreads its mass uniformly, (card U)⁻¹ at every utterance.

theorem RSA.Gibbs.speakerAlpha_countRestrict_singleton {U : Type u_1} [Fintype U] [DecidableEq U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (α : ℝ) (score : U → ℝ) (a : U) (ha : a ∈ A) : (speakerAlpha (MeasureTheory.Measure.count.restrict ↑A) α score) {a} = ENNReal.ofReal (Real.exp (α * score a) / ∑ x ∈ A, Real.exp (α * score x))

Closed form of the α-speaker over the applicable set A: the softmax at inverse temperature α restricted to A. Generalizes speakerAlpha_count_singleton (the A = univ case) to the finite-support speaker the studies consume.

theorem RSA.Gibbs.speakerAlpha_countRestrict_singleton_of_not_mem {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (α : ℝ) (score : U → ℝ) (a : U) (ha : a ∉ A) : (speakerAlpha (MeasureTheory.Measure.count.restrict ↑A) α score) {a} = 0

A non-applicable utterance gets zero α-speaker mass.

theorem RSA.Gibbs.speakerAlpha_countRestrict_lt_iff_score_lt {U : Type u_1} [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) {α : ℝ} (hα : 0 < α) (score : U → ℝ) (a b : U) (ha : a ∈ A) (hb : b ∈ A) : (speakerAlpha (MeasureTheory.Measure.count.restrict ↑A) α score) {a} < (speakerAlpha (MeasureTheory.Measure.count.restrict ↑A) α score) {b} ↔ score a < score b

α-monotonicity, finite support (α > 0): over the applicable set A, the positively-rational speaker prefers the higher-utility utterance.

theorem RSA.Gibbs.speakerAlpha_countRestrict_zero_singleton {U : Type u_1} [Fintype U] [DecidableEq U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (score : U → ℝ) (a : U) (ha : a ∈ A) : (speakerAlpha (MeasureTheory.Measure.count.restrict ↑A) 0 score) {a} = ENNReal.ofReal (↑A.card)⁻¹

α = 0 is the uniform speaker over the applicable set: zero rationality spreads mass uniformly across A, (A.card)⁻¹ at each applicable utterance.

theorem RSA.Gibbs.speakerAlpha_countRestrict_tendsto_one_of_isMax {U : Type u_1} [Fintype U] [DecidableEq U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (score : U → ℝ) (a : U) (ha : a ∈ A) (hmax : ∀ b ∈ A, b ≠ a → score b < score a) : Filter.Tendsto (fun (α : ℝ) => (speakerAlpha (MeasureTheory.Measure.count.restrict ↑A) α score) {a}) Filter.atTop (nhds 1)

α → ∞ concentrates on the unique best applicable utterance: if a strictly maximizes the utility over the applicable set A, the fully-rational speaker assigns it mass → 1. The softmax becomes the argmax (zero-temperature limit).

theorem RSA.Gibbs.speakerAlpha_countRestrict_tendsto_zero_of_exists_gt {U : Type u_1} [Fintype U] [DecidableEq U] [MeasurableSpace U] [MeasurableSingletonClass U] (A : Finset U) (score : U → ℝ) (a : U) (ha : a ∈ A) (hbeat : ∃ b ∈ A, score a < score b) : Filter.Tendsto (fun (α : ℝ) => (speakerAlpha (MeasureTheory.Measure.count.restrict ↑A) α score) {a}) Filter.atTop (nhds 0)

α → ∞ abandons a dominated utterance: if some applicable utterance strictly beats a, the fully-rational speaker assigns a mass → 0. Dual to speakerAlpha_countRestrict_tendsto_one_of_isMax.

The pragmatic listener as a Bayesian posterior (measure-native)

The pragmatic listener L1 is the Bayesian posterior of the speaker kernel S1 : Kernel World Utterance against the world prior — mathlib's ProbabilityTheory.posterior, S1 † prior : Kernel Utterance World. This is the listener stated measure-natively: it is a kernel/measure, characterized by Bayes-consistency rather than by pointwise singleton values, so it is uniform across discrete and continuous distribution classes (where singletons are null and a pointwise reading is unavailable).

noncomputable def RSA.Gibbs.listener {W : Type u_2} {U : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [StandardBorelSpace W] [Nonempty W] (S1 : ProbabilityTheory.Kernel W U) (prior : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure prior] [ProbabilityTheory.IsFiniteKernel S1] : ProbabilityTheory.Kernel U W

The RSA pragmatic listener: the Bayesian posterior S1 † prior of the speaker kernel against the world prior.

Equations

• RSA.Gibbs.listener S1 prior = ProbabilityTheory.posterior S1 prior

theorem RSA.Gibbs.listener_comp_speaker_marginal {W : Type u_2} {U : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [StandardBorelSpace W] [Nonempty W] (S1 : ProbabilityTheory.Kernel W U) (prior : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure prior] [ProbabilityTheory.IsMarkovKernel S1] : (prior.bind ⇑S1).bind ⇑(listener S1 prior) = prior

Listener–speaker consistency (measure-native): averaging the listener over the speaker's marginal of the prior recovers the prior, L1 ∘ₘ (S1 ∘ₘ prior) = prior. The Bayesian-coherence identity for RSA, as an equality of measures — no singletons, any distribution class.

Bayes' theorem and region inference (measure-native)

theorem RSA.Gibbs.listener_eq_withDensity {W : Type u_2} {U : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [Countable W] [StandardBorelSpace W] [Nonempty W] (S1 : ProbabilityTheory.Kernel W U) (prior : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure prior] [ProbabilityTheory.IsFiniteKernel S1] : ∀ᵐ (u : U) ∂prior.bind ⇑S1, (listener S1 prior) u = prior.withDensity fun (w : W) => (S1 w).rnDeriv (prior.bind ⇑S1) u

Bayes' theorem for the RSA listener: for almost every utterance u, the listener is the prior reweighted by the per-world speaker likelihood-ratio, L1 u = prior.withDensity (fun w ↦ (S1 w).rnDeriv (S1 ∘ₘ prior) u). The posterior is the prior tilted by how diagnostic each world is for u. For countable worlds the absolute-continuity side condition is automatic.

theorem RSA.Gibbs.listener_region {W : Type u_2} {U : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [Countable W] [StandardBorelSpace W] [Nonempty W] (S1 : ProbabilityTheory.Kernel W U) (prior : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure prior] [ProbabilityTheory.IsFiniteKernel S1] {A : Set W} (hA : MeasurableSet A) : ∀ᵐ (u : U) ∂prior.bind ⇑S1, ((listener S1 prior) u) A = ∫⁻ (w : W) in A, (S1 w).rnDeriv (prior.bind ⇑S1) u ∂prior

Region inference: the listener's posterior mass on a set of worlds A given utterance u is the integral of the speaker likelihood-ratio over A. This is the measure-native quantity behind RSA "the listener infers φ" claims (projection, exhaustivity = posterior mass on the relevant region of worlds) — stated at the level of sets, where it is meaningful for any distribution class, rather than at points.

The RSA speaker is the rational optimizer

speaker base score = base.tilted score is a Gibbs measure, so the Gibbs / Donsker–Varadhan variational principle (InformationTheory.isGreatest_cgf, proved generically in Core/Probability/GibbsVariational.lean) applies directly: among all candidate distributions over utterances, the speaker maximizes the free energy 𝔼_q[score] − KL(q ‖ base), with optimal value the cumulant generating function cgf score base 1 (= log ∫ exp score ∂base, the free energy / log-partition). This turns RSA's "rational speaker" from a stipulated softmax into a theorem.

theorem RSA.Gibbs.speaker_isGreatest {U : Type u_1} [MeasurableSpace U] (base : MeasureTheory.Measure U) [MeasureTheory.IsProbabilityMeasure base] (score : U → ℝ) (h_int_f : MeasureTheory.Integrable score (speaker base score)) (h_int_llr : MeasureTheory.Integrable (MeasureTheory.llr (speaker base score) base) (speaker base score)) (h_exp : MeasureTheory.Integrable (fun (u : U) => Real.exp (score u)) base) : IsGreatest (base.freeEnergy score '' {q : MeasureTheory.Measure U | MeasureTheory.IsProbabilityMeasure q ∧ q.AbsolutelyContinuous base ∧ MeasureTheory.Integrable (MeasureTheory.llr q base) q ∧ MeasureTheory.Integrable score q}) (ProbabilityTheory.cgf score base 1)

The RSA speaker is the rational optimizer: cgf score base 1 is the greatest value of the free-energy functional base.freeEnergy score over candidate utterance distributions, attained at speaker base score = base.tilted score. A direct instance of the Gibbs / Donsker–Varadhan variational principle InformationTheory.isGreatest_cgf.