The Rational Speech Act pipeline on probability kernels

This file defines the Rational Speech Act model in mathlib's probability vocabulary, following Frank and Goodman's model as presented in Degen's review (eqs. 1–4) and in Franke and Bergen's comparison of latent-variable variants (eqs. 5–22). The speaker believes a measure on states and is the softmax of the expected log of the listener's mass under that belief less a real cost, scaled by the rationality, so that Frank and Goodman's speaker, who knows the state, believes the point mass there. The listener holds a prior over states and reweights it by the mass each state's measure gives the utterance heard. At the channel of a speaker who is only truthful she is the literal listener, who conditions the prior on the extension of the utterance, and at a speaker she is the pragmatic listener, mathlib's posterior kernel wherever the utterance is heard; the listener of a graded meaning is the density kernel Kernel.ofDensity. A latent the speaker also knows is a coordinate of the state, and so is the speaker's choice when the listener hears only its form: her prior is then the joint of the world prior and the speaker. A speaker whose utility is not an expected log-probability, such as a question- or politeness-weighted one, is the softmax kernel Kernel.softmax of her score, with ⊥ marking the utterances she cannot use. Rationality, cost, meaning, and prior are arguments, so findings quantify over them. Boolean meanings at a uniform prior on finitely many states, where masses reduce to counting, are treated in Linglib.Pragmatics.RSA.Uniform.

Main definitions

• RSA.listener: the prior reweighted by the mass each state's measure gives the utterance heard, and normalized. At the channel RSA.truthful sem of a speaker who is only truthful it is eq. 1, the prior conditioned on the denotation of the utterance.
• RSA.speaker: the softmax of the expected log of the listener's mass under the speaker's belief, less a cost. Its weights are the geometric mean of the listener's mass over the belief to the power α, times exp (-(α * C)); at the point-mass belief it is the speaker of eqs. 2/6–7, with weights L ^ α * exp (-(α * C)) (RSA.speaker_dirac_eq_ofWeights).

Main results

• RSA.speaker_apply_singleton_eq_zero_iff: the speaker produces exactly the utterances whose listener rules out no state she entertains.
• RSA.listener_prod_fst: lexical uncertainty. Against independent priors over states and a latent, the state marginal of the joint listener is the listener of the speaker averaged over the latent.
• RSA.speaker_ofDensity_apply_singleton: against the listener of a graded meaning the prior cancels from the speaker's choice, and she weighs an utterance by the geometric mean of its meaning over her belief and the inverse of the meaning's prior mass.
• RSA.tendsto_speaker_dirac_real_singleton_atTop: as rationality grows the speaker puts all its mass on the utterance the listener most favors.

References

• M. C. Frank and N. D. Goodman, Predicting Pragmatic Reasoning in Language Games (2012)
• J. Degen, The Rational Speech Act Framework (2023)
• L. Bergen, R. Levy and N. D. Goodman, Pragmatic Reasoning through Semantic Inference (2016)
• M. Franke and L. Bergen, Theory-Driven Statistical Modeling for Semantics and Pragmatics: A Case Study on Grammatically Generated Implicature Readings (2020)

The RSA pipeline

noncomputable def RSA.truthful {W : Type u_1} {U : Type u_2} [MeasurableSpace U] (sem : U → Set W) (w : W) : MeasureTheory.Measure U

The channel of a speaker who is only required to be truthful. The denotation sem gives each utterance the set of states it is true at, and the channel puts mass one on each utterance true at the state. For utterances that denote sets of states, sem is fun u ↦ ⟦u⟧, and its value at a lexicon, a threshold or a context when the denotation depends on one.

Equations

• RSA.truthful sem w = MeasureTheory.Measure.count.restrict {u : U | w ∈ sem u}

instance RSA.instIsFiniteMeasureTruthfulOfFinite {W : Type u_1} {U : Type u_2} [MeasurableSpace U] [Finite U] (sem : U → Set W) (w : W) : MeasureTheory.IsFiniteMeasure (truthful sem w)

theorem RSA.truthful_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace U] [MeasurableSingletonClass U] (sem : U → Set W) (w : W) (u : U) : (truthful sem w) {u} = (sem u).indicator 1 w

The listener

A listener holds a prior over states and takes the utterance to come from a channel, a measure on utterances at each state. She reweights the prior by the mass each state's measure gives the utterance she hears and normalizes, which is Bayes' rule with the zero measure at an utterance no state she entertains produces. The literal listener (eq. 1) takes the speaker to be truthful and no more, and so conditions the prior on the denotation of the utterance. The pragmatic listener (eq. 3) takes the channel of a speaker, and is mathlib's posterior wherever the utterance is heard.

noncomputable def RSA.listener {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) : ProbabilityTheory.Kernel U W

The listener reweights the prior μ by the mass each state's measure S w gives the utterance heard, and normalizes. Her row at an utterance that no state of positive prior produces is the zero measure.

Equations

• RSA.listener μ S = ProbabilityTheory.Kernel.ofDensity μ fun (u : U) (w : W) => (S w) {u}

theorem RSA.listener_apply {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) (u : U) : (listener μ S) u = (μ.withDensity fun (w : W) => (S w) {u})[|Set.univ]

instance RSA.instIsZeroOrProbabilityMeasureCoeKernelMeasureListener {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) (u : U) : MeasureTheory.IsZeroOrProbabilityMeasure ((listener μ S) u)

instance RSA.instIsFiniteKernelListener {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) : ProbabilityTheory.IsFiniteKernel (listener μ S)

theorem RSA.listener_apply_singleton' {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasurableSingletonClass W] (u : U) (w : W) : ((listener μ S) u) {w} = (S w) {u} * μ {w} / ∫⁻ (w' : W), (S w') {u} ∂μ

theorem RSA.listener_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasurableSingletonClass W] [Fintype W] (u : U) (w : W) : ((listener μ S) u) {w} = (S w) {u} * μ {w} / ∑ w' : W, (S w') {u} * μ {w'}

theorem RSA.listener_apply_singleton_of_equiv {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasurableSingletonClass W] [Fintype W] {W' : Type u_4} {U' : Type u_5} [MeasurableSpace W'] [MeasurableSpace U'] [Countable U'] [MeasurableSingletonClass U'] [Fintype W'] [MeasurableSingletonClass W'] (e : W ≃ W') {μ' : MeasureTheory.Measure W'} {S' : W' → MeasureTheory.Measure U'} {u : U} {u' : U'} (hμ : ∀ (w : W), μ' {e w} = μ {w}) (hS : ∀ (w : W), (S' (e w)) {u'} = (S w) {u}) (w : W) : ((listener μ' S') u') {e w} = ((listener μ S) u) {w}

A relabelling of the states that carries one prior and channel to another carries the listener along.

theorem RSA.listener_apply_singleton_eq_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure W} {S : W → MeasureTheory.Measure U} [MeasurableSingletonClass W] [Fintype W] {u : U} {w : W} (h : (S w) {u} = 0) : ((listener μ S) u) {w} = 0

A state whose measure gives the utterance no mass gets none from the listener.

theorem RSA.ne_zero_of_listener_apply_singleton_ne_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure W} {S : W → MeasureTheory.Measure U} [MeasurableSingletonClass W] [Fintype W] {u : U} {w : W} (h : ((listener μ S) u) {w} ≠ 0) : μ {w} ≠ 0 ∧ (S w) {u} ≠ 0

A state the listener gives mass has positive prior and produces the utterance.

theorem RSA.listener_apply_singleton_ne_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure W} {S : W → MeasureTheory.Measure U} [MeasurableSingletonClass W] [Fintype W] {u : U} {w : W} [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (hμ : μ {w} ≠ 0) (hS : (S w) {u} ≠ 0) : ((listener μ S) u) {w} ≠ 0

The listener gives mass to a state of positive prior that produces the utterance.

theorem RSA.listener_apply_singleton_ne_zero_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure W} {S : W → MeasureTheory.Measure U} [MeasurableSingletonClass W] [Fintype W] {u : U} {w : W} [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] : ((listener μ S) u) {w} ≠ 0 ↔ μ {w} ≠ 0 ∧ (S w) {u} ≠ 0

The listener puts mass on a state exactly when it has positive prior and produces the utterance.

Events

Bayes' rule on reals, for the mass of a state and of a finite event. It holds at every utterance, since an utterance that no state of positive prior produces gives the zero row and a zero normalizer.

theorem RSA.listener_apply_singleton_congr {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) {u : U} {w₁ w₂ : W} (hS : (S w₁) {u} = (S w₂) {u}) (hμ : μ {w₁} = μ {w₂}) : ((listener μ S) u) {w₁} = ((listener μ S) u) {w₂}

Two states with the same prior mass that produce the utterance alike get the same mass.

theorem RSA.listener_apply_finset {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) (u : U) (E : Finset W) : ((listener μ S) u) ↑E = (∑ w ∈ E, (S w) {u} * μ {w}) / ∑ w : W, (S w) {u} * μ {w}

theorem RSA.isProbabilityMeasure_listener_of_ne_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] {u : U} {w : W} (hμ : μ {w} ≠ 0) (hS : (S w) {u} ≠ 0) : MeasureTheory.IsProbabilityMeasure ((listener μ S) u)

The listener's row is a probability measure at an utterance that some state of positive prior produces.

theorem RSA.listener_real_finset {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (u : U) (E : Finset W) : ((listener μ S) u).real ↑E = (∑ w ∈ E, μ.real {w} * (S w).real {u}) / ∑ w : W, μ.real {w} * (S w).real {u}

Bayes' rule on reals for an event. Both sides vanish at an utterance that no state of positive prior produces.

theorem RSA.listener_real_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (u : U) (w : W) : ((listener μ S) u).real {w} = μ.real {w} * (S w).real {u} / ∑ w' : W, μ.real {w'} * (S w').real {u}

Bayes' rule on reals at a state.

theorem RSA.listener_real_finset_lt_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (u : U) (E₁ E₂ : Finset W) : ((listener μ S) u).real ↑E₁ < ((listener μ S) u).real ↑E₂ ↔ ∑ w ∈ E₁, μ.real {w} * (S w).real {u} < ∑ w ∈ E₂, μ.real {w} * (S w).real {u}

The listener prefers the event with the greater prior-weighted production probability, at every utterance, heard or not.

theorem RSA.listener_real_singleton_lt_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (u : U) (w₁ w₂ : W) : ((listener μ S) u).real {w₁} < ((listener μ S) u).real {w₂} ↔ μ.real {w₁} * (S w₁).real {u} < μ.real {w₂} * (S w₂).real {u}

The listener prefers the state with the greater prior mass times production probability, at every utterance, heard or not.

theorem RSA.listener_real_lt_of_certain {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] {u : U} {E₁ E₂ : Finset W} {w₀ : W} (hw₀ : w₀ ∈ E₂) (hle : ∀ (w : W), (S w).real {u} ≤ 1) (hs : (S w₀) {u} = 1) (hlt : ∑ w ∈ E₁, μ.real {w} < μ.real {w₀}) : ((listener μ S) u).real ↑E₁ < ((listener μ S) u).real ↑E₂

A state producing the utterance with certainty outweighs any event of smaller total prior mass, when no state produces it with probability above one.

theorem RSA.listener_real_singleton_lt_iff_of_forall_eq {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (S : W → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (hμeq : ∀ (w w' : W), μ {w} = μ {w'}) (hμ0 : ∀ (w : W), μ {w} ≠ 0) (u : U) (w₁ w₂ : W) : ((listener μ S) u).real {w₁} < ((listener μ S) u).real {w₂} ↔ (S w₁).real {u} < (S w₂).real {u}

At a prior giving every state the same positive mass, the listener ranks two states as they produce the utterance.

The uniform prior

Against the uniform prior the prior cancels, and the listener's mass on a state is its share of the production probability of the utterance.

theorem RSA.listener_uniformOn_univ_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (S : W → MeasureTheory.Measure U) [Nonempty W] (u : U) (w : W) : ((listener (ProbabilityTheory.uniformOn Set.univ) S) u) {w} = (S w) {u} / ∑ w' : W, (S w') {u}

theorem RSA.listener_uniformOn_univ_real_finset {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (S : W → MeasureTheory.Measure U) [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] [Nonempty W] (u : U) (E : Finset W) : ((listener (ProbabilityTheory.uniformOn Set.univ) S) u).real ↑E = (∑ w ∈ E, (S w).real {u}) / ∑ w : W, (S w).real {u}

theorem RSA.listener_uniformOn_real_lt_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (S : W → MeasureTheory.Measure U) [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (u : U) (w₁ w₂ : W) : ((listener (ProbabilityTheory.uniformOn Set.univ) S) u).real {w₁} < ((listener (ProbabilityTheory.uniformOn Set.univ) S) u).real {w₂} ↔ (S w₁).real {u} < (S w₂).real {u}

Against the uniform prior the listener ranks two states as they produce the utterance.

theorem RSA.listener_uniformOn_real_le_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (S : W → MeasureTheory.Measure U) [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (u : U) (w₁ w₂ : W) : ((listener (ProbabilityTheory.uniformOn Set.univ) S) u).real {w₁} ≤ ((listener (ProbabilityTheory.uniformOn Set.univ) S) u).real {w₂} ↔ (S w₁).real {u} ≤ (S w₂).real {u}

theorem RSA.listener_uniformOn_real_finset_lt_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (S : W → MeasureTheory.Measure U) [∀ (w : W), MeasureTheory.IsFiniteMeasure (S w)] (u : U) (E₁ E₂ : Finset W) : ((listener (ProbabilityTheory.uniformOn Set.univ) S) u).real ↑E₁ < ((listener (ProbabilityTheory.uniformOn Set.univ) S) u).real ↑E₂ ↔ ∑ w ∈ E₁, (S w).real {u} < ∑ w ∈ E₂, (S w).real {u}

Against the uniform prior the listener ranks two events as their states together produce the utterance.

Marginals of a listener over a product

A latent the speaker also knows, a lexicon or a threshold or a question, is a coordinate of the state: the speaker at a pair is fun p ↦ speaker α C (L p.2) Measure.dirac p.1, addressing that latent's listener, and her listener holds a prior over pairs. Its marginals pool the prior-weighted production probabilities over the other coordinate. When the prior over pairs is a product, forgetting the latent after the joint inference is inverting the speaker averaged over the latent, so the two presentations of lexical uncertainty agree (listener_prod_fst).

theorem RSA.listener_fst_apply_singleton_ne_zero_iff {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (a : A) : ((listener μ S) u).fst {a} ≠ 0 ↔ ∃ (b : B), μ {(a, b)} ≠ 0 ∧ (S (a, b)) {u} ≠ 0

The first marginal of the listener is positive at a point exactly when some second coordinate pairs a positive prior with a positive production probability.

theorem RSA.listener_snd_apply_singleton_ne_zero_iff {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (b : B) : ((listener μ S) u).snd {b} ≠ 0 ↔ ∃ (a : A), μ {(a, b)} ≠ 0 ∧ (S (a, b)) {u} ≠ 0

theorem RSA.listener_fst_real_singleton {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (a : A) : ((listener μ S) u).fst.real {a} = (∑ b : B, μ.real {(a, b)} * (S (a, b)).real {u}) / ∑ p : A × B, μ.real {p} * (S p).real {u}

The first marginal of the listener pools the prior-weighted production probabilities over the second coordinate.

theorem RSA.listener_snd_real_singleton {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (b : B) : ((listener μ S) u).snd.real {b} = (∑ a : A, μ.real {(a, b)} * (S (a, b)).real {u}) / ∑ p : A × B, μ.real {p} * (S p).real {u}

theorem RSA.listener_fst_real_lt_iff {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (a₁ a₂ : A) : ((listener μ S) u).fst.real {a₁} < ((listener μ S) u).fst.real {a₂} ↔ ∑ b : B, μ.real {(a₁, b)} * (S (a₁, b)).real {u} < ∑ b : B, μ.real {(a₂, b)} * (S (a₂, b)).real {u}

Comparing first marginals of the listener compares the prior-weighted production probabilities pooled over the second coordinate.

theorem RSA.listener_snd_real_lt_iff {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (b₁ b₂ : B) : ((listener μ S) u).snd.real {b₁} < ((listener μ S) u).snd.real {b₂} ↔ ∑ a : A, μ.real {(a, b₁)} * (S (a, b₁)).real {u} < ∑ a : A, μ.real {(a, b₂)} * (S (a, b₂)).real {u}

theorem RSA.listener_prod_fst {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μA : MeasureTheory.Measure A) (ν : MeasureTheory.Measure B) (S : A × B → MeasureTheory.Measure U) : (listener (μA.prod ν) S).fst = listener μA fun (a : A) => ∑ b : B, ν {b} • S (a, b)

Lexical uncertainty. Against a product prior, the first marginal of the listener is the listener of the speaker averaged over the second coordinate by its prior.

theorem RSA.listener_prod_fst_real_singleton {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μA : MeasureTheory.Measure A) [MeasureTheory.IsFiniteMeasure μA] (ν : MeasureTheory.Measure B) [MeasureTheory.IsFiniteMeasure ν] (S : A × B → MeasureTheory.Measure U) [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (a : A) : ((listener (μA.prod ν) S) u).fst.real {a} = (μA.real {a} * ∑ b : B, ν.real {b} * (S (a, b)).real {u}) / ∑ p : A × B, (μA.prod ν).real {p} * (S p).real {u}

Against a product prior the first marginal of the listener is the prior at the point times the production probability averaged over the second coordinate, normalized.

theorem RSA.listener_fst_real_lt_iff_of_forall_eq {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (hμeq : ∀ (p q : A × B), μ {p} = μ {q}) (hμ0 : ∀ (p : A × B), μ {p} ≠ 0) (u : U) (a₁ a₂ : A) : ((listener μ S) u).fst.real {a₁} < ((listener μ S) u).fst.real {a₂} ↔ ∑ b : B, (S (a₁, b)).real {u} < ∑ b : B, (S (a₂, b)).real {u}

At a prior giving every pair the same positive mass, the first marginal of the listener prefers the point with the greater production probability summed over the second coordinate.

theorem RSA.listener_snd_real_lt_iff_of_forall_eq {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {A : Type u_4} {B : Type u_5} [MeasurableSpace A] [MeasurableSpace B] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure (A × B)) (S : A × B → MeasureTheory.Measure U) [MeasureTheory.IsFiniteMeasure μ] [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (hμeq : ∀ (p q : A × B), μ {p} = μ {q}) (hμ0 : ∀ (p : A × B), μ {p} ≠ 0) (u : U) (b₁ b₂ : B) : ((listener μ S) u).snd.real {b₁} < ((listener μ S) u).snd.real {b₂} ↔ ∑ a : A, (S (a, b₁)).real {u} < ∑ a : A, (S (a, b₂)).real {u}

At a prior giving every pair the same positive mass, the second marginal of the listener prefers the point with the greater production probability summed over the first coordinate.

The listener of a kernel

When the channel is a kernel, the normalizer is the marginal probability of the utterance, the listener is a probability measure exactly at the utterances that are heard, and there she is mathlib's posterior.

theorem RSA.listener_apply_singleton_eq_div {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (κ : ProbabilityTheory.Kernel W U) (u : U) (w : W) : ((listener μ ⇑κ) u) {w} = μ {w} * (κ w) {u} / (μ.bind ⇑κ) {u}

Bayes' rule holds at every utterance. The listener's mass on a state is its prior times the mass its row gives the utterance, over the utterance's marginal.

theorem RSA.isProbabilityMeasure_listener {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (κ : ProbabilityTheory.Kernel W U) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] {u : U} (hu : (μ.bind ⇑κ) {u} ≠ 0) : MeasureTheory.IsProbabilityMeasure ((listener μ ⇑κ) u)

The listener's row at a heard utterance is a probability measure.

theorem RSA.isMarkovKernel_listener {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (κ : ProbabilityTheory.Kernel W U) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] (h : ∀ (u : U), (μ.bind ⇑κ) {u} ≠ 0) : ProbabilityTheory.IsMarkovKernel (listener μ ⇑κ)

The listener is a probability kernel when every utterance is heard.

theorem RSA.comp_real_mul_listener_real {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (κ : ProbabilityTheory.Kernel W U) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] (u : U) (w : W) : (μ.bind ⇑κ).real {u} * ((listener μ ⇑κ) u).real {w} = μ.real {w} * (κ w).real {u}

At every state and utterance, the utterance's marginal times the listener is the prior times the production, Bayes' rule on reals with the denominator cleared. Both sides vanish at an utterance that is not heard.

theorem RSA.listener_apply_eq_posterior {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [Fintype W] [MeasurableSingletonClass W] (μ : MeasureTheory.Measure W) (κ : ProbabilityTheory.Kernel W U) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [StandardBorelSpace W] [Nonempty W] {u : U} (hu : (μ.bind ⇑κ) {u} ≠ 0) : (listener μ ⇑κ) u = (ProbabilityTheory.posterior κ μ) u

At a heard utterance the listener is the posterior, by Bayes' rule.

theorem RSA.listener_dirac_apply {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) {f : W → U} (hf : Measurable f) (u : U) : (listener μ fun (w : W) => MeasureTheory.Measure.dirac (f w)) u = μ[|f ⁻¹' {u}]

A listener who hears a function of the state conditions the prior on its fibre.

The listener of a truthful speaker

theorem RSA.listener_truthful_eq_ofDensity {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (sem : U → Set W) : listener μ (truthful sem) = ProbabilityTheory.Kernel.ofDensity μ fun (u : U) => (sem u).indicator 1

The listener of a truthful speaker is the density kernel of the indicator of the denotation against the prior.

theorem RSA.listener_truthful_apply' {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (sem : U → Set W) (u : U) (hs : MeasurableSet (sem u)) : (listener μ (truthful sem)) u = μ[|sem u]

The listener of a truthful speaker (eq. 1) conditions the prior on the denotation of the utterance.

theorem RSA.listener_truthful_apply {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) (u : U) : (listener μ (truthful sem)) u = μ[|sem u]

theorem RSA.listener_truthful_apply_univ {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) [MeasureTheory.IsFiniteMeasure μ] {u : U} (h : μ (sem u) ≠ 0) : ((listener μ (truthful sem)) u) Set.univ = 1

The listener of a truthful speaker is a probability measure at an utterance whose denotation has positive prior mass.

theorem RSA.listener_truthful_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) {u : U} {w : W} (h : w ∈ sem u) : ((listener μ (truthful sem)) u) {w} = (μ (sem u))⁻¹ * μ {w}

theorem RSA.listener_truthful_apply_singleton_of_notMem {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) {u : U} {w : W} (h : w ∉ sem u) : ((listener μ (truthful sem)) u) {w} = 0

theorem RSA.listener_truthful_real_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) {u : U} {w : W} (h : w ∈ sem u) : ((listener μ (truthful sem)) u).real {w} = μ.real {w} / μ.real (sem u)

On reals the listener of a truthful speaker gives a state the utterance is true at its share of the prior mass of the denotation.

theorem RSA.listener_truthful_apply_singleton_of_eq_univ {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) [MeasureTheory.IsProbabilityMeasure μ] {u : U} (h : sem u = Set.univ) (w : W) : ((listener μ (truthful sem)) u) {w} = μ {w}

A tautology leaves a probability prior unchanged.

theorem RSA.listener_truthful_apply_singleton_of_eq_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) [MeasureTheory.IsFiniteMeasure μ] {u : U} {w : W} (h : sem u = {w}) (hμ : μ {w} ≠ 0) : ((listener μ (truthful sem)) u) {w} = 1

An utterance true at one state only puts all its mass there.

theorem RSA.listener_truthful_apply_singleton_ne_zero_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (μ : MeasureTheory.Measure W) (sem : U → Set W) [MeasureTheory.IsFiniteMeasure μ] (u : U) (w : W) : ((listener μ (truthful sem)) u) {w} ≠ 0 ↔ w ∈ sem u ∧ μ {w} ≠ 0

The listener of a truthful speaker puts mass on a state exactly when the utterance is true there and the state has positive prior.

theorem RSA.listener_truthful_apply_singleton_of_equiv {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] {W' : Type u_4} {U' : Type u_5} [MeasurableSpace W'] [DiscreteMeasurableSpace W'] [MeasurableSpace U'] [Countable U'] [MeasurableSingletonClass U'] [Fintype W] [Fintype W'] (e : W ≃ W') {μ : MeasureTheory.Measure W} {μ' : MeasureTheory.Measure W'} {sem : U → Set W} {sem' : U' → Set W'} {u : U} {u' : U'} (hμ : ∀ (w : W), μ' {e w} = μ {w}) (hsem : ∀ (w : W), e w ∈ sem' u' ↔ w ∈ sem u) (w : W) : ((listener μ' (truthful sem')) u') {e w} = ((listener μ (truthful sem)) u) {w}

A relabelling of the states that carries one prior and denotation to another carries the listener of a truthful speaker along.

The speaker

A speaker believes a measure on states and addresses a listener. Her weight for an utterance is the exponential of the rationality times its utility: the expected log of the listener's mass under her belief, less a real cost. Written without logarithms, the weight is the geometric mean of the listener's mass over her belief, to the power of the rationality, times the cost weight exp (-(α * C u)).

noncomputable def RSA.speaker {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) (b : O → MeasureTheory.Measure W) : ProbabilityTheory.Kernel O U

The speaker at rationality α and cost C addresses the listener L and at o believes b o. Her weight for an utterance is the geometric mean of its listener's mass over her belief, to the power α, times the cost weight.

Equations

• RSA.speaker α C L b = ProbabilityTheory.Kernel.ofWeights fun (o : O) (u : U) => ((b o).geomMean fun (w : W) => (L u) {w}) ^ α * ENNReal.ofReal (Real.exp (-(α * C u)))

instance RSA.instIsFiniteKernelSpeaker {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) (b : O → MeasureTheory.Measure W) : ProbabilityTheory.IsFiniteKernel (speaker α C L b)

theorem RSA.speaker_apply_univ_le_one {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) (b : O → MeasureTheory.Measure W) (o : O) : ((speaker α C L b) o) Set.univ ≤ 1

A speaker row has total mass at most one.

theorem RSA.speaker_real_singleton_le_one {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) (b : O → MeasureTheory.Measure W) (o : O) (u : U) : ((speaker α C L b) o).real {u} ≤ 1

Speaker shares are at most one.

theorem RSA.speaker_apply_singleton {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) (b : O → MeasureTheory.Measure W) (o : O) [MeasurableSingletonClass U] (u : U) : ((speaker α C L b) o) {u} = ((b o).geomMean fun (w : W) => (L u) {w}) ^ α * ENNReal.ofReal (Real.exp (-(α * C u))) / ∑ u' : U, ((b o).geomMean fun (w : W) => (L u') {w}) ^ α * ENNReal.ofReal (Real.exp (-(α * C u')))

theorem RSA.sum_speaker_real_singleton_le_one {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) (b : O → MeasureTheory.Measure W) (o : O) [MeasurableSingletonClass U] (S : Finset U) : ∑ u ∈ S, ((speaker α C L b) o).real {u} ≤ 1

Speaker shares over any set of utterances sum to at most one.

theorem RSA.speaker_real_singleton_lt_one {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} [MeasurableSingletonClass U] [DecidableEq U] {u u' : U} (hne : u' ≠ u) (h : ((speaker α C L b) o) {u'} ≠ 0) : ((speaker α C L b) o).real {u} < 1

Another utterance of positive mass keeps a share strictly below one.

theorem RSA.isProbabilityMeasure_speaker {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} [∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)] (hα : 0 ≤ α) (h0 : ∃ (u : U), ∀ (w : W), (b o) {w} ≠ 0 → (L u) {w} ≠ 0) : MeasureTheory.IsProbabilityMeasure ((speaker α C L b) o)

The speaker's row is a probability measure at an observation where some utterance's listener rules out no state she entertains.

theorem RSA.isMarkovKernel_speaker {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} [∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)] (hα : 0 ≤ α) (h0 : ∀ (o : O), ∃ (u : U), ∀ (w : W), (b o) {w} ≠ 0 → (L u) {w} ≠ 0) : ProbabilityTheory.IsMarkovKernel (speaker α C L b)

The speaker is a probability kernel when at every observation some utterance's listener rules out no state she entertains.

theorem RSA.speaker_apply_singleton_ne_zero {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} {u : U} [∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)] [MeasurableSingletonClass U] (hα : 0 ≤ α) (h : ∀ (w : W), (b o) {w} ≠ 0 → (L u) {w} ≠ 0) : ((speaker α C L b) o) {u} ≠ 0

An utterance whose listener rules out no state she entertains is produced with positive mass.

theorem RSA.speaker_real_singleton_lt_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} [∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)] [MeasurableSingletonClass U] (hα : 0 ≤ α) (h0 : ∃ (u : U), ∀ (w : W), (b o) {w} ≠ 0 → (L u) {w} ≠ 0) {u u' : U} : ((speaker α C L b) o).real {u} < ((speaker α C L b) o).real {u'} ↔ ((b o).geomMean fun (w : W) => (L u) {w}) ^ α * ENNReal.ofReal (Real.exp (-(α * C u))) < ((b o).geomMean fun (w : W) => (L u') {w}) ^ α * ENNReal.ofReal (Real.exp (-(α * C u')))

Row preference of the speaker compares the weights; the normalization cancels.

theorem RSA.speaker_apply_singleton_eq_zero_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [Fintype U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} {u : U} [∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)] [MeasurableSingletonClass U] [MeasureTheory.IsFiniteMeasure (b o)] (hα : 0 < α) : ((speaker α C L b) o) {u} = 0 ↔ ∃ (w : W), (b o) {w} ≠ 0 ∧ (L u) {w} = 0

The speaker never produces an utterance whose listener rules out a state she entertains.

The speaker against a graded meaning

The listener of a graded meaning reweights the prior by the meaning of the utterance. The prior, which no utterance changes, cancels from the speaker's choice, and she weighs an utterance by the geometric mean of its meaning over her belief against the meaning's prior mass.

theorem RSA.speaker_ofDensity_apply_singleton {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {b : O → MeasureTheory.Measure W} {o : O} {μ : MeasureTheory.Measure W} {m : U → W → ENNReal} [MeasureTheory.IsFiniteMeasure μ] (hα : 0 ≤ α) [MeasureTheory.IsProbabilityMeasure (b o)] (hb : (b o).AbsolutelyContinuous μ) (u : U) : ((speaker α C (⇑(ProbabilityTheory.Kernel.ofDensity μ m)) b) o) {u} = (b o).geomMean (m u) ^ α * ((∑ w : W, m u w * μ {w})⁻¹ ^ α * ENNReal.ofReal (Real.exp (-(α * C u)))) / ∑ u' : U, (b o).geomMean (m u') ^ α * ((∑ w : W, m u' w * μ {w})⁻¹ ^ α * ENNReal.ofReal (Real.exp (-(α * C u'))))

Against the listener of a graded meaning the speaker weighs an utterance by the geometric mean of its meaning over her belief and by the inverse of the meaning's prior mass.

theorem RSA.speaker_ofDensity_apply_congr {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {b : O → MeasureTheory.Measure W} {μ : MeasureTheory.Measure W} {m : U → W → ENNReal} [MeasureTheory.IsFiniteMeasure μ] (hα : 0 ≤ α) {o₁ o₂ : O} [MeasureTheory.IsProbabilityMeasure (b o₁)] [MeasureTheory.IsProbabilityMeasure (b o₂)] (h₁ : (b o₁).AbsolutelyContinuous μ) (h₂ : (b o₂).AbsolutelyContinuous μ) (h : ∀ (u : U), (b o₂).geomMean (m u) = (b o₁).geomMean (m u)) : (speaker α C (⇑(ProbabilityTheory.Kernel.ofDensity μ m)) b) o₂ = (speaker α C (⇑(ProbabilityTheory.Kernel.ofDensity μ m)) b) o₁

Against the listener of a graded meaning, two observations at which every meaning has the same geometric mean over the speaker's belief yield the same speaker.

The speaker who knows the state

The speaker of eqs. 2/6–7 knows the state, so she believes the point mass there, and her weight for an utterance is the listener's mass at the state to the power α, times the cost weight.

theorem RSA.speaker_dirac_eq_ofWeights {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) : speaker α C L MeasureTheory.Measure.dirac = ProbabilityTheory.Kernel.ofWeights fun (w : W) (u : U) => (L u) {w} ^ α * ENNReal.ofReal (Real.exp (-(α * C u)))

A speaker who knows the state weights an utterance by its listener's mass there to the power α, times the cost weight exp (-(α * C u)).

theorem RSA.speaker_dirac_eq_softmax {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) : speaker α C L MeasureTheory.Measure.dirac = ProbabilityTheory.Kernel.softmax fun (w : W) (u : U) => ↑α * ((L u) {w}).log - ↑(α * C u)

A speaker who knows the state is the softmax of the log of the listener's mass there less the cost, scaled by the rationality. The extended logarithm gives an utterance whose listener rules the state out the score ⊥ at positive rationality, so no condition on the listener is needed.

theorem RSA.isProbabilityMeasure_speaker_dirac {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {w : W} (hα : 0 ≤ α) (C : U → ℝ) (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsFiniteKernel L] (h0 : ∃ (u : U), (L u) {w} ≠ 0) : MeasureTheory.IsProbabilityMeasure ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w)

The speaker who knows the state is a probability measure there when some utterance's listener gives it mass.

theorem RSA.isMarkovKernel_speaker_dirac {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} (hα : 0 ≤ α) (C : U → ℝ) (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsFiniteKernel L] (h0 : ∀ (w : W), ∃ (u : U), (L u) {w} ≠ 0) : ProbabilityTheory.IsMarkovKernel (speaker α C (⇑L) MeasureTheory.Measure.dirac)

The speaker is a probability kernel whenever every state has a true utterance.

@[simp]

theorem RSA.speaker_dirac_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] [MeasurableSingletonClass U] (α : ℝ) (C : U → ℝ) (L : U → MeasureTheory.Measure W) (w : W) (u : U) : ((speaker α C L MeasureTheory.Measure.dirac) w) {u} = (L u) {w} ^ α * ENNReal.ofReal (Real.exp (-(α * C u))) / ∑ u' : U, (L u') {w} ^ α * ENNReal.ofReal (Real.exp (-(α * C u')))

theorem RSA.speaker_dirac_zero_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] [MeasurableSingletonClass U] (α : ℝ) (L : U → MeasureTheory.Measure W) (w : W) (u : U) : ((speaker α 0 L MeasureTheory.Measure.dirac) w) {u} = (L u) {w} ^ α / ∑ u' : U, (L u') {w} ^ α

At zero cost the speaker's weights are the listener's masses to the power α.

theorem RSA.speaker_dirac_apply_singleton_of_equiv {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] [MeasurableSingletonClass U] {W' : Type u_4} {U' : Type u_5} [MeasurableSpace W'] [MeasurableSpace U'] [Fintype W'] [MeasurableSingletonClass W'] [Fintype U'] [MeasurableSingletonClass U'] (τ : U ≃ U') (α : ℝ) (C : U' → ℝ) {L : ProbabilityTheory.Kernel U W} {L' : ProbabilityTheory.Kernel U' W'} {w : W} {w' : W'} (h : ∀ (v : U), (L' (τ v)) {w'} = (L v) {w}) (u : U) : ((speaker α C (⇑L') MeasureTheory.Measure.dirac) w') {τ u} = ((speaker α (C ∘ ⇑τ) (⇑L) MeasureTheory.Measure.dirac) w) {u}

Relabelling the utterances carries the speaker along, with the cost relabelled with them. A listener that treats τ v at w' as the other treats v at w makes the speaker at w' produce τ u as the other produces u at w.

theorem RSA.speaker_dirac_apply_singleton_eq_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] (hα : 0 < α) (h : (L u) {w} = 0) : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w) {u} = 0

A literally false utterance is never produced (positive rationality).

theorem RSA.speaker_dirac_apply_singleton_ne_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 ≤ α) (h : (L u) {w} ≠ 0) : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w) {u} ≠ 0

A literally true utterance is produced with positive mass.

theorem RSA.speaker_dirac_apply_singleton_ne_zero_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 < α) : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w) {u} ≠ 0 ↔ (L u) {w} ≠ 0

theorem RSA.speaker_dirac_apply_singleton_eq_one {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 < α) (h : (L u) {w} ≠ 0) (hother : ∀ (u' : U), u' ≠ u → (L u') {w} = 0) : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w) {u} = 1

A state with a unique applicable utterance produces it with certainty.

theorem RSA.speaker_dirac_real_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 ≤ α) (u : U) : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u} = ((L u) {w} ^ α).toReal * Real.exp (-(α * C u)) / ∑ u' : U, ((L u') {w} ^ α).toReal * Real.exp (-(α * C u'))

On reals a speaker share is the weighted listener value over the row's total.

theorem RSA.speaker_dirac_zero_real_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 ≤ α) (u : U) : ((speaker α 0 (⇑L) MeasureTheory.Measure.dirac) w).real {u} = ((L u) {w} ^ α).toReal / ∑ u' : U, ((L u') {w} ^ α).toReal

At zero cost a speaker share on reals is the listener's mass to the power α over the row's total.

theorem RSA.speaker_dirac_real_singleton_lt_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 ≤ α) (h0 : ∃ (u : U), (L u) {w} ≠ 0) {u u' : U} : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u} < ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u'} ↔ (L u) {w} ^ α * ENNReal.ofReal (Real.exp (-(α * C u))) < (L u') {w} ^ α * ENNReal.ofReal (Real.exp (-(α * C u')))

Row-preference of the speaker reduces to comparing the weighted listener values; the normalization cancels.

theorem RSA.speaker_dirac_real_singleton_div {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 ≤ α) (h : (L u) {w} ≠ 0) (u' : U) : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u'} / ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u} = (((L u') {w}).toReal / ((L u) {w}).toReal) ^ α * Real.exp (-(α * (C u' - C u)))

The odds of one utterance against another do not depend on the other alternatives. They are the ratio of the listener's masses at the state to the power α, discounted by the difference in cost.

theorem RSA.speaker_dirac_real_singleton_lt_iff_log {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 < α) {u' : U} (hu : (L u) {w} ≠ 0) (hu' : (L u') {w} ≠ 0) : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u} < ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u'} ↔ Real.log ((L u) {w}).toReal - C u < Real.log ((L u') {w}).toReal - C u'

Of two utterances with listener mass at the state, the speaker prefers the one of greater utility, the log of the listener's mass less the cost.

theorem RSA.speaker_dirac_real_singleton_of_pair {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 < α) {u' : U} (huu' : u ≠ u') (hu : (L u) {w} ≠ 0) (hu' : (L u') {w} ≠ 0) (hsupp : ∀ (v : U), (L v) {w} ≠ 0 → v = u ∨ v = u') : ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u} = (α * (Real.log ((L u) {w}).toReal - C u - (Real.log ((L u') {w}).toReal - C u'))).sigmoid

When exactly two utterances have listener mass at the state, the share of one is the logistic function of its advantage in utility over the other, scaled by the rationality.

theorem RSA.speaker_listener_truthful_dirac_eq_one {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {w : W} {u : U} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (sem : U → Set W) (hμ : μ {w} ≠ 0) (hmem : w ∈ sem u) (hother : ∀ (u' : U), u' ≠ u → w ∉ sem u') : ((speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w) {u} = 1

With Boolean meanings, a state whose only true utterance is u produces u with certainty at any prior giving the state positive mass.

theorem RSA.speaker_listener_truthful_dirac_apply_singleton_ne_zero_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (sem : U → Set W) (u : U) (w : W) : ((speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w) {u} ≠ 0 ↔ w ∈ sem u ∧ μ {w} ≠ 0

With Boolean meanings the speaker produces an utterance at a state exactly when it is true there and the state has positive prior.

theorem RSA.speaker_listener_truthful_dirac_apply_singleton_eq_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {w : W} {u : U} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) (sem : U → Set W) (h : w ∉ sem u) : ((speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w) {u} = 0

With Boolean meanings the speaker never produces a false utterance.

theorem RSA.speaker_listener_truthful_dirac_real_singleton_eq_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {w : W} {u : U} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) (sem : U → Set W) (h : w ∉ sem u) : ((speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w).real {u} = 0

theorem RSA.speaker_listener_truthful_dirac_congr {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (sem : U → Set W) {w w' : W} (hw : μ {w} ≠ 0) (hw' : μ {w'} ≠ 0) (h : ∀ (u : U), w ∈ sem u ↔ w' ∈ sem u) : (speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w' = (speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w

With Boolean meanings the speaker sees a state only through the utterances true at it, so two states of positive prior verifying the same utterances have the same production row.

theorem RSA.speaker_listener_truthful_dirac_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {w : W} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (sem : U → Set W) (hw : μ {w} ≠ 0) (u : U) : ((speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w) {u} = (sem u).indicator (fun (x : W) => (μ (sem u))⁻¹ ^ α * ENNReal.ofReal (Real.exp (-(α * C u)))) w / ∑ u' : U, (sem u').indicator (fun (x : W) => (μ (sem u'))⁻¹ ^ α * ENNReal.ofReal (Real.exp (-(α * C u')))) w

With Boolean meanings the prior cancels from the speaker, which at a state of positive prior weights each true utterance by its extension's mass to the power -α and by its cost.

theorem RSA.speaker_listener_truthful_dirac_le_of_subset {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (sem : U → Set W) {w w' : W} (hw : μ {w} ≠ 0) (hsub : ∀ (u : U), w ∈ sem u → w' ∈ sem u) {u : U} (hu : w ∈ sem u) : ((speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w') {u} ≤ ((speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w) {u}

With Boolean meanings a state verifying more utterances produces each of its true utterances less, since the prior cancels from the speaker and only the inclusion of the true utterances matters.

theorem RSA.tendsto_speaker_dirac_real_singleton_atTop {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} [MeasurableSingletonClass U] [ProbabilityTheory.IsFiniteKernel L] (hu : (L u) {w} ≠ 0) (hmax : ∀ (u' : U), u' ≠ u → ((L u') {w}).toReal * Real.exp (-C u') < ((L u) {w}).toReal * Real.exp (-C u)) : Filter.Tendsto (fun (α : ℝ) => ((speaker α C (⇑L) MeasureTheory.Measure.dirac) w).real {u}) Filter.atTop (nhds 1)

As rationality grows, the speaker puts all its mass on the utterance whose listener mass, discounted by its cost, is greatest at w, so the fully rational speaker maximizes the utility.

theorem RSA.speaker_listener_truthful_dirac_real_singleton_lt_iff {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass W] [Fintype W] [Fintype U] {α : ℝ} {w : W} [MeasurableSingletonClass U] [DiscreteMeasurableSpace W] (hα : 0 < α) (c : ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (sem : U → Set W) (hμ : μ {w} ≠ 0) {u u' : U} (hu : w ∈ sem u) (hu' : w ∈ sem u') : ((speaker α (fun (x : U) => c) (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w).real {u} < ((speaker α (fun (x : U) => c) (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac) w).real {u'} ↔ μ (sem u') < μ (sem u)

With Boolean meanings and a constant cost, a state two utterances both fit produces the utterance with the smaller extension more often, since informativity is the inverse of extension mass.

The heard form

When the listener hears only the form obs u of the speaker's choice u (eqs. 18b/21b), her state is the pair of the world and the choice, her prior the joint of the world prior and the speaker, and her channel the point mass at the form. Her first marginal is her belief about the world and her second her belief about the choice.

theorem RSA.listener_compProd_dirac_apply_singleton_ne_zero_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] [Countable O] [MeasurableSingletonClass O] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel W U) [ProbabilityTheory.IsFiniteKernel κ] (obs : U → O) (o : O) (w : W) (u : U) : ((listener (μ.compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o) {(w, u)} ≠ 0 ↔ obs u = o ∧ μ {w} ≠ 0 ∧ (κ w) {u} ≠ 0

The listener of the form gives mass to a pair of a state and a choice exactly when the choice has the form heard, the state has positive prior and it produces the choice.

theorem RSA.listener_compProd_dirac_fst_real_lt_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] [Countable O] [MeasurableSingletonClass O] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel W U) [ProbabilityTheory.IsFiniteKernel κ] (obs : U → O) [DecidableEq O] (o : O) (w₁ w₂ : W) : ((listener (μ.compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).fst.real {w₁} < ((listener (μ.compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).fst.real {w₂} ↔ ∑ u : U with obs u = o, μ.real {w₁} * (κ w₁).real {u} < ∑ u : U with obs u = o, μ.real {w₂} * (κ w₂).real {u}

The listener of the form prefers the state with the greater prior-weighted production probability pooled over the choices with the form heard.

theorem RSA.listener_compProd_dirac_snd_real_lt_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] [Countable O] [MeasurableSingletonClass O] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel W U) [ProbabilityTheory.IsFiniteKernel κ] (obs : U → O) [DecidableEq O] {o : O} {u₁ u₂ : U} (h₁ : obs u₁ = o) (h₂ : obs u₂ = o) : ((listener (μ.compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).snd.real {u₁} < ((listener (μ.compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).snd.real {u₂} ↔ ∑ w : W, μ.real {w} * (κ w).real {u₁} < ∑ w : W, μ.real {w} * (κ w).real {u₂}

Between two choices with the form heard, the listener of the form prefers the one with the greater prior-weighted production probability pooled over the states.

theorem RSA.listener_uniformOn_compProd_dirac_fst_real_lt_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] [Countable O] [MeasurableSingletonClass O] (κ : ProbabilityTheory.Kernel W U) [ProbabilityTheory.IsFiniteKernel κ] (obs : U → O) [DecidableEq O] (o : O) (w₁ w₂ : W) : ((listener ((ProbabilityTheory.uniformOn Set.univ).compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).fst.real {w₁} < ((listener ((ProbabilityTheory.uniformOn Set.univ).compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).fst.real {w₂} ↔ (κ w₁).real ↑{x : U | obs x = o} < (κ w₂).real ↑{x : U | obs x = o}

At a uniform prior the listener of the form prefers the state likelier to produce a choice with the form heard.

theorem RSA.listener_uniformOn_compProd_dirac_snd_real_lt_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSpace O] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] [Countable O] [MeasurableSingletonClass O] (κ : ProbabilityTheory.Kernel W U) [ProbabilityTheory.IsFiniteKernel κ] (obs : U → O) [DecidableEq O] {o : O} {u₁ u₂ : U} (h₁ : obs u₁ = o) (h₂ : obs u₂ = o) : ((listener ((ProbabilityTheory.uniformOn Set.univ).compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).snd.real {u₁} < ((listener ((ProbabilityTheory.uniformOn Set.univ).compProd κ) fun (p : W × U) => MeasureTheory.Measure.dirac (obs p.2)) o).snd.real {u₂} ↔ ∑ w : W, (κ w).real {u₁} < ∑ w : W, (κ w).real {u₂}

At a uniform prior the listener of the form prefers, of two choices with the form heard, the one the states together are likelier to produce.

Pragmatic listeners

The pragmatic listener (eq. 3) is the listener of a speaker.

theorem RSA.listener_speaker_listener_truthful_apply_singleton_of_notMem {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSingletonClass U] {α : ℝ} (hα : 0 < α) (C : U → ℝ) (μ : MeasureTheory.Measure W) (sem : U → Set W) {u : U} {w : W} (hw : w ∉ sem u) : ((listener μ ⇑(speaker α C (⇑(listener μ (truthful sem))) MeasureTheory.Measure.dirac)) u) {w} = 0

With Boolean meanings, hearing an utterance rules out every state it does not fit.