Mathesis
Dhruv GuptaDhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

F2 — given A nonempty, BlackwellEquivalent (learnerExperiment K) publicOnlyExperiment ↔ AuditSealed K (blackwell1953).

DeclAuditCP.blackwellEquivalent_publicOnly_iff_auditSealed
∀ {S : Type uS} {A : Type uA} {Y : Type uY} [Nonempty A] (K : AuditCP.AuditChannel S A Y),
  AuditCP.BlackwellEquivalent (AuditCP.learnerExperiment K) AuditCP.publicOnlyExperiment ↔ AuditCP.AuditSealed K
TopicAuditing

Arguments

DOIAuthorDate
MTH.R-2026-6016Dhruv GuptaDhruv Gupta2026-09-24T00:00:00Z
DOIMTH.C-2026-6016
Cite

Verification

Library
AuditCP.FiniteBlackwell
Statement digest
54d616839f6a
First verified
2026-09-24T00:00:00Z