Informativity profiles

The combinatorial shadow of a finite Boolean RSA model: for a meaning sem : C → Finset T assigning each choice its extension, the profile of a state is the multiset of extension sizes of the choices true there, and the fibre profile keeps the choices heard as a given form under obs : C → O. The uniform-prior speaker's masses are ratios of inverse-power sums over these multisets (Linglib.Pragmatics.RSA.Uniform), so preference certificates are Multiset.StrictDominates facts and pinned-rationality comparisons are ℕ inequalities.

Main definitions

• RSA.profile, RSA.fiberProfile, RSA.restProfile — extension-size multisets.
• RSA.pooledDivPowSum, RSA.familyDivPowSum — ℕ-cleared posterior masses for the evaluation registers.

Main results

• RSA.invPowSum_odds_lt_of_prodMul_strictDominates — strict dominance of fibre-by-rest products decides the odds comparison uniformly in the exponent.

def RSA.trueChoices {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] (sem : C → Finset T) (t : T) : Finset C

The choices true at a state.

Equations

• RSA.trueChoices sem t = {x : C | t ∈ sem x}

def RSA.profile {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] (sem : C → Finset T) (t : T) : Multiset ℕ

The informativity profile: extension sizes of the true choices.

Equations

• RSA.profile sem t = Multiset.map (fun (c : C) => (sem c).card) (RSA.trueChoices sem t).val

def RSA.fiberProfile {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype C] [DecidableEq T] (sem : C → Finset T) [DecidableEq O] (obs : C → O) (o : O) (t : T) : Multiset ℕ

The profile restricted to choices heard as o.

Equations

• RSA.fiberProfile sem obs o t = Multiset.map (fun (c : C) => (sem c).card) {x ∈ RSA.trueChoices sem t | obs x = o}.val

def RSA.restProfile {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype C] [DecidableEq T] (sem : C → Finset T) [DecidableEq O] (obs : C → O) (o : O) (t : T) : Multiset ℕ

The profile of true choices heard otherwise.

Equations

• RSA.restProfile sem obs o t = Multiset.map (fun (c : C) => (sem c).card) {x ∈ RSA.trueChoices sem t | obs x ≠ o}.val

theorem RSA.profile_eq_fiberProfile_add_restProfile {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype C] [DecidableEq T] (sem : C → Finset T) [DecidableEq O] (obs : C → O) (o : O) (t : T) : profile sem t = fiberProfile sem obs o t + restProfile sem obs o t

theorem RSA.zero_notMem_profile {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] (sem : C → Finset T) (t : T) : 0 ∉ profile sem t

theorem RSA.zero_notMem_fiberProfile {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype C] [DecidableEq T] (sem : C → Finset T) [DecidableEq O] (obs : C → O) (o : O) (t : T) : 0 ∉ fiberProfile sem obs o t

theorem RSA.zero_notMem_restProfile {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype C] [DecidableEq T] (sem : C → Finset T) [DecidableEq O] (obs : C → O) (o : O) (t : T) : 0 ∉ restProfile sem obs o t

theorem RSA.exists_of_fiberProfile_ne_zero {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype C] [DecidableEq T] (sem : C → Finset T) [DecidableEq O] (obs : C → O) {o : O} {t : T} (h : fiberProfile sem obs o t ≠ 0) : ∃ (c : C), obs c = o ∧ t ∈ sem c

A nonempty fibre profile exhibits an o-shaped true choice — certificates carry their own truth witnesses.

theorem RSA.profile_invPowSum_toReal {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] (sem : C → Finset T) {α : ℝ} (hα : 0 ≤ α) (t : T) : (Multiset.invPowSum α (profile sem t)).toReal = ∑ c : C, if t ∈ sem c then (↑(sem c).card)⁻¹ ^ α else 0

The real profile sum, expanded over the choices: the informativity weights of the choices true at the state.

theorem RSA.profile_ne_zero {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] (sem : C → Finset T) (hsem : ∀ (t : T), ∃ (c : C), t ∈ sem c) (t : T) : profile sem t ≠ 0

theorem RSA.invPowSum_odds_lt_of_prodMul_strictDominates {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype C] [DecidableEq T] (sem : C → Finset T) [DecidableEq O] (obs : C → O) {α : ℝ} (hα : 0 < α) {o : O} {t₁ t₂ : T} (hcert : ((fiberProfile sem obs o t₂).prodMul (restProfile sem obs o t₁)).StrictDominates ((fiberProfile sem obs o t₁).prodMul (restProfile sem obs o t₂))) : (Multiset.invPowSum α (fiberProfile sem obs o t₁)).toReal * (Multiset.invPowSum α (profile sem t₂)).toReal < (Multiset.invPowSum α (fiberProfile sem obs o t₂)).toReal * (Multiset.invPowSum α (profile sem t₁)).toReal

The certificate closes the odds comparison: strict domination of the fibre-by-rest cross products decides it uniformly in the rationality (the shared fibre-by-fibre terms cancel).

def RSA.pooledDivPowSum {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] (sem : C → Finset T) [Fintype T] (D k : ℕ) (c : C) : ℕ

The ℕ-cleared production mass of a choice, pooled over its true states: its common-denominator weight times, per true state, the product of the other states' cleared partition sums. Pooled evaluation-register hypotheses compare these.

Equations

• RSA.pooledDivPowSum sem D k c = (D / (sem c).card) ^ k * ∑ t ∈ sem c, ∏ t' ∈ Finset.univ.erase t, Multiset.divPowSum D k (RSA.profile sem t')

theorem RSA.pooledDivPowSum_eq_sum {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] (sem : C → Finset T) [Fintype T] (D k : ℕ) (c : C) : pooledDivPowSum sem D k c = ∑ t : T, if t ∈ sem c then (D / (sem c).card) ^ k * ∏ t' ∈ Finset.univ.erase t, Multiset.divPowSum D k (profile sem t') else 0

def RSA.familyDivPowSum {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] [Fintype T] {Λ : Type u_4} [Fintype Λ] [DecidableEq Λ] (sem : Λ → C → Finset T) (D k : ℕ) (c : C) (E : Finset (T × Λ)) : ℕ

The ℕ-cleared posterior mass of an event of (state, latent) pairs given c for a family of extensions: per pair, its common-denominator speaker weight times the product of the other pairs' cleared partition sums. Family evaluation-register hypotheses compare these.

Equations

• RSA.familyDivPowSum sem D k c E = ∑ p ∈ E, (if p.1 ∈ sem p.2 c then (D / (sem p.2 c).card) ^ k else 0) * ∏ q ∈ Finset.univ.erase p, Multiset.divPowSum D k (RSA.profile (sem q.2) q.1)

theorem RSA.familyDivPowSum_eq_sum {T : Type u_1} {C : Type u_2} [Fintype C] [DecidableEq T] [Fintype T] {Λ : Type u_4} [Fintype Λ] [DecidableEq Λ] (sem : Λ → C → Finset T) (D k : ℕ) (c : C) (E : Finset (T × Λ)) : familyDivPowSum sem D k c E = ∑ p : T × Λ, if p ∈ E then (if p.1 ∈ sem p.2 c then (D / (sem p.2 c).card) ^ k else 0) * ∏ q ∈ Finset.univ.erase p, Multiset.divPowSum D k (profile (sem q.2) q.1) else 0